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  4699  nntri3  6730  nntri2or2  6731  nntr2  6736  tridc  7157  nnnninfeq  7419  exmidontriimlem2  7529  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprprlemnkj  8007  caucvgprprlemnbj  8008  caucvgsr  8117  npnflt  10148  nmnfgt  10151  xleadd1a  10206  xltadd1  10209  xlt2add  10213  xsubge0  10214  xleaddadd  10220  addmodlteq  10760  iseqf1olemkle  10859  hashfiv01gt1  11145  iswrdiz  11231  xrmaxltsup  11943  xrmaxadd  11946  xrbdtri  11961  cvgratz  12218  zdvdsdc  12498  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  divalg  12610  znege1  12875  ennnfonelemk  13151  isxmet2d  15213  trilpolemres  16826  trirec0  16828