![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exim | Structured version Visualization version GIF version |
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
exim | ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
2 | 1 | aleximi 1835 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: eximi 1838 19.38b 1844 19.23v 1946 alequexv 2005 nf5-1 2142 spimt 2386 darii 2661 festino 2670 baroco 2672 darapti 2680 elex2OLD 3496 elex22 3497 vtoclegftOLD 3575 spcimgft 3578 rspn0 4353 exel 5434 bj-axdd2 35470 bj-2exim 35489 bj-sylget 35498 bj-alexim 35504 bj-cbvalimt 35516 bj-cbveximt 35517 bj-eqs 35552 bj-nnf-exlim 35634 bj-nnflemee 35641 bj-nnflemae 35642 bj-axc10 35661 bj-alequex 35662 bj-spimtv 35672 bj-spcimdv 35775 bj-spcimdvv 35776 sn-exelALT 41035 2exim 43138 pm11.71 43156 onfrALTlem2 43307 19.41rg 43311 ax6e2nd 43319 elex2VD 43599 elex22VD 43600 onfrALTlem2VD 43650 19.41rgVD 43663 ax6e2eqVD 43668 ax6e2ndVD 43669 ax6e2ndeqVD 43670 ax6e2ndALT 43691 ax6e2ndeqALT 43692 |
Copyright terms: Public domain | W3C validator |