Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 19.35 | Structured version Visualization version Unicode version |
Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
Ref | Expression |
---|---|
19.35 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.27 42 | . . . 4 | |
2 | 1 | aleximi 1759 | . . 3 |
3 | 2 | com12 32 | . 2 |
4 | exnal 1754 | . . . 4 | |
5 | pm2.21 120 | . . . . 5 | |
6 | 5 | eximi 1762 | . . . 4 |
7 | 4, 6 | sylbir 225 | . . 3 |
8 | exa1 1765 | . . 3 | |
9 | 7, 8 | ja 173 | . 2 |
10 | 3, 9 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 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: 19.35i 1806 19.35ri 1807 19.25 1808 19.43 1810 nfimt 1821 nfimdOLDOLD 1824 speimfwALT 1877 19.39 1899 19.24 1900 19.36v 1904 19.37v 1910 19.36 2098 19.37 2100 spimt 2253 grothprim 9656 bj-spimt2 32709 bj-spimtv 32718 bj-snsetex 32951 |
Copyright terms: Public domain | W3C validator |