# Metamath Proof Explorer

## Theorem ax12indi

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Implication case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ax12indn.1 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
ax12indi.2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\psi }\right)\right)\right)$
Assertion ax12indi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left(\left({\phi }\to {\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ax12indn.1 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\right)\right)$
2 ax12indi.2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\psi }\right)\right)\right)$
3 1 ax12indn ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left(¬{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)\right)$
4 3 imp ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {x}={y}\right)\to \left(¬{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)$
5 pm2.21 ${⊢}¬{\phi }\to \left({\phi }\to {\psi }\right)$
6 5 imim2i ${⊢}\left({x}={y}\to ¬{\phi }\right)\to \left({x}={y}\to \left({\phi }\to {\psi }\right)\right)$
7 6 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)$
8 4 7 syl6 ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {x}={y}\right)\to \left(¬{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)\right)$
9 2 imp ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {x}={y}\right)\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\psi }\right)\right)$
10 ax-1 ${⊢}{\psi }\to \left({\phi }\to {\psi }\right)$
11 10 imim2i ${⊢}\left({x}={y}\to {\psi }\right)\to \left({x}={y}\to \left({\phi }\to {\psi }\right)\right)$
12 11 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)$
13 9 12 syl6 ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {x}={y}\right)\to \left({\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)\right)$
14 8 13 jad ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge {x}={y}\right)\to \left(\left({\phi }\to {\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)\right)$
15 14 ex ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left(\left({\phi }\to {\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({\phi }\to {\psi }\right)\right)\right)\right)$