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

Theorem mp3and 1280
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 1132 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 mp3and.4 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
64, 5mpd 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  eqsupd  7208  mreexexlemd  13546  btwnouttr2  24645  btwnexch2  24646  cgrsub  24668  btwnconn1lem2  24711  btwnconn1lem5  24714  btwnconn1lem6  24715  segcon2  24728  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsideofeq  24753  lineelsb2  24771  lshpkrlem6  29305
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