Theorem 2eximi 1869

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2mo  2679  2eu6  2687  cgsex2g  3503  cgsex4g  3504  dtruALT2  5344  exexneq  5419  mosubopt  5496  ssrel  5772  relopabi  5812  xpdifid  6168  xpdifcnvepel  6169  ssoprab2i  7527  hash1to3  14540  catcone0  17753  isfunc  17931  umgr3v3e3cycl  30550  frgrconngr  30660  bnj605  35308  bnj607  35317  bnj916  35334  bnj996  35357  bnj907  35368  bnj1128  35391  funen1cnv  35490  cusgr3cyclex  35640  acycgrislfgr  35656  umgracycusgr  35658  cusgracyclt3v  35660  ac6s6f  38854  mnringmulrcld  44984  2uasbanh  45302  2uasbanhVD  45651  elsprel  48256  sprssspr  48262  2exopprim  48306  reuopreuprim  48307