Theorem exlimivv 1952

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)

Hypothesis

Ref	Expression
exlimivv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimivv	⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Distinct variable groups:   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	exlimiv 1651	. 2 ⊢ (∃𝑦𝜑 → 𝜓)
3	2	exlimiv 1651	1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2858  cgsex4g  2859  opabss  4190  copsexg  4379  elopab  4395  epelg  4430  0nelelxp  4798  elvvuni  4834  optocl  4846  xpsspw  4882  relopabi  4900  relop  4925  reldmm  4995  elreldm  5003  xpmlem  5203  dfco2a  5283  unielrel  5310  oprabid  6107  1stval2  6379  2ndval2  6380  xp1st  6389  xp2nd  6390  poxp  6458  rntpos  6518  dftpos4  6524  tpostpos  6525  tfrlem7  6578  th3qlem2  6902  ener  7056  domtr  7062  unen  7095  xpsnen  7109  mapen  7136  ltdcnq  7754  archnqq  7774  enq0tr  7791  nqnq0pi  7795  nqnq0  7798  nqpnq0nq  7810  nqnq0a  7811  nqnq0m  7812  nq0m0r  7813  nq0a0  7814  nq02m  7822  prarloc  7860  axaddcl  8221  axmulcl  8223  hashfacen  11262  fundm2domnop0  11278  fsumdvdsmul  16019  griedg0ssusgr  16406  bj-inex  16847