Theorem exlimivv 1635

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	⊢ (∃x∃yφ → ψ)

Distinct variable groups:   ψ,x   ψ,y

Allowed substitution hints:   φ(x,y)

Proof of Theorem exlimivv

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 ⊢ (φ → ψ)
2	1	exlimiv 1634	. 2 ⊢ (∃yφ → ψ)
3	2	exlimiv 1634	1 ⊢ (∃x∃yφ → ψ)

Syntax hints:   → wi 4  ∃wex 1541

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  2mo  2282  cgsex2g  2891  cgsex4g  2892  elxpk  4196  opkabssvvk  4208  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  cokrelk  4284  pw1equn  4331  pw1eqadj  4332  copsexg  4607  elopab  4696  brsi  4761  optocl  4838  xpnz  5045  dfco2a  5081  dfxp2  5113  1stfo  5505  2ndfo  5506  brswap  5509  oprabid  5550  brtxp  5783  txpcofun  5803  pw1fnf1o  5855  entr  6038  unen  6048  xpen  6055  xpassen  6057  mucnc  6131  muccl  6132  muccom  6134  mucass  6135  ncaddccl  6144  ncdisjeq  6148  tcdi  6164  elce  6175  ce0addcnnul  6179  cenc  6181  sbthlem3  6205  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  taddc  6229  letc  6231  ce2le  6233  muc0or  6252  frecxp  6314