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

Theorem mp3and 1283
 Description: A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
Hypotheses
Ref Expression
mp3and.1
mp3and.2
mp3and.3
mp3and.4
Assertion
Ref Expression
mp3and

Proof of Theorem mp3and
StepHypRef Expression
1 mp3and.1 . . 3
2 mp3and.2 . . 3
3 mp3and.3 . . 3
41, 2, 33jca 1135 . 2
5 mp3and.4 . 2
64, 5mpd 15 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 937 This theorem is referenced by:  eqsupd  7491  mreexexlemd  13900  measdivcst  24610  btwnouttr2  25987  btwnexch2  25988  cgrsub  26010  btwnconn1lem2  26053  btwnconn1lem5  26056  btwnconn1lem6  26057  segcon2  26070  btwnoutside  26090  broutsideof3  26091  outsideoftr  26094  outsideofeq  26095  lineelsb2  26113  fmuldfeq  27727  stoweidlem5  27768  lshpkrlem6  30011 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 179  df-an 362  df-3an 939
 Copyright terms: Public domain W3C validator