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

Theorem mp3and 1419
 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 1235 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  eqsupd  8246  eqinfd  8274  mreexexlemd  16127  mhmlem  17358  nn0gsumfz  18203  mdetunilem3  20239  mdetunilem9  20245  axtgeucl  25171  wwlkextprop  26272  measdivcst  29615  btwnouttr2  31299  btwnexch2  31300  cgrsub  31322  btwnconn1lem2  31365  btwnconn1lem5  31368  btwnconn1lem6  31369  segcon2  31382  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsideofeq  31407  lineelsb2  31425  relowlssretop  32387  lshpkrlem6  33420  fmuldfeq  38650  stoweidlem5  38898  wwlksnextprop  41118  el0ldep  42049  ldepspr  42056
 Copyright terms: Public domain W3C validator