Theorem exlimdvv 1937

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2204. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
exlimdvv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

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

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥   𝜒,𝑦   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem exlimdvv

Step	Hyp	Ref	Expression
1		exlimdvv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	exlimdv 1936	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1936	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  euotd  5513  opabssxpd  5723  dfpo2  6295  funopg  6582  fmptsnd  7169  tpres  7204  opreuopreu  8022  frxp2  8132  frxp3  8139  fundmen  9033  undomOLD  9062  ttrcltr  9713  infxpenc2  10019  zorn2lem6  10498  fpwwe2lem11  10638  genpnnp  11002  addsrmo  11070  mulsrmo  11071  hashfun  14399  hash2exprb  14434  rtrclreclem3  15009  summo  15665  fsum2dlem  15718  ntrivcvgmul  15850  prodmo  15882  fprod2dlem  15926  iscatd2  17627  gsumval3eu  19774  gsum2d2  19844  ptbasin  23088  txcls  23115  txbasval  23117  reconn  24351  phtpcer  24518  pcohtpy  24543  mbfi1flimlem  25247  mbfmullem  25250  itg2add  25284  fsumvma  26723  umgr3v3e3cycl  29475  conngrv2edg  29486  2ndresdju  31912  cusgracyclt3v  34216  pconnconn  34291  txsconn  34301  neibastop1  35330  itg2addnc  36628  riscer  36942  dalem62  38691  pellexlem5  41653  pellex  41655  nnoeomeqom  42144  iunrelexpuztr  42552  fzisoeu  44089  stoweidlem53  44848  stoweidlem56  44851  fundcmpsurinjpreimafv  46155  ichnreuop  46219