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  4724  nntri3  6770  nntri2or2  6771  nntr2  6776  tridc  7204  nnnninfeq  7468  exmidontriimlem2  7578  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprprlemnkj  8059  caucvgprprlemnbj  8060  caucvgsr  8169  npnflt  10227  nmnfgt  10230  xleadd1a  10285  xltadd1  10288  xlt2add  10292  xsubge0  10293  xleaddadd  10299  addmodlteq  10848  iseqf1olemkle  10947  hashfiv01gt1  11235  iswrdiz  11325  xrmaxltsup  12040  xrmaxadd  12043  xrbdtri  12058  cvgratz  12315  zdvdsdc  12595  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  divalg  12707  znege1  12974  ennnfonelemk  13340  isxmet2d  15498  trilpolemres  17189  trirec0  17191