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  7307  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprprlemnkj  7778  caucvgprprlemnbj  7779  caucvgsr  7888  npnflt  9909  nmnfgt  9912  xleadd1a  9967  xltadd1  9970  xlt2add  9974  xsubge0  9975  xleaddadd  9981  addmodlteq  10509  iseqf1olemkle  10608  hashfiv01gt1  10893  iswrdiz  10961  xrmaxltsup  11442  xrmaxadd  11445  xrbdtri  11460  cvgratz  11716  zdvdsdc  11996  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  divalg  12108  znege1  12373  ennnfonelemk  12644  isxmet2d  14692  trilpolemres  15799  trirec0  15801