Theorem 2eximdv 1954

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1867. (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
2alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥, 𝑦)   𝜒(𝑥, 𝑦)

Proof of Theorem 2eximdv

Step	Hyp	Ref	Expression
1		2alimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	eximdv 1952	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒))
3	2	eximdv 1952	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  ax-5 1945

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

This theorem is used by:  2eu6  2684  cgsex2g  3499  cgsex4g  3500  spc2egv  3557  rexopabb  5506  elrelb  5780  relop  5834  elinxp  6020  opreuopreu  8070  en3  9300  en4  9301  addsrpr  11187  mulsrpr  11188  hash2prde  14642  hash3tpde  14665  pmtrrn2  19704  umgredg  29746  umgr2wlkon  30569  trsp2cyc  33754  mpofvd  35797  acycgrsubgr  36080  satfvsucsuc  36297  fmla0xp  36315  fundmpss  36710  cgsex2gd  38250  pellexlem5  44033  ax6e2eq  45731  fnchoice  46251  fzisoeu  46521  stoweidlem35  47250  stoweidlem60  47275  or2expropbi  48309  ich2exprop  48758  grlimprclnbgr  49299