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

Theorem mp3anr1 1276
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 440 . . 3  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ph )  ->  ta )
41, 3mp3anl1 1273 . 2  |-  ( ( ( ch  /\  th )  /\  ph )  ->  ta )
54ancoms 440 1  |-  ( (
ph  /\  ( ch  /\ 
th ) )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  vc2  21882  vcsubdir  21883  vc0  21896  vcm  21898  vcnegneg  21901  vcnegsubdi2  21902  vcsub4  21903  nvaddsub4  21990  nvnncan  21992  nvpi  22003  nvge0  22011  ipval3  22053  ipidsq  22057  lnoadd  22107  lnosub  22108  dipsubdir  22197
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator