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  1867  sbied  1909  ax16  1926  sb9i  1989  ax16i  1995  alimdv  2018  mo  2140  2mo  2196  ralimdaa  2595  axpowndlem3  8189  axext4dist  23526  pm11.71  26963
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