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

Theorem ralimdv2 2808
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 1728 . 2  |-  ( ph  ->  ( A. x ( x  e.  A  ->  ps )  ->  A. x
( x  e.  B  ->  ch ) ) )
3 df-ral 2756 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
4 df-ral 2756 . 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 1401    e. wcel 1840   A.wral 2751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723
This theorem depends on definitions:  df-bi 185  df-ral 2756
This theorem is referenced by:  ralimdva  2809  ssralv  3500  zorn2lem7  8832  pwfseqlem3  8986  sup2  10457  xrsupexmnf  11465  xrinfmexpnf  11466  xrsupsslem  11467  xrinfmsslem  11468  xrub  11472  r19.29uz  13237  rexuzre  13239  caurcvg  13553  caucvg  13555  isprm5  14352  mrissmrid  15145  elcls3  19767  iscnp4  19947  cncls2  19957  cnntr  19959  2ndcsep  20142  dyadmbllem  22190  xrlimcnp  23514  pntlem3  24065  sigaclfu2  28450  mapdordlem2  34621  iunrelexp0  35645  climrec  36944  0ellimcdiv  36990
  Copyright terms: Public domain W3C validator