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  2641  2eu6  2650  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  dtruALT2  5312  exexneq  5381  dtruOLD  5388  mosubopt  5457  ssrel  5730  relopabi  5769  xpdifid  6121  ssoprab2i  7464  hash1to3  14417  catcone0  17611  isfunc  17789  umgr3v3e3cycl  30146  frgrconngr  30256  bnj605  34873  bnj607  34882  bnj916  34899  bnj996  34922  bnj907  34933  bnj1128  34956  funen1cnv  35054  cusgr3cyclex  35108  acycgrislfgr  35124  umgracycusgr  35126  cusgracyclt3v  35128  ac6s6f  38152  mnringmulrcld  44201  2uasbanh  44535  2uasbanhVD  44884  elsprel  47460  sprssspr  47466  2exopprim  47510  reuopreuprim  47511