# Metamath Proof Explorer

## Theorem axc5c4c711to11

Description: Rederivation of ax-11 from axc5c4c711 . Note that ax-11 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc5c4c711to11 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 ax-1 ${⊢}{\phi }\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
2 1 2alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
3 axc5c4c711toc7 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
4 3 con4i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
5 pm2.21 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \left(\left({\phi }\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\right)\right)$
6 axc5c4c711 ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \left(\left({\phi }\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\right)\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 sp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
8 6 7 syl6 ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \left(\left({\phi }\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\right)\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
9 5 8 syl ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
10 9 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
11 axc5c4c711toc7 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
12 10 11 nsyl4 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
13 12 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
14 4 13 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)$
15 pm2.27 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to \left(\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to {\phi }\right)$
16 id ${⊢}{\phi }\to {\phi }$
17 15 16 mpg ${⊢}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to {\phi }$
18 17 2alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\phi }\right)\to {\phi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
19 2 14 18 3syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$