Theorem 2eximi 1836

Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
eximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2eximi	⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Proof of Theorem 2eximi

Step	Hyp	Ref	Expression
1		eximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	eximi 1835	. 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓)
3	2	eximi 1835	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

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  2642  2eu6  2651  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  dtruALT2  5327  exexneq  5396  dtruOLD  5403  mosubopt  5472  elopaelxpOLD  5731  ssrel  5747  ssrelOLD  5748  relopabi  5787  xpdifid  6143  ssoprab2i  7502  hash1to3  14463  catcone0  17654  isfunc  17832  umgr3v3e3cycl  30119  frgrconngr  30229  bnj605  34903  bnj607  34912  bnj916  34929  bnj996  34952  bnj907  34963  bnj1128  34986  funen1cnv  35084  cusgr3cyclex  35123  acycgrislfgr  35139  umgracycusgr  35141  cusgracyclt3v  35143  ac6s6f  38162  mnringmulrcld  44210  2uasbanh  44544  2uasbanhVD  44893  elsprel  47466  sprssspr  47472  2exopprim  47516  reuopreuprim  47517