Theorem mpjao3dan 1289

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 787	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 964	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 121	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 788	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698   \/ w3o 962

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

This theorem depends on definitions:  df-bi 116  df-3or 964

This theorem is referenced by:  wetriext  4536  nntri3  6444  nntri2or2  6445  nntr2  6450  tridc  6844  nnnninfeq  7071  exmidontriimlem2  7157  caucvgprlemnkj  7586  caucvgprlemnbj  7587  caucvgprprlemnkj  7612  caucvgprprlemnbj  7613  caucvgsr  7722  npnflt  9719  nmnfgt  9722  xleadd1a  9777  xltadd1  9780  xlt2add  9784  xsubge0  9785  xleaddadd  9791  addmodlteq  10297  iseqf1olemkle  10383  hashfiv01gt1  10656  xrmaxltsup  11155  xrmaxadd  11158  xrbdtri  11173  cvgratz  11429  zdvdsdc  11707  divalglemeunn  11811  divalglemex  11812  divalglemeuneg  11813  divalg  11814  znege1  12052  ennnfonelemk  12129  isxmet2d  12748  trilpolemres  13613  trirec0  13615