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

Theorem mp3anr1 1316
Description: An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
Hypotheses
Ref Expression
mp3anr1.1  |-  ps
mp3anr1.2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Assertion
Ref Expression
mp3anr1  |-  ( (
ph  /\  ( ch  /\ 
th ) )  ->  ta )

Proof of Theorem mp3anr1
StepHypRef Expression
1 mp3anr1.1 . . 3  |-  ps
2 mp3anr1.2 . . . 4  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
32ancoms 453 . . 3  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ph )  ->  ta )
41, 3mp3anl1 1313 . 2  |-  ( ( ( ch  /\  th )  /\  ph )  ->  ta )
54ancoms 453 1  |-  ( (
ph  /\  ( ch  /\ 
th ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970
This theorem is referenced by:  vc2  25110  vcsubdir  25111  vc0  25124  vcm  25126  vcnegneg  25129  vcnegsubdi2  25130  vcsub4  25131  nvaddsub4  25218  nvnncan  25220  nvpi  25231  nvge0  25239  ipval3  25281  ipidsq  25285  lnoadd  25335  lnosub  25336  dipsubdir  25425
  Copyright terms: Public domain W3C validator