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

Theorem mpii 41
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 11 . 2  |-  ( ps 
->  ch )
3 mpii.2 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpdi 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equveliOLD  2082  intmin  4062  dfiin2g  4116  ssorduni  4758  suceloni  4785  tfrlem1  6628  lubid  14431  irredmul  15806  opnneiid  17182  isufil2  17932  mdbr3  23792  mdbr4  23793  dmdbr5  23803  filnetlem4  26391  equveliNEW7  29455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator