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  6775  nntri2or2  6776  nntr2  6781  tridc  7210  nnnninfeq  7474  exmidontriimlem2  7584  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprprlemnkj  8065  caucvgprprlemnbj  8066  caucvgsr  8175  npnflt  10233  nmnfgt  10236  xleadd1a  10291  xltadd1  10294  xlt2add  10298  xsubge0  10299  xleaddadd  10305  addmodlteq  10855  iseqf1olemkle  10954  hashfiv01gt1  11242  iswrdiz  11332  xrmaxltsup  12048  xrmaxadd  12051  xrbdtri  12066  cvgratz  12323  zdvdsdc  12603  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  divalg  12715  znege1  12982  ennnfonelemk  13348  isxmet2d  15591  trilpolemres  17315  trirec0  17317