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  21111  vcsubdir  21112  vc0  21125  vcm  21127  vcnegneg  21130  vcnegsubdi2  21131  vcsub4  21132  nvaddsub4  21219  nvnncan  21221  nvpi  21232  nvge0  21240  ipval3  21282  ipidsq  21286  lnoadd  21336  lnosub  21337  dipsubdir  21426
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