Theorem exlimivv 1921

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

Syntax hints:   → wi 4  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2810  cgsex4g  2811  opabss  4116  copsexg  4296  elopab  4312  epelg  4345  0nelelxp  4712  elvvuni  4747  optocl  4759  xpsspw  4795  relopabi  4811  relop  4836  elreldm  4913  xpmlem  5112  dfco2a  5192  unielrel  5219  oprabid  5989  1stval2  6254  2ndval2  6255  xp1st  6264  xp2nd  6265  poxp  6331  rntpos  6356  dftpos4  6362  tpostpos  6363  tfrlem7  6416  th3qlem2  6738  ener  6884  domtr  6890  unen  6922  xpsnen  6931  mapen  6958  ltdcnq  7530  archnqq  7550  enq0tr  7567  nqnq0pi  7571  nqnq0  7574  nqpnq0nq  7586  nqnq0a  7587  nqnq0m  7588  nq0m0r  7589  nq0a0  7590  nq02m  7598  prarloc  7636  axaddcl  7997  axmulcl  7999  hashfacen  11003  fundm2domnop0  11012  fsumdvdsmul  15538  bj-inex  15981