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

Theorem mp3anr1 1323
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 451 . . 3  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ph )  ->  ta )
41, 3mp3anl1 1320 . 2  |-  ( ( ( ch  /\  th )  /\  ph )  ->  ta )
54ancoms 451 1  |-  ( (
ph  /\  ( ch  /\ 
th ) )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  vc2  25862  vcsubdir  25863  vc0  25876  vcm  25878  vcnegneg  25881  vcnegsubdi2  25882  vcsub4  25883  nvaddsub4  25970  nvnncan  25972  nvpi  25983  nvge0  25991  ipval3  26033  ipidsq  26037  lnoadd  26087  lnosub  26088  dipsubdir  26177
  Copyright terms: Public domain W3C validator