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

Theorem mpjao3dan 1543
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 948 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1072 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 208 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 949 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wo 826  w3o 1070
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 383  df-or 827  df-3or 1072
This theorem is referenced by:  wemaplem2  8607  r1val1  8812  xleadd1a  12287  xlt2add  12294  xmullem  12298  xmulgt0  12317  xmulasslem3  12320  xlemul1a  12322  xadddilem  12328  xadddi  12329  xadddi2  12331  isxmet2d  22351  icccvx  22968  ivthicc  23445  mbfmulc2lem  23633  c1lip1  23979  dvivth  23992  reeff1o  24420  coseq00topi  24474  tanabsge  24478  logcnlem3  24610  atantan  24870  atanbnd  24873  cvxcl  24931  ostthlem1  25536  iscgrglt  25629  tgdim01ln  25679  lnxfr  25681  lnext  25682  tgfscgr  25683  tglineeltr  25746  colmid  25803  prodtp  29910  xrpxdivcld  29980  archirngz  30080  archiabllem1b  30083  esumcst  30462  sgnmulsgn  30948  sgnmulsgp  30949  hgt750lemb  31071  fnwe2lem3  38144
  Copyright terms: Public domain W3C validator