MPE Home 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 206  df-an 395  df-3an 1086
This theorem is referenced by:  eqsupd  9493  eqinfd  9521  updjud  9970  mreexexlemd  17652  mhmlem  19052  nn0gsumfz  19978  mdetunilem3  22604  mdetunilem9  22610  axtgupdim2  28395  axtgeucl  28396  wwlksnextprop  29843  measdivcst  34070  btwnouttr2  35859  btwnexch2  35860  cgrsub  35882  btwnconn1lem2  35925  btwnconn1lem5  35928  btwnconn1lem6  35929  segcon2  35942  btwnoutside  35962  broutsideof3  35963  outsideoftr  35966  outsideofeq  35967  lineelsb2  35985  relowlssretop  37083  lshpkrlem6  38826  reladdrsub  42096  onsupuni  42931  omabs2  43035  fmuldfeq  45240  stoweidlem5  45662  el0ldep  47885  ldepspr  47892
  Copyright terms: Public domain W3C validator