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  moimv  2164  ralimdv2  2594  mo2icl  2895  sstr2  3128  reuss2  3390  ssuni  3790  disjss2  3936  disjss1  3939  disjiun  3953  disjss3  3962  frss  4297  alxfr  4484  dfwe2  4510  ordom  4602  ssrel  4729  ssrelrel  4740  fv2  5419  dff3  5572  iotaval  6201  findcard3  7033  dffi2  7109  indcardi  7601  zorn2lem4  8059  uzindi  10974  caubnd  11772  ramtlecl  12974  dfcon2  17072  2ndcdisj  17109  wilthlem3  20235  onsuct0  24220  domrngref  24391  bwt2  24924  pgapspf2  25385  psgnunilem4  26752  ax10ext  26938
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