Theorem 2eximi 1753

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

Syntax hints:   → wi 4  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2mo  2539  2eu6  2546  cgsex2g  3212  cgsex4g  3213  vtocl2  3234  vtocl3  3235  dtru  4783  mosubopt  4897  elopaelxp  5114  ssrel  5130  relopabi  5167  xpdifid  5481  ssoprab2i  6647  hash1to3  13128  isfunc  16347  usgraop  25879  usgraedg4  25916  3v3e3cycl2  26192  frconngra  26548  bnj605  30231  bnj607  30240  bnj916  30257  bnj996  30279  bnj907  30289  bnj1128  30312  bj-dtru  31985  ac6s6f  33151  2uasbanh  37798  2uasbanhVD  38169  umgr3v3e3cycl  41351  frgrconngr  41464