Theorem r19.21adv 1262

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 group(s):   ph,x   ps,x

Proof of Theorem r19.21adv

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

Syntax hints:   -> wi 2   e. wcel 1092  A.wral 1201

This theorem is referenced by:  r19.21aivv 1263  wefrc 2195  oneqmin 2273  ralxp 2456  isocnv 2934  isotr 2935  isowe 2941  f1oiso 2942  tfrlem1 2949  abianfp 3000  omsmo 3196  mapenlem2 3385  nneneq 3408  fiint 3445  cflim 3704  nnleltp1t 4448  zmax 4618  zbtwnre 4619  sqr2irrlem3 4779  hial0 5058  ocsh 5164  ococss 5174  occllem6 5185  projlem26 5218  pjthu 5241  pjthu2 5242  pjss2co 5634  pj3cor1 5661  strlem3a 5693  mdbr3 5729  mdbr4 5730  dmdbr 5731  ssmd2 5735  mdsymlem7 5782

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org