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 942 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 1072 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 208 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 943 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∨ wo 836   ∨ 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 837  df-3or 1072 This theorem is referenced by:  wemaplem2  8612  r1val1  8817  xleadd1a  12288  xlt2add  12295  xmullem  12299  xmulgt0  12318  xmulasslem3  12321  xlemul1a  12323  xadddilem  12329  xadddi  12330  xadddi2  12332  isxmet2d  22352  icccvx  22969  ivthicc  23446  mbfmulc2lem  23634  c1lip1  23980  dvivth  23993  reeff1o  24421  coseq00topi  24475  tanabsge  24479  logcnlem3  24611  atantan  24871  atanbnd  24874  cvxcl  24932  ostthlem1  25537  iscgrglt  25630  tgdim01ln  25680  lnxfr  25682  lnext  25683  tgfscgr  25684  tglineeltr  25747  colmid  25804  prodtp  29913  xrpxdivcld  29983  archirngz  30083  archiabllem1b  30086  esumcst  30465  sgnmulsgn  30951  sgnmulsgp  30952  hgt750lemb  31074  fnwe2lem3  38148
 Copyright terms: Public domain W3C validator