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  7469  exmidontriimlem2  7579  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprprlemnkj  8060  caucvgprprlemnbj  8061  caucvgsr  8170  npnflt  10228  nmnfgt  10231  xleadd1a  10286  xltadd1  10289  xlt2add  10293  xsubge0  10294  xleaddadd  10300  addmodlteq  10850  iseqf1olemkle  10949  hashfiv01gt1  11237  iswrdiz  11327  xrmaxltsup  12043  xrmaxadd  12046  xrbdtri  12061  cvgratz  12318  zdvdsdc  12598  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  divalg  12710  znege1  12977  ennnfonelemk  13343  isxmet2d  15540  trilpolemres  17258  trirec0  17260