Theorem mpjao3dan 1295

Description: Eliminate a 3-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

Step	Hyp	Ref	Expression
1		mpjao3dan.1	. . 3
2		mpjao3dan.2	. . 3
3	1, 2	jaodan 785	. 2
4		mpjao3dan.3	. 2
5		mpjao3dan.4	. . 3
6		df-3or 974	. . 3
7	5, 6	sylib 196	. 2
8	3, 4, 7	mpjaodan 786	1

Syntax hints:  ->wi 4  \/wo 368  /\wa 369  \/w3o 972

This theorem is referenced by:  wemaplem2  7993  r1val1  8225  xleadd1a  11474  xlt2add  11481  xmullem  11485  xmulgt0  11504  xmulasslem3  11507  xlemul1a  11509  xadddilem  11515  xadddi  11516  xadddi2  11518  isxmet2d  20830  icccvx  21450  ivthicc  21870  mbfmulc2lem  22054  c1lip1  22398  dvivth  22411  reeff1o  22842  coseq00topi  22895  tanabsge  22899  logcnlem3  23025  atantan  23254  atanbnd  23257  cvxcl  23314  ostthlem1  23812  tgdim01ln  23951  lnxfr  23953  lnext  23954  tgfscgr  23955  tglineeltr  24011  colmid  24065  xrpxdivcld  27631  archirngz  27733  archiabllem1b  27736  esumcst  28071  sgnmulsgn  28488  sgnmulsgp  28489  fnwe2lem3  30998

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 185  df-or 370  df-an 371  df-3or 974