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

Theorem mp3and 1575
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 1122 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  eqsupd  8523  eqinfd  8551  updjud  8964  mreexexlemd  16512  mhmlem  17743  nn0gsumfz  18587  mdetunilem3  20638  mdetunilem9  20644  axtgeucl  25592  wwlksnextprop  27057  measdivcst  30628  noprefixmo  32185  btwnouttr2  32466  btwnexch2  32467  cgrsub  32489  btwnconn1lem2  32532  btwnconn1lem5  32535  btwnconn1lem6  32536  segcon2  32549  btwnoutside  32569  broutsideof3  32570  outsideoftr  32573  outsideofeq  32574  lineelsb2  32592  relowlssretop  33547  lshpkrlem6  34922  fmuldfeq  40328  stoweidlem5  40734  el0ldep  42778  ldepspr  42785
  Copyright terms: Public domain W3C validator