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

Theorem ralimdv2 2796
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 1675 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  B  ->  ch ) ) )
3 df-ral 2720 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2720 . 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 1367    e. wcel 1756   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ral 2720
This theorem is referenced by:  ssralv  3416  zorn2lem7  8671  pwfseqlem3  8827  sup2  10286  xrsupexmnf  11267  xrinfmexpnf  11268  xrsupsslem  11269  xrinfmsslem  11270  xrub  11274  r19.29uz  12838  rexuzre  12840  caurcvg  13154  caucvg  13156  isprm5  13798  mrissmrid  14579  elcls3  18687  iscnp4  18867  cncls2  18877  cnntr  18879  2ndcsep  19063  dyadmbllem  21079  xrlimcnp  22362  pntlem3  22858  sigaclfu2  26564  climrec  29776  mapdordlem2  35282
  Copyright terms: Public domain W3C validator