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

Theorem ralimdv2 2636
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 1611 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  B  ->  ch ) ) )
3 df-ral 2561 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2561 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43imtr4g 261 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ssralv  3250  zorn2lem7  8145  pwfseqlem3  8298  sup2  9726  xrsupexmnf  10639  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  r19.29uz  11850  rexuzre  11852  caurcvg  12165  caucvg  12167  isprm5  12807  mrissmrid  13559  elcls3  16836  cncls2  17018  cnntr  17020  2ndcsep  17201  dyadmbllem  18970  xrlimcnp  20279  pntlem3  20774  iscnp4  25666  bsstrs  26249  nbssntrs  26250  climrec  27832  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator