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

Theorem mp3and 1317
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 1168 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 mp3and.4 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
64, 5mpd 15 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 371  df-3an 967
This theorem is referenced by:  eqsupd  7728  mreexexlemd  14603  mdetunilem3  18442  mdetunilem9  18448  measdivcst  26661  btwnouttr2  28075  btwnexch2  28076  cgrsub  28098  btwnconn1lem2  28141  btwnconn1lem5  28144  btwnconn1lem6  28145  segcon2  28158  btwnoutside  28178  broutsideof3  28179  outsideoftr  28182  outsideofeq  28183  lineelsb2  28201  fmuldfeq  29790  stoweidlem5  29826  wwlkextprop  30589  nn0gsumfz  30837  el0ldep  30997  ldepspr  31004  lshpkrlem6  32856
  Copyright terms: Public domain W3C validator