Theorem r19.20i2 1703

Description: Inference quantifying both antecedent and consequent.

Hypothesis

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

Assertion

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

Proof of Theorem r19.20i2

Step	Hyp	Ref	Expression
1		r19.20i2.1	. . 3 |- ((x e. A -> ph) -> (x e. B -> ps))
2	1	19.20i 992	. 2 |- (A.x(x e. A -> ph) -> A.x(x e. B -> ps))
3		df-ral 1649	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4		df-ral 1649	. 2 |- (A.x e. B ps <-> A.x(x e. B -> ps))
5	2, 3, 4	3imtr4 219	1 |- (A.x e. A ph -> A.x e. B ps)

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

This theorem is referenced by:  r19.20i 1704  ralcom3 1777  tfi 3126  omex 4627  kmlem1 4765  brdom5 4802  brdom4 4803  xrub 6080  seqzeq 6555  cau5i 6917  iserzshft2 7107  clim2serzt 7134  iserzmulc1 7136  isum1p 7206  isumreclt 7210  isummulc1ALT 7213  fsum0diaglem2 7257  basgen2t 7639  sumdmd 10347  dmdbr4at 10348  dmdbr6at 10350

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