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

Theorem alimd 1705
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alimd.1  |-  F/ x ph
alimd.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
alimd  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)

Proof of Theorem alimd
StepHypRef Expression
1 alimd.1 . . 3  |-  F/ x ph
21nfri 1703 . 2  |-  ( ph  ->  A. x ph )
3 alimd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3alimdh 1551 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532   F/wnf 1539
This theorem is referenced by:  alrimdd  1709  nfimd  1727  a4imt  1866  sbied  1908  ax16  1925  sb9i  1988  ax16i  1994  alimdv  2017  mo  2135  2mo  2191  ralimdaa  2582  axpowndlem3  8101  axext4dist  23325  pm11.71  26762
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-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator