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

Theorem mpjao3dan 1423
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 951 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1080 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 219 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 952 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 841  w3o 1078
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 208  df-an 397  df-or 842  df-3or 1080
This theorem is referenced by:  wemaplem2  8999  r1val1  9203  xleadd1a  12634  xlt2add  12641  xmullem  12645  xmulgt0  12664  xmulasslem3  12667  xlemul1a  12669  xadddilem  12675  xadddi  12676  xadddi2  12678  isxmet2d  22864  icccvx  23481  ivthicc  23986  mbfmulc2lem  24175  c1lip1  24521  dvivth  24534  reeff1o  24962  coseq00topi  25015  tanabsge  25019  logcnlem3  25154  atantan  25428  atanbnd  25431  cvxcl  25489  ostthlem1  26130  iscgrglt  26227  tgdim01ln  26277  lnxfr  26279  lnext  26280  tgfscgr  26281  tglineeltr  26344  colmid  26401  prodtp  30470  xrpxdivcld  30538  s3f1  30550  cycpmco2  30702  cyc3co2  30709  archirngz  30745  archiabllem1b  30748  esumcst  31221  sgnmulsgn  31706  sgnmulsgp  31707  hgt750lemb  31826  fnwe2lem3  39530
  Copyright terms: Public domain W3C validator