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

Theorem mpjao3dan 1411
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 940 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1069 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 210 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 941 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wo 833  w3o 1067
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 199  df-an 388  df-or 834  df-3or 1069
This theorem is referenced by:  wemaplem2  8808  r1val1  9011  xleadd1a  12465  xlt2add  12472  xmullem  12476  xmulgt0  12495  xmulasslem3  12498  xlemul1a  12500  xadddilem  12506  xadddi  12507  xadddi2  12509  isxmet2d  22643  icccvx  23260  ivthicc  23765  mbfmulc2lem  23954  c1lip1  24300  dvivth  24313  reeff1o  24741  coseq00topi  24794  tanabsge  24798  logcnlem3  24931  atantan  25205  atanbnd  25208  cvxcl  25267  ostthlem1  25908  iscgrglt  26005  tgdim01ln  26055  lnxfr  26057  lnext  26058  tgfscgr  26059  tglineeltr  26122  colmid  26179  prodtp  30292  xrpxdivcld  30360  s3f1  30368  cyc3co2  30460  archirngz  30484  archiabllem1b  30487  esumcst  30966  sgnmulsgn  31453  sgnmulsgp  31454  hgt750lemb  31575  fnwe2lem3  39048
  Copyright terms: Public domain W3C validator