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 1826 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
3 | 2 | eximi 1826 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 2mo 2726 2eu6 2737 cgsex2g 3536 cgsex4g 3537 vtocl2OLD 3560 dtru 5262 mosubopt 5391 elopaelxp 5634 ssrel 5650 relopabi 5687 xpdifid 6018 ssoprab2i 7252 hash1to3 13837 isfunc 17122 umgr3v3e3cycl 27890 frgrconngr 28000 bnj605 32078 bnj607 32087 bnj916 32104 bnj996 32126 bnj907 32136 bnj1128 32159 funen1cnv 32254 cusgr3cyclex 32280 acycgrislfgr 32296 umgracycusgr 32298 cusgracyclt3v 32300 bj-dtru 34036 ac6s6f 35332 sn-dtru 38989 2uasbanh 40772 2uasbanhVD 41122 elsprel 43514 sprssspr 43520 2exopprim 43564 reuopreuprim 43565 |
Copyright terms: Public domain | W3C validator |