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  6557  nntri2or2  6558  nntr2  6563  tridc  6962  nnnninfeq  7196  exmidontriimlem2  7292  caucvgprlemnkj  7736  caucvgprlemnbj  7737  caucvgprprlemnkj  7762  caucvgprprlemnbj  7763  caucvgsr  7872  npnflt  9893  nmnfgt  9896  xleadd1a  9951  xltadd1  9954  xlt2add  9958  xsubge0  9959  xleaddadd  9965  addmodlteq  10493  iseqf1olemkle  10592  hashfiv01gt1  10877  iswrdiz  10945  xrmaxltsup  11426  xrmaxadd  11429  xrbdtri  11444  cvgratz  11700  zdvdsdc  11980  divalglemeunn  12089  divalglemex  12090  divalglemeuneg  12091  divalg  12092  znege1  12357  ennnfonelemk  12628  isxmet2d  14610  trilpolemres  15715  trirec0  15717