MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimdv2 Structured version   Unicode version

Theorem ralimdv2 2794
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
StepHypRef Expression
1 ralimdv2.1 . . 3  |-  ( ph  ->  ( ( x  e.  A  ->  ps )  ->  ( x  e.  B  ->  ch ) ) )
21alimdv 1680 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  B  ->  ch ) ) )
3 df-ral 2718 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2718 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43imtr4g 270 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1362    e. wcel 1761   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-ral 2718
This theorem is referenced by:  ssralv  3413  zorn2lem7  8667  pwfseqlem3  8823  sup2  10282  xrsupexmnf  11263  xrinfmexpnf  11264  xrsupsslem  11265  xrinfmsslem  11266  xrub  11270  r19.29uz  12834  rexuzre  12836  caurcvg  13150  caucvg  13152  isprm5  13794  mrissmrid  14575  elcls3  18646  iscnp4  18826  cncls2  18836  cnntr  18838  2ndcsep  19022  dyadmbllem  21038  xrlimcnp  22321  pntlem3  22817  sigaclfu2  26500  climrec  29701  mapdordlem2  35004
  Copyright terms: Public domain W3C validator