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

Theorem mp3and 1282
Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
Hypotheses
Ref Expression
mp3and.1  |-  ( ph  ->  ps )
mp3and.2  |-  ( ph  ->  ch )
mp3and.3  |-  ( ph  ->  th )
mp3and.4  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
Assertion
Ref Expression
mp3and  |-  ( ph  ->  ta )

Proof of Theorem mp3and
StepHypRef Expression
1 mp3and.1 . . 3  |-  ( ph  ->  ps )
2 mp3and.2 . . 3  |-  ( ph  ->  ch )
3 mp3and.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1134 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 mp3and.4 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
64, 5mpd 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  eqsupd  7426  mreexexlemd  13832  measdivcst  24540  btwnouttr2  25868  btwnexch2  25869  cgrsub  25891  btwnconn1lem2  25934  btwnconn1lem5  25937  btwnconn1lem6  25938  segcon2  25951  btwnoutside  25971  broutsideof3  25972  outsideoftr  25975  outsideofeq  25976  lineelsb2  25994  fmuldfeq  27588  stoweidlem5  27629  lshpkrlem6  29610
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