Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > aleximi | Structured version Visualization version Unicode version |
Description: A variant of al2imi 1743: instead of applying quantifiers to the final implication, replace them with . A shorter proof is possible using nfa1 2028, sps 2055 and eximd 2085, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.) |
Ref | Expression |
---|---|
aleximi.1 |
Ref | Expression |
---|---|
aleximi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aleximi.1 | . . . . 5 | |
2 | 1 | con3d 148 | . . . 4 |
3 | 2 | al2imi 1743 | . . 3 |
4 | alnex 1706 | . . 3 | |
5 | alnex 1706 | . . 3 | |
6 | 3, 4, 5 | 3imtr3g 284 | . 2 |
7 | 6 | con4d 114 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: alexbii 1760 exim 1761 exanOLD 1789 eximdh 1791 19.29 1801 19.29r 1802 19.35 1805 19.25 1808 19.30 1809 19.40b 1815 speimfw 1876 aeveq 1982 aevOLD 2162 2ax6elem 2449 mo3 2507 mopick 2535 2mo 2551 ssopab2 5001 ssoprab2 6711 axextnd 9413 bj-2exim 32595 bj-exalimi 32612 bj-sb56 32639 wl-dveeq12 33311 wl-mo3t 33358 pm10.56 38569 2exim 38578 |
Copyright terms: Public domain | W3C validator |