Theorem mpjao3dan 1285

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

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 697   \/ w3o 961

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 698

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

This theorem is referenced by:  wetriext  4491  nntri3  6393  nntri2or2  6394  nntr2  6399  tridc  6793  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprprlemnkj  7500  caucvgprprlemnbj  7501  caucvgsr  7610  npnflt  9598  nmnfgt  9601  xleadd1a  9656  xltadd1  9659  xlt2add  9663  xsubge0  9664  xleaddadd  9670  addmodlteq  10171  iseqf1olemkle  10257  hashfiv01gt1  10528  xrmaxltsup  11027  xrmaxadd  11030  xrbdtri  11045  cvgratz  11301  zdvdsdc  11514  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  divalg  11621  znege1  11856  ennnfonelemk  11913  isxmet2d  12517  nninfalllemn  13202  trilpolemres  13235