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

Theorem mp3and 1424
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 1240 . 2 (𝜑 → (𝜓𝜒𝜃))
5 mp3and.4 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
64, 5mpd 15 1 (𝜑𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  eqsupd  8307  eqinfd  8335  mreexexlemd  16225  mhmlem  17456  nn0gsumfz  18301  mdetunilem3  20339  mdetunilem9  20345  axtgeucl  25271  wwlksnextprop  26676  measdivcst  30066  btwnouttr2  31768  btwnexch2  31769  cgrsub  31791  btwnconn1lem2  31834  btwnconn1lem5  31837  btwnconn1lem6  31838  segcon2  31851  btwnoutside  31871  broutsideof3  31872  outsideoftr  31875  outsideofeq  31876  lineelsb2  31894  relowlssretop  32840  lshpkrlem6  33879  fmuldfeq  39216  stoweidlem5  39526  el0ldep  41540  ldepspr  41547
  Copyright terms: Public domain W3C validator