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

Theorem mpjao3dan 1392
 Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
Hypotheses
Ref Expression
mpjao3dan.1 ((𝜑𝜓) → 𝜒)
mpjao3dan.2 ((𝜑𝜃) → 𝜒)
mpjao3dan.3 ((𝜑𝜏) → 𝜒)
mpjao3dan.4 (𝜑 → (𝜓𝜃𝜏))
Assertion
Ref Expression
mpjao3dan (𝜑𝜒)

Proof of Theorem mpjao3dan
StepHypRef Expression
1 mpjao3dan.1 . . 3 ((𝜑𝜓) → 𝜒)
2 mpjao3dan.2 . . 3 ((𝜑𝜃) → 𝜒)
31, 2jaodan 825 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1037 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 208 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 826 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   ∨ w3o 1035 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-or 385  df-an 386  df-3or 1037 This theorem is referenced by:  wemaplem2  8397  r1val1  8594  xleadd1a  12023  xlt2add  12030  xmullem  12034  xmulgt0  12053  xmulasslem3  12056  xlemul1a  12058  xadddilem  12064  xadddi  12065  xadddi2  12067  isxmet2d  22037  icccvx  22652  ivthicc  23129  mbfmulc2lem  23315  c1lip1  23659  dvivth  23672  reeff1o  24100  coseq00topi  24153  tanabsge  24157  logcnlem3  24285  atantan  24545  atanbnd  24548  cvxcl  24606  ostthlem1  25211  iscgrglt  25304  tgdim01ln  25354  lnxfr  25356  lnext  25357  tgfscgr  25358  tglineeltr  25421  colmid  25478  xrpxdivcld  29420  archirngz  29520  archiabllem1b  29523  esumcst  29898  sgnmulsgn  30384  sgnmulsgp  30385  fnwe2lem3  37069
 Copyright terms: Public domain W3C validator