Theorem r19.20i 1696

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
r19.20i.1	|- (x e. A -> (ph -> ps))

Assertion

Ref	Expression
r19.20i	|- (A.x e. A ph -> A.x e. A ps)

Proof of Theorem r19.20i

Step	Hyp	Ref	Expression
1		r19.20i.1	. . 3 |- (x e. A -> (ph -> ps))
2	1	a2i 9	. 2 |- ((x e. A -> ph) -> (x e. A -> ps))
3	2	r19.20i2 1695	1 |- (A.x e. A ph -> A.x e. A ps)

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

This theorem is referenced by:  r19.20ia 1697  r19.20si 1698  r19.12 1732  exfo 3807  ixpf 4340  tz9.12lem3 4633  aceq6a 4713  kmlem12 4748  brdom6disj 4777  arch 6018  cvg2 6859  caure 6864  cauim 6865  fsum1 6943  clm4 7018  climcmplem 7073  iserzcmp0 7079  climabslem 7084  cvgcmp3c 7122  reccnv 7153  expcnvlem1 7162  lmfexlem3 7893  ubthlem5 8464  hlimunii 9029  spanun 9382  lnopunilem1 9850

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

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

Copyright terms: Public domain