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

Theorem mp3and 1281
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 1133 . 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 935
This theorem is referenced by:  eqsupd  7355  mreexexlemd  13756  btwnouttr2  25472  btwnexch2  25473  cgrsub  25495  btwnconn1lem2  25538  btwnconn1lem5  25541  btwnconn1lem6  25542  segcon2  25555  btwnoutside  25575  broutsideof3  25576  outsideoftr  25579  outsideofeq  25580  lineelsb2  25598  lshpkrlem6  29364
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 937
  Copyright terms: Public domain W3C validator