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

Theorem mp3and 1329
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 1177 . 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 974
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 369  df-3an 976
This theorem is referenced by:  eqsupd  7950  mreexexlemd  15258  mhmlem  16514  nn0gsumfz  17332  mdetunilem3  19408  mdetunilem9  19414  axtgeucl  24248  wwlkextprop  25161  measdivcst  28673  btwnouttr2  30360  btwnexch2  30361  cgrsub  30383  btwnconn1lem2  30426  btwnconn1lem5  30429  btwnconn1lem6  30430  segcon2  30443  btwnoutside  30463  broutsideof3  30464  outsideoftr  30467  outsideofeq  30468  lineelsb2  30486  relowlssretop  31280  lshpkrlem6  32133  fmuldfeq  36945  stoweidlem5  37155  el0ldep  38578  ldepspr  38585
  Copyright terms: Public domain W3C validator