Theorem mpjao3dan 1348

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 809	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 1010	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 122	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 810	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   \/ wo 720   \/ w3o 1008

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-3or 1010

This theorem is used by:  wetriext  4726  nntri3  6774  nntri2or2  6775  nntr2  6780  tridc  7208  nnnninfeq  7474  exmidontriimlem2  7584  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprprlemnkj  8065  caucvgprprlemnbj  8066  caucvgsr  8175  npnflt  10234  nmnfgt  10237  xleadd1a  10292  xltadd1  10295  xlt2add  10299  xsubge0  10300  xleaddadd  10306  addmodlteq  10856  iseqf1olemkle  10955  hashfiv01gt1  11243  iswrdiz  11333  xrmaxltsup  12049  xrmaxadd  12052  xrbdtri  12067  cvgratz  12324  zdvdsdc  12604  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  divalg  12716  znege1  12983  ennnfonelemk  13349  isxmet2d  15574  trilpolemres  17298  trirec0  17300