Theorem mpjao3dan 1395

Description: Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)

Hypotheses

Ref	Expression
mpjao3dan.1	|- ( ( ph /\ ps ) -> ch )
mpjao3dan.2	|- ( ( ph /\ th ) -> ch )
mpjao3dan.3	|- ( ( ph /\ ta ) -> ch )
mpjao3dan.4	|- ( ph -> ( ps \/ th \/ ta ) )

Assertion

Ref	Expression
mpjao3dan	|- ( ph -> ch )

Proof of Theorem mpjao3dan

Step	Hyp	Ref	Expression
1		mpjao3dan.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2		mpjao3dan.2	. . 3 |- ( ( ph /\ th ) -> ch )
3	1, 2	jaodan 826	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 1038	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 208	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 827	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   \/ w3o 1036

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-or 385  df-an 386  df-3or 1038

This theorem is referenced by:  wemaplem2  8452  r1val1  8649  xleadd1a  12083  xlt2add  12090  xmullem  12094  xmulgt0  12113  xmulasslem3  12116  xlemul1a  12118  xadddilem  12124  xadddi  12125  xadddi2  12127  isxmet2d  22132  icccvx  22749  ivthicc  23227  mbfmulc2lem  23414  c1lip1  23760  dvivth  23773  reeff1o  24201  coseq00topi  24254  tanabsge  24258  logcnlem3  24390  atantan  24650  atanbnd  24653  cvxcl  24711  ostthlem1  25316  iscgrglt  25409  tgdim01ln  25459  lnxfr  25461  lnext  25462  tgfscgr  25463  tglineeltr  25526  colmid  25583  prodtp  29573  xrpxdivcld  29643  archirngz  29743  archiabllem1b  29746  esumcst  30125  sgnmulsgn  30611  sgnmulsgp  30612  hgt750lemb  30734  fnwe2lem3  37622