![]() |
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 1826 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: eximi 1829 19.38b 1835 19.23v 1937 alequexv 1996 nf5-1 2133 spimt 2379 darii 2653 festino 2662 baroco 2664 darapti 2672 elex2OLD 3485 elex22 3486 vtoclegftOLD 3570 spcimgft 3572 rspn0 4354 exel 5438 bj-axdd2 36245 bj-2exim 36264 bj-sylget 36273 bj-alexim 36279 bj-cbvalimt 36291 bj-cbveximt 36292 bj-eqs 36327 bj-nnf-exlim 36409 bj-nnflemee 36416 bj-nnflemae 36417 bj-axc10 36436 bj-alequex 36437 bj-spimtv 36447 bj-spcimdv 36549 bj-spcimdvv 36550 sn-exelALT 41883 nfa1w 42267 2exim 43990 pm11.71 44008 onfrALTlem2 44159 19.41rg 44163 ax6e2nd 44171 elex2VD 44451 elex22VD 44452 onfrALTlem2VD 44502 19.41rgVD 44515 ax6e2eqVD 44520 ax6e2ndVD 44521 ax6e2ndeqVD 44522 ax6e2ndALT 44543 ax6e2ndeqALT 44544 |
Copyright terms: Public domain | W3C validator |