Theorem r19.21adv 1710

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)

Hypothesis

Ref	Expression
r19.21adv.1	|- (ph -> (ps -> (x e. A -> ch)))

Assertion

Ref	Expression
r19.21adv	|- (ph -> (ps -> A.x e. A ch))

Distinct variable groups:   ph,x   ps,x

Proof of Theorem r19.21adv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		ax-17 968	. 2 |- (ps -> A.xps)
3		r19.21adv.1	. 2 |- (ph -> (ps -> (x e. A -> ch)))
4	1, 2, 3	r19.21ad 1709	1 |- (ph -> (ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 955  A.wral 1637

This theorem is referenced by:  r19.21adva 1711  r19.21aivv 1712  ralxfrd 2887  wefrc 2933  oneqmin 3008  isocnv 3881  isotr 3882  f1oiso 3889  tfrlem1 3896  abianfp 3947  omsmo 4241  mapenlem2 4470  nneneq 4492  cflim 4881  nnleltp1t 5901  infmrcl 6016  supxrunb2 6037  zmax 6168  zbtwnre 6169  fzrevralt 6451  sqr2irrlem3 6656  seq1ublem 6848  cau3ir 6852  clm4le 7019  climconst 7031  climshft 7041  climcau 7092  caucvglem2 7094  caucvg 7099  expcnvlem6 7167  topbast 7569  clsval2 7627  elcls3 7652  neips 7668  clslp 7689  cncnp 7717  opnuni 7808  opnin 7809  lmnn 7873  metcnp4 7904  xplmi 7907  bcthlem21 7953  isgrp2i 8011  ipblnfi 8447  hial0 8889  hial02 8890  ocsh 9072  ococss 9082  occllem6 9094  projlem26 9127  pjtheu 9150  lnopm 9840  adjlnopt 9934  bra11 9954  pjss2co 10003  pj3cor1 10047  strlem3a 10089  hstrlem3a 10097  mdbr3 10134  mdbr4 10135  dmdmdt 10137  dmdbr3 10141  dmdbr4 10142  ssmd2 10147  mdslmd1 10164  mdsymlem7 10244  cdj1 10265  cdj3lem2b 10269  ghomf1olem 10301

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  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain