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

Theorem mp3and 1322
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 1171 . 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 968
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 970
This theorem is referenced by:  eqsupd  7908  mreexexlemd  14890  nn0gsumfz  16798  mdetunilem3  18878  mdetunilem9  18884  wwlkextprop  24408  measdivcst  27824  btwnouttr2  29237  btwnexch2  29238  cgrsub  29260  btwnconn1lem2  29303  btwnconn1lem5  29306  btwnconn1lem6  29307  segcon2  29320  btwnoutside  29340  broutsideof3  29341  outsideoftr  29344  outsideofeq  29345  lineelsb2  29363  fmuldfeq  31090  stoweidlem5  31262  el0ldep  32017  ldepspr  32024  lshpkrlem6  33789
  Copyright terms: Public domain W3C validator