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

Theorem mp3and 1443
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 1108 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  eqsupd  8716  eqinfd  8744  updjud  9157  mreexexlemd  16773  mhmlem  18006  nn0gsumfz  18854  mdetunilem3  20927  mdetunilem9  20933  axtgupdim2  25959  axtgeucl  25960  wwlksnextprop  27415  wwlksnextpropOLD  27416  measdivcst  31126  noprefixmo  32720  btwnouttr2  33001  btwnexch2  33002  cgrsub  33024  btwnconn1lem2  33067  btwnconn1lem5  33070  btwnconn1lem6  33071  segcon2  33084  btwnoutside  33104  broutsideof3  33105  outsideoftr  33108  outsideofeq  33109  lineelsb2  33127  relowlssretop  34083  lshpkrlem6  35693  reladdrsub  38645  fmuldfeq  41293  stoweidlem5  41719  el0ldep  43886  ldepspr  43893
  Copyright terms: Public domain W3C validator