Theorem r19.20dv2 1687

Description: Inference quantifying both antecedent and consequent.

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.20dv2

Step	Hyp	Ref	Expression
1		r19.20dv2.1	. . 3 |- (ph -> ((x e. A -> ps) -> (x e. B -> ch)))
2	1	19.20dv 1271	. 2 |- (ph -> (A.x(x e. A -> ps) -> A.x(x e. B -> ch)))
3		df-ral 1625	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
4		df-ral 1625	. 2 |- (A.x e. B ch <-> A.x(x e. B -> ch))
5	2, 3, 4	3imtr4g 551	1 |- (ph -> (A.x e. A ps -> A.x e. B ch))

Syntax hints:   -> wi 3  A.wal 950   e. wcel 1105  A.wral 1621

This theorem is referenced by:  ssralv 2085  xrsupexmnf 5972  xrinfmexpnf 5973  xrsupsslem 5974  xrinfmsslem 5975  xrub 5978  fsequb 6406  seqzfveq 6437  fsump1s 6902  fsumcllem 6903  fsum1ps 6907  fsumsplit 6909  fsumadd 6911  fsumcom 6917  fsumrev 6918  fsummulc1 6922  fsumcmp 6929  fsumcmpndx2 6931  fsumabs 6932  climconst 6982  clim2serzt 7021  climserzle 7034  isum1p 7092  iserzgt0 7097  fsum0diaglem2 7143  fsum0diag2 7145  fsum0diag3 7146  fsum0diag4 7147  elcls3 7600  metreslem 7710

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  ax-17 1190

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

Copyright terms: Public domain