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

Theorem alimdv 1607
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 1603 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1550 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  2alimdv  1609  ax16i  1986  ax16ALT2  1988  morimv  2191  ralimdv2  2623  mo2icl  2944  sstr2  3186  reuss2  3448  ssuni  3849  disjss2  3996  disjss1  3999  disjiun  4013  disjss3  4022  frss  4360  alxfr  4547  dfwe2  4573  ordom  4665  ssrel  4776  ssrelrel  4787  iotaval  5230  dff3  5673  findcard3  7100  dffi2  7176  indcardi  7668  zorn2lem4  8126  uzindi  11043  caubnd  11842  ramtlecl  13047  dfcon2  17145  wilthlem3  20308  disjss1f  23351  onsuct0  24880  domrngref  25060  bwt2  25592  pgapspf2  26053  psgnunilem4  27420  ax10ext  27606  nbcusgra  28159  cusgrauvtx  28168
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
  Copyright terms: Public domain W3C validator