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

Theorem alimdv 1611
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
alimdv  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem alimdv
StepHypRef Expression
1 ax-17 1606 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1553 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  2alimdv  1613  ax16i  1999  ax16ALT2  2001  morimv  2204  ralimdv2  2636  mo2icl  2957  sstr2  3199  reuss2  3461  ssuni  3865  disjss2  4012  disjss1  4015  disjiun  4029  disjss3  4038  frss  4376  alxfr  4563  dfwe2  4589  ordom  4681  ssrel  4792  ssrelrel  4803  iotaval  5246  dff3  5689  findcard3  7116  dffi2  7192  indcardi  7684  zorn2lem4  8142  uzindi  11059  caubnd  11858  ramtlecl  13063  dfcon2  17161  wilthlem3  20324  disjss1f  23366  onsuct0  24952  domrngref  25163  bwt2  25695  pgapspf2  26156  psgnunilem4  27523  ax10ext  27709  nbcusgra  28298  cusgrauvtx  28309  ax16iNEW7  29526  ax16ALT2OLD7  29697
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
  Copyright terms: Public domain W3C validator