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

Theorem mp3and 1467
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 1261 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  eqsupd  8404  eqinfd  8432  mreexexlemd  16351  mhmlem  17582  nn0gsumfz  18426  mdetunilem3  20468  mdetunilem9  20474  axtgeucl  25416  wwlksnextprop  26875  measdivcst  30416  noprefixmo  31973  btwnouttr2  32254  btwnexch2  32255  cgrsub  32277  btwnconn1lem2  32320  btwnconn1lem5  32323  btwnconn1lem6  32324  segcon2  32337  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  outsideofeq  32362  lineelsb2  32380  relowlssretop  33341  lshpkrlem6  34720  fmuldfeq  40133  stoweidlem5  40540  el0ldep  42580  ldepspr  42587
  Copyright terms: Public domain W3C validator