Theorem r19.20i2 1679

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 968	. 2 |- (A.x(x e. A -> ph) -> A.x(x e. B -> ps))
3		df-ral 1625	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4		df-ral 1625	. 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 950   e. wcel 1105  A.wral 1621

This theorem is referenced by:  r19.20i 1680  ralcom3 1753  tfi 3089  omex 4551  kmlem1 4689  brdom5 4726  brdom4 4727  xrub 5978  seqzeq 6438  cau5i 6805  iserzshft2 6995  clim2serzt 7021  iserzmulc1 7023  isum1p 7092  isumreclt 7096  isummulc1ALT 7099  fsum0diaglem2 7143  basgen2t 7532  sumdmd 10468  dmdbr6at 10470

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

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

Copyright terms: Public domain