Theorem mpjao3dan 1341

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 713   \/ w3o 1001

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 714

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

This theorem is referenced by:  wetriext  4673  nntri3  6660  nntri2or2  6661  nntr2  6666  tridc  7082  nnnninfeq  7318  exmidontriimlem2  7427  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprprlemnkj  7902  caucvgprprlemnbj  7903  caucvgsr  8012  npnflt  10040  nmnfgt  10043  xleadd1a  10098  xltadd1  10101  xlt2add  10105  xsubge0  10106  xleaddadd  10112  addmodlteq  10650  iseqf1olemkle  10749  hashfiv01gt1  11034  iswrdiz  11110  xrmaxltsup  11809  xrmaxadd  11812  xrbdtri  11827  cvgratz  12083  zdvdsdc  12363  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  divalg  12475  znege1  12740  ennnfonelemk  13011  isxmet2d  15062  trilpolemres  16582  trirec0  16584