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  1941  intmin  3898  dfiin2g  3952  ssorduni  4593  suceloni  4620  tfrlem1  6407  lubid  14132  irredmul  15507  opnneiid  16879  isufil2  17619  mdbr3  22893  mdbr4  22894  dmdbr5  22904  issubcv  25773  filnetlem4  26433  equveliNEW7  29503  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator