Theorem mpjao3dan 1343

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 715   \/ w3o 1003

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 716

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

This theorem is referenced by:  wetriext  4675  nntri3  6665  nntri2or2  6666  nntr2  6671  tridc  7089  nnnninfeq  7327  exmidontriimlem2  7437  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprprlemnkj  7912  caucvgprprlemnbj  7913  caucvgsr  8022  npnflt  10050  nmnfgt  10053  xleadd1a  10108  xltadd1  10111  xlt2add  10115  xsubge0  10116  xleaddadd  10122  addmodlteq  10661  iseqf1olemkle  10760  hashfiv01gt1  11045  iswrdiz  11124  xrmaxltsup  11836  xrmaxadd  11839  xrbdtri  11854  cvgratz  12111  zdvdsdc  12391  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  divalg  12503  znege1  12768  ennnfonelemk  13039  isxmet2d  15091  trilpolemres  16697  trirec0  16699