Theorem exlimivv 1890

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

Syntax hints:   → wi 4  ∃wex 1486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1443  ax-ie2 1488  ax-17 1520

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2767  cgsex4g  2768  opabss  4054  copsexg  4230  elopab  4244  epelg  4276  0nelelxp  4641  elvvuni  4676  optocl  4688  xpsspw  4724  relopabi  4738  relop  4762  elreldm  4838  xpmlem  5033  dfco2a  5113  unielrel  5140  oprabid  5889  1stval2  6138  2ndval2  6139  xp1st  6148  xp2nd  6149  poxp  6215  rntpos  6240  dftpos4  6246  tpostpos  6247  tfrlem7  6300  th3qlem2  6620  ener  6761  domtr  6767  unen  6798  xpsnen  6803  mapen  6828  ltdcnq  7363  archnqq  7383  enq0tr  7400  nqnq0pi  7404  nqnq0  7407  nqpnq0nq  7419  nqnq0a  7420  nqnq0m  7421  nq0m0r  7422  nq0a0  7423  nq02m  7431  prarloc  7469  axaddcl  7830  axmulcl  7832  hashfacen  10775  bj-inex  14027