Theorem ralimdv2 2961

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)

Hypothesis

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

Assertion

Ref	Expression
ralimdv2	|- ( ph -> ( A. x e. A ps -> A. x e. B ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem ralimdv2

Step	Hyp	Ref	Expression
1		ralimdv2.1	. . 3 |- ( ph -> ( ( x e. A -> ps ) -> ( x e. B -> ch ) ) )
2	1	alimdv 1845	. 2 |- ( ph -> ( A. x ( x e. A -> ps ) -> A. x ( x e. B -> ch ) ) )
3		df-ral 2917	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4		df-ral 2917	. 2 |- ( A. x e. B ch <-> A. x ( x e. B -> ch ) )
5	2, 3, 4	3imtr4g 285	1 |- ( ph -> ( A. x e. A ps -> A. x e. B ch ) )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralimdva  2962  ssralv  3666  zorn2lem7  9324  pwfseqlem3  9482  sup2  10979  xrsupexmnf  12135  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  r19.29uz  14090  rexuzre  14092  caurcvg  14407  caucvg  14409  isprm5  15419  prmgaplem5  15759  prmgaplem6  15760  mrissmrid  16301  elcls3  20887  iscnp4  21067  cncls2  21077  cnntr  21079  2ndcsep  21262  dyadmbllem  23367  xrlimcnp  24695  pntlem3  25298  sigaclfu2  30184  mapdordlem2  36926  iunrelexp0  37994  climrec  39835  0ellimcdiv  39881