![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2eximi | Structured version Visualization version GIF version |
Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Ref | Expression |
---|---|
eximi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
2eximi | ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eximi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | eximi 1797 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
3 | 2 | eximi 1797 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 |
This theorem depends on definitions: df-bi 199 df-ex 1743 |
This theorem is referenced by: 2mo 2679 2eu6 2688 cgsex2g 3459 cgsex4g 3460 vtocl2OLD 3481 dtru 5125 mosubopt 5257 elopaelxp 5492 ssrel 5508 relopabi 5545 xpdifid 5867 ssoprab2i 7081 hash1to3 13663 isfunc 16995 umgr3v3e3cycl 27716 frgrconngr 27831 bnj605 31826 bnj607 31835 bnj916 31852 bnj996 31874 bnj907 31884 bnj1128 31907 bj-dtru 33625 ac6s6f 34895 sn-dtru 38556 2uasbanh 40314 2uasbanhVD 40664 elsprel 43006 sprssspr 43012 2exopprim 43056 reuopreuprim 43057 |
Copyright terms: Public domain | W3C validator |