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  10217  nmnfgt  10220  xleadd1a  10275  xltadd1  10278  xlt2add  10282  xsubge0  10283  xleaddadd  10289  addmodlteq  10835  iseqf1olemkle  10934  hashfiv01gt1  11221  iswrdiz  11311  xrmaxltsup  12024  xrmaxadd  12027  xrbdtri  12042  cvgratz  12299  zdvdsdc  12579  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  divalg  12691  znege1  12956  ennnfonelemk  13291  isxmet2d  15449  trilpolemres  17091  trirec0  17093