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

Theorem alimdv 2017
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  2019  moimv  2161  ralimdv2  2585  mo2icl  2881  sstr2  3107  reuss2  3355  ssuni  3749  disjss2  3893  disjss1  3896  disjiun  3910  disjss3  3919  frss  4253  alxfr  4438  dfwe2  4464  ordom  4556  ssrel  4683  ssrelrel  4694  fv2  5373  dff3  5525  iotaval  6154  findcard3  6985  dffi2  7060  indcardi  7552  zorn2lem4  8010  uzindi  10921  caubnd  11719  ramtlecl  12921  dfcon2  16977  2ndcdisj  17014  wilthlem3  20140  onsuct0  24054  domrngref  24225  bwt2  24758  pgapspf2  25219  psgnunilem4  26586  ax10ext  26772
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