MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpii 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:  equveli  2023  intmin  4012  dfiin2g  4066  ssorduni  4706  suceloni  4733  tfrlem1  6572  lubid  14366  irredmul  15741  opnneiid  17113  isufil2  17861  mdbr3  23648  mdbr4  23649  dmdbr5  23659  filnetlem4  26101  equveliNEW7  28864
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator