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

Theorem alimdv 1685
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 1680 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1618 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem is referenced by:  2alimdv  1687  ax12v  1804  axc9lem1  1970  axc16i  2037  morimvOLD  2344  ralimdv2  2871  mo2icl  3282  sstr2  3511  reuss2  3778  ssuni  4267  disjss2  4420  disjss1  4423  disjiun  4437  disjss3  4446  alxfr  4660  frss  4846  ssrel  5089  ssrel2  5091  ssrelrel  5101  iotaval  5560  dff3  6032  dfwe2  6595  ordom  6687  findcard3  7759  dffi2  7879  indcardi  8418  zorn2lem4  8875  uzindi  12055  caubnd  13150  ramtlecl  14373  psgnunilem4  16318  bwthOLD  19677  dfcon2  19686  wilthlem3  23072  nbcusgra  24139  disjss1f  27108  wzel  28957  onsuct0  29483  axc11next  30891
  Copyright terms: Public domain W3C validator