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

Theorem ralimdv2 2786
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 1631 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  B  ->  ch ) ) )
3 df-ral 2710 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2710 . 2  |-  ( A. x  e.  B  ch  <->  A. x ( x  e.  B  ->  ch )
)
52, 3, 43imtr4g 262 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    e. wcel 1725   A.wral 2705
This theorem is referenced by:  ssralv  3407  zorn2lem7  8382  pwfseqlem3  8535  sup2  9964  xrsupexmnf  10883  xrinfmexpnf  10884  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  r19.29uz  12154  rexuzre  12156  caurcvg  12470  caucvg  12472  isprm5  13112  mrissmrid  13866  elcls3  17147  iscnp4  17327  cncls2  17337  cnntr  17339  2ndcsep  17522  dyadmbllem  19491  xrlimcnp  20807  pntlem3  21303  sigaclfu2  24504  climrec  27705  mapdordlem2  32435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ral 2710
  Copyright terms: Public domain W3C validator