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

Theorem alimd 1780
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 1778 . 2  |-  ( ph  ->  A. x ph )
3 alimd.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3alimdh 1572 1  |-  ( ph  ->  ( A. x ps 
->  A. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549   F/wnf 1553
This theorem is referenced by:  alrimdd  1784  nfimdOLD  1828  spimtOLD  1956  sbiedOLD  2124  sb9i  2169  mo  2302  2mo  2358  ralimdaa  2775  axpowndlem3  8463  axext4dist  25412  pm11.71  27511  spimtNEW7  29361  sbiedNEW7  29392  sb9iOLD7  29597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator