| 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 1835 | . 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓) |
| 3 | 2 | eximi 1835 | 1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: 2mo 2648 2eu6 2657 cgsex2g 3527 cgsex4g 3528 cgsex4gOLD 3529 dtruALT2 5370 exexneq 5439 dtruOLD 5446 mosubopt 5515 elopaelxpOLD 5776 ssrel 5792 ssrelOLD 5793 relopabi 5832 xpdifid 6188 ssoprab2i 7544 hash1to3 14531 catcone0 17730 isfunc 17909 umgr3v3e3cycl 30203 frgrconngr 30313 bnj605 34921 bnj607 34930 bnj916 34947 bnj996 34970 bnj907 34981 bnj1128 35004 funen1cnv 35102 cusgr3cyclex 35141 acycgrislfgr 35157 umgracycusgr 35159 cusgracyclt3v 35161 ac6s6f 38180 mnringmulrcld 44247 2uasbanh 44581 2uasbanhVD 44931 elsprel 47462 sprssspr 47468 2exopprim 47512 reuopreuprim 47513 |
| Copyright terms: Public domain | W3C validator |