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

Theorem mpii 39
Description: A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.)
Hypotheses
Ref Expression
mpii.1  |-  ch
mpii.2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mpii  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpii
StepHypRef Expression
1 mpii.1 . . 3  |-  ch
21a1i 10 . 2  |-  ( ps 
->  ch )
3 mpii.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdi 38 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equveli  1928  intmin  3882  dfiin2g  3936  ssorduni  4577  suceloni  4604  tfrlem1  6391  lubid  14116  irredmul  15491  opnneiid  16863  isufil2  17603  mdbr3  22877  mdbr4  22878  dmdbr5  22888  issubcv  25670  filnetlem4  26330  a12lem1  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator