![]() |
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 1896 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1618 ∃wex 1841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 |
This theorem depends on definitions: df-bi 197 df-ex 1842 |
This theorem is referenced by: eximi 1899 19.38b 1905 19.23v 2008 19.23vOLD 2056 nf5-1 2160 19.8a 2187 19.9ht 2278 spimt 2386 elex2 3344 elex22 3345 vtoclegft 3408 spcimgft 3412 bj-axdd2 32853 bj-2exim 32872 bj-exlimh 32879 bj-alexim 32882 bj-sbex 32903 bj-alequexv 32932 bj-eqs 32940 bj-axc10 32984 bj-alequex 32985 bj-spimtv 32995 bj-spcimdv 33161 bj-spcimdvv 33162 2exim 39049 pm11.71 39068 onfrALTlem2 39232 19.41rg 39237 ax6e2nd 39245 elex2VD 39541 elex22VD 39542 onfrALTlem2VD 39593 19.41rgVD 39606 ax6e2eqVD 39611 ax6e2ndVD 39612 ax6e2ndeqVD 39613 ax6e2ndALT 39634 ax6e2ndeqALT 39635 |
Copyright terms: Public domain | W3C validator |