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

Theorem alimdv 2018
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 nfv 1629 . 2  |-  F/ x ph
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimd 1705 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  2alimdv  2020  morimv  2166  ralimdv2  2598  mo2icl  2919  sstr2  3161  reuss2  3423  ssuni  3823  disjss2  3970  disjss1  3973  disjiun  3987  disjss3  3996  frss  4332  alxfr  4519  dfwe2  4545  ordom  4637  ssrel  4764  ssrelrel  4775  fv2  5454  dff3  5607  iotaval  6236  findcard3  7068  dffi2  7144  indcardi  7636  zorn2lem4  8094  uzindi  11009  caubnd  11807  ramtlecl  13009  dfcon2  17107  wilthlem3  20270  onsuct0  24255  domrngref  24426  bwt2  24959  pgapspf2  25420  psgnunilem4  26787  ax10ext  26973
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator