Theorem r19.22sdv 1730

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.)

Hypothesis

Ref	Expression
r19.22sdv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
r19.22sdv	|- (ph -> (E.x e. A ps -> E.x e. A ch))

Distinct variable group:   ph,x

Proof of Theorem r19.22sdv

Step	Hyp	Ref	Expression
1		r19.22sdv.1	. . 3 |- (ph -> (ps -> ch))
2	1	a1d 12	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	2	r19.22dv 1729	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 955  E.wrex 1638

This theorem is referenced by:  iunpw 2904  fvelima 3749  ssfi 4515  isfinite2 4523  clm4le 7019  2climnn 7039  2climnn0 7040  climsqueeze 7076  climsqueeze2 7077  climabslem 7084  caucvglem4 7096  rescncf 7207  tgclt 7566  tgss2t 7579  neiss 7664  ssnei2 7671  cnpco 7708  cnsscnp 7711  opni3 7806  opnuni 7808  neibl 7817  metcnss2 7838  lmuni 7886  caussi 7889  metcnp4lem2 7903  xplmi 7907  xplm 7909  iscms2lem5 7927  lmcau 7930  isgrp 7975  ubthlem6 8465  minveclem25 8500  minveclem26 8501  htthlem12 8561  hlimcaui 9027  occllem6 9094  projlem25 9126  projlem31 9132  osumlem4 9498

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-ral 1641  df-rex 1642

Copyright terms: Public domain