![]() |
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 1829 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
3 | 2 | eximi 1829 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃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: 2mo 2636 2eu6 2645 cgsex2g 3508 cgsex4g 3509 cgsex4gOLD 3510 cgsex4gOLDOLD 3511 dtruALT2 5370 exexneq 5436 dtruOLD 5443 mosubopt 5512 elopaelxpOLD 5768 ssrel 5784 ssrelOLD 5785 relopabi 5824 xpdifid 6174 ssoprab2i 7531 hash1to3 14496 catcone0 17686 isfunc 17869 umgr3v3e3cycl 30086 frgrconngr 30196 bnj605 34689 bnj607 34698 bnj916 34715 bnj996 34738 bnj907 34749 bnj1128 34772 funen1cnv 34862 cusgr3cyclex 34897 acycgrislfgr 34913 umgracycusgr 34915 cusgracyclt3v 34917 ac6s6f 37797 mnringmulrcld 43812 2uasbanh 44147 2uasbanhVD 44497 elsprel 46957 sprssspr 46963 2exopprim 47007 reuopreuprim 47008 |
Copyright terms: Public domain | W3C validator |