Theorem mpjao3dan 1318

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 709   \/ w3o 979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117  df-3or 981

This theorem is referenced by:  wetriext  4614  nntri3  6564  nntri2or2  6565  nntr2  6570  tridc  6969  nnnninfeq  7203  exmidontriimlem2  7305  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprprlemnkj  7776  caucvgprprlemnbj  7777  caucvgsr  7886  npnflt  9907  nmnfgt  9910  xleadd1a  9965  xltadd1  9968  xlt2add  9972  xsubge0  9973  xleaddadd  9979  addmodlteq  10507  iseqf1olemkle  10606  hashfiv01gt1  10891  iswrdiz  10959  xrmaxltsup  11440  xrmaxadd  11443  xrbdtri  11458  cvgratz  11714  zdvdsdc  11994  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  divalg  12106  znege1  12371  ennnfonelemk  12642  isxmet2d  14668  trilpolemres  15773  trirec0  15775