|   | 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 1831 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 | 
| This theorem is referenced by: eximi 1834 19.38b 1840 19.23v 1941 alequexv 1999 nf5-1 2144 spimt 2390 darii 2664 festino 2673 baroco 2675 darapti 2683 elex2OLD 3504 elex22 3505 spcimgfi1OLD 3547 vtoclegftOLD 3588 sbccomlem 3868 rspn0 4355 exel 5437 bj-axdd2 36594 bj-2exim 36613 bj-sylget 36623 bj-alexim 36629 bj-cbvalimt 36641 bj-cbveximt 36642 bj-eqs 36677 bj-nnf-exlim 36758 bj-nnflemee 36765 bj-nnflemae 36766 bj-axc10 36785 bj-alequex 36786 bj-spimtv 36796 bj-spcimdv 36897 bj-spcimdvv 36898 sn-exelALT 42258 2exim 44403 pm11.71 44421 onfrALTlem2 44571 19.41rg 44575 ax6e2nd 44583 elex2VD 44863 elex22VD 44864 onfrALTlem2VD 44914 19.41rgVD 44927 ax6e2eqVD 44932 ax6e2ndVD 44933 ax6e2ndeqVD 44934 ax6e2ndALT 44955 ax6e2ndeqALT 44956 | 
| Copyright terms: Public domain | W3C validator |