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

Theorem alimdv 1676
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-5 1671 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1609 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem is referenced by:  2alimdv  1678  axc9lem1  1954  axc16i  2021  morimvOLD  2329  ralimdv2  2898  mo2icl  3238  sstr2  3464  reuss2  3731  ssuni  4214  disjss2  4366  disjss1  4369  disjiun  4383  disjss3  4392  alxfr  4606  frss  4788  ssrel  5029  ssrel2  5031  ssrelrel  5041  iotaval  5493  dff3  5958  dfwe2  6496  ordom  6588  findcard3  7659  dffi2  7777  indcardi  8315  zorn2lem4  8772  uzindi  11913  caubnd  12957  ramtlecl  14172  psgnunilem4  16114  bwthOLD  19139  dfcon2  19148  wilthlem3  22534  nbcusgra  23516  disjss1f  26062  wzel  27898  onsuct0  28424  axc11next  29801
  Copyright terms: Public domain W3C validator