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

Theorem mp3and 1363
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 1185 . 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 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  eqsupd  7974  eqinfd  8004  mreexexlemd  15538  mhmlem  16794  nn0gsumfz  17601  mdetunilem3  19626  mdetunilem9  19632  axtgeucl  24507  wwlkextprop  25458  measdivcst  29043  btwnouttr2  30782  btwnexch2  30783  cgrsub  30805  btwnconn1lem2  30848  btwnconn1lem5  30851  btwnconn1lem6  30852  segcon2  30865  btwnoutside  30885  broutsideof3  30886  outsideoftr  30889  outsideofeq  30890  lineelsb2  30908  relowlssretop  31707  lshpkrlem6  32600  fmuldfeq  37481  stoweidlem5  37685  el0ldep  39533  ldepspr  39540
  Copyright terms: Public domain W3C validator