Theorem mpjao3dan 1431

Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.)

Hypotheses

Ref	Expression
mpjao3dan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
mpjao3dan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
mpjao3dan.3	⊢ ((𝜑 ∧ 𝜏) → 𝜒)
mpjao3dan.4	⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))

Assertion

Ref	Expression
mpjao3dan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjao3dan

Step	Hyp	Ref	Expression
1		mpjao3dan.4	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))
2		mpjao3dan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		mpjao3dan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4		mpjao3dan.3	. . 3 ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
5	2, 3, 4	3jaodan 1430	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
6	1, 5	mpdan 685	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1086

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 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089

This theorem is referenced by:  wemaplem2  9492  r1val1  9731  xleadd1a  13182  xlt2add  13189  xmullem  13193  xmulgt0  13212  xmulasslem3  13215  xlemul1a  13217  xadddilem  13223  xadddi  13224  xadddi2  13226  isxmet2d  23717  icccvx  24350  ivthicc  24859  mbfmulc2lem  25048  c1lip1  25398  dvivth  25411  reeff1o  25843  coseq00topi  25896  tanabsge  25900  logcnlem3  26036  atantan  26310  atanbnd  26313  cvxcl  26371  ostthlem1  27012  iscgrglt  27519  tgdim01ln  27569  lnxfr  27571  lnext  27572  tgfscgr  27573  tglineeltr  27636  colmid  27693  prodtp  31793  xrpxdivcld  31861  s3f1  31873  cycpmco2  32052  cyc3co2  32059  archirngz  32095  archiabllem1b  32098  esumcst  32751  sgnmulsgn  33238  sgnmulsgp  33239  hgt750lemb  33358  exp11d  40869  fnwe2lem3  41437