Theorem r19.20i 1704

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

Syntax hints:   -> wi 3   e. wcel 958  A.wral 1645

This theorem is referenced by:  r19.20ia 1705  r19.20si 1706  r19.12 1740  exfo 3822  ixpf 4356  tz9.12lem3 4661  aceq6a 4741  kmlem12 4776  brdom6disj 4805  arch 6071  cvg2 6922  caure 6927  cauim 6928  fsum1 7005  clm4 7080  climcmplem 7137  iserzcmp0 7143  climabslem 7148  cvgcmp3c 7186  reccnv 7218  expcnvlem1 7227  lmfexlem3 7958  ubthlem5 8533  hlimunii 9108  spanun 9467  lnopunilem1 9935

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

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

Copyright terms: Public domain