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

Theorem alimdv 1631
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-17 1626 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1572 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  2alimdv  1633  ax16i  2130  ax16ALT2  2132  morimv  2328  ralimdv2  2773  mo2icl  3100  sstr2  3342  reuss2  3608  ssuni  4024  disjss2  4172  disjss1  4175  disjiun  4189  disjss3  4198  frss  4536  alxfr  4722  dfwe2  4748  ordom  4840  ssrel  4950  ssrel2  4952  ssrelrel  4962  iotaval  5415  dff3  5868  findcard3  7336  dffi2  7414  indcardi  7906  zorn2lem4  8363  uzindi  11303  caubnd  12145  ramtlecl  13351  bwth  17456  dfcon2  17465  wilthlem3  20836  nbcusgra  21455  disjss1f  23999  onsuct0  26134  psgnunilem4  27330  ax10ext  27516  ax16iNEW7  29301  ax16ALT2OLD7  29473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
  Copyright terms: Public domain W3C validator