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

Theorem mp3and 1461
 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 1125 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  eqsupd  8908  eqinfd  8936  updjud  9350  mreexexlemd  16910  mhmlem  18215  nn0gsumfz  19101  mdetunilem3  21229  mdetunilem9  21235  axtgupdim2  26275  axtgeucl  26276  wwlksnextprop  27708  measdivcst  31608  noprefixmo  33330  btwnouttr2  33611  btwnexch2  33612  cgrsub  33634  btwnconn1lem2  33677  btwnconn1lem5  33680  btwnconn1lem6  33681  segcon2  33694  btwnoutside  33714  broutsideof3  33715  outsideoftr  33718  outsideofeq  33719  lineelsb2  33737  relowlssretop  34799  lshpkrlem6  36430  reladdrsub  39566  fmuldfeq  42268  stoweidlem5  42690  el0ldep  44916  ldepspr  44923
 Copyright terms: Public domain W3C validator