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

Theorem mp3anr1 1274
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 439 . . 3  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ph )  ->  ta )
41, 3mp3anl1 1271 . 2  |-  ( ( ( ch  /\  th )  /\  ph )  ->  ta )
54ancoms 439 1  |-  ( (
ph  /\  ( ch  /\ 
th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  vc2  21127  vcsubdir  21128  vc0  21141  vcm  21143  vcnegneg  21146  vcnegsubdi2  21147  vcsub4  21148  nvaddsub4  21235  nvnncan  21237  nvpi  21248  nvge0  21256  ipval3  21298  ipidsq  21302  lnoadd  21352  lnosub  21353  dipsubdir  21442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator