Theorem r19.22sdv 1741

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 1740	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 960  E.wrex 1649

This theorem is referenced by:  iunpw 2920  fvelima 3770  ssfi 4547  ssfiOLD 4548  isfinite2OLD 4558  clm4le 7081  2climnn 7102  2climnn0 7103  climsqueeze 7140  climsqueeze2 7141  climabslem 7148  caucvglem4 7160  rescncf 7272  tgclt 7623  tgss2t 7636  neiss 7720  ssnei2 7727  cnpco 7766  cnsscnp 7769  opni3 7863  opnuni 7865  neibl 7874  metcnss2 7896  lmuni 7948  caussi 7951  metcnp4lem2 7966  xplmi 7970  xplm 7972  iscms2lem5 7990  lmcau 7993  isgrp 8038  ubthlem6 8530  minveclem25 8565  minveclem26 8566  htthlem12 8627  hlimcaui 9101  occllem6 9173  projlem25 9205  projlem31 9211  osumlem4 9576

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain