Theorem r19.20i2 1700

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 990	. 2 |- (A.x(x e. A -> ph) -> A.x(x e. B -> ps))
3		df-ral 1646	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
4		df-ral 1646	. 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 952   e. wcel 956  A.wral 1642

This theorem is referenced by:  r19.20i 1701  ralcom3 1774  tfi 3121  omex 4607  kmlem1 4745  brdom5 4782  brdom4 4783  xrub 6035  seqzeq 6495  cau5i 6862  iserzshft2 7052  clim2serzt 7078  iserzmulc1 7080  isum1p 7149  isumreclt 7153  isummulc1ALT 7156  fsum0diaglem2 7200  basgen2t 7589  sumdmd 10283  dmdbr6at 10285

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

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

Copyright terms: Public domain