Theorem mpjao3dan 1344

Description: Eliminate a 3-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 805	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 1006	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 122	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 806	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716   \/ w3o 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117  df-3or 1006

This theorem is referenced by:  wetriext  4701  nntri3  6732  nntri2or2  6733  nntr2  6738  tridc  7159  nnnninfeq  7421  exmidontriimlem2  7531  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprprlemnkj  8009  caucvgprprlemnbj  8010  caucvgsr  8119  npnflt  10151  nmnfgt  10154  xleadd1a  10209  xltadd1  10212  xlt2add  10216  xsubge0  10217  xleaddadd  10223  addmodlteq  10764  iseqf1olemkle  10863  hashfiv01gt1  11149  iswrdiz  11235  xrmaxltsup  11947  xrmaxadd  11950  xrbdtri  11965  cvgratz  12222  zdvdsdc  12502  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  divalg  12614  znege1  12879  ennnfonelemk  13168  isxmet2d  15230  trilpolemres  16843  trirec0  16845