Theorem r19.20dv2 1714

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 1291	. 2 |- (ph -> (A.x(x e. A -> ps) -> A.x(x e. B -> ch)))
3		df-ral 1652	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
4		df-ral 1652	. 2 |- (A.x e. B ch <-> A.x(x e. B -> ch))
5	2, 3, 4	3imtr4g 555	1 |- (ph -> (A.x e. A ps -> A.x e. B ch))

Syntax hints:   -> wi 3  A.wal 956   e. wcel 960  A.wral 1648

This theorem is referenced by:  ssralv 2117  xrsupexmnf 6076  xrinfmexpnf 6077  xrsupsslem 6078  xrinfmsslem 6079  xrub 6082  fsequb 6524  seqzfveq 6555  fsump1s 7013  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  climconst 7094  clim2serzt 7134  climserzle 7147  isum1p 7206  iserzgt0 7211  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag3 7260  fsum0diag4 7261  elcls3 7708  metreslem 7819

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

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

Copyright terms: Public domain