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

Theorem alimdv 1608
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 1604 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2alimdh 1551 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1528
This theorem is referenced by:  2alimdv  1610  ax16i  1943  ax16  1991  morimv  2193  ralimdv2  2625  mo2icl  2946  sstr2  3188  reuss2  3450  ssuni  3851  disjss2  3998  disjss1  4001  disjiun  4015  disjss3  4024  frss  4360  alxfr  4547  dfwe2  4573  ordom  4665  ssrel  4776  ssrelrel  4787  fv2  5482  dff3  5635  iotaval  6264  findcard3  7096  dffi2  7172  indcardi  7664  zorn2lem4  8122  uzindi  11038  caubnd  11837  ramtlecl  13042  dfcon2  17140  wilthlem3  20303  onsuct0  24288  domrngref  24459  bwt2  24992  pgapspf2  25453  psgnunilem4  26820  ax10ext  27006
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604
  Copyright terms: Public domain W3C validator