Theorem 2eximi 1839

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 1838	. 2 ⊢ (∃𝑦𝜑 → ∃𝑦𝜓)
3	2	eximi 1838	1 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  2mo  2650  2eu6  2658  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  dtru  5288  mosubopt  5418  elopaelxp  5667  ssrel  5683  relopabi  5721  xpdifid  6060  ssoprab2i  7363  hash1to3  14133  catcone0  17313  isfunc  17495  umgr3v3e3cycl  28449  frgrconngr  28559  bnj605  32787  bnj607  32796  bnj916  32813  bnj996  32836  bnj907  32847  bnj1128  32870  funen1cnv  32960  cusgr3cyclex  32998  acycgrislfgr  33014  umgracycusgr  33016  cusgracyclt3v  33018  bj-dtru  34926  ac6s6f  36258  sn-dtru  40116  mnringmulrcld  41735  2uasbanh  42070  2uasbanhVD  42420  elsprel  44815  sprssspr  44821  2exopprim  44865  reuopreuprim  44866