Theorem mpjao3dan 1348

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 720   \/ w3o 1008

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 721

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

This theorem is referenced by:  wetriext  4719  nntri3  6760  nntri2or2  6761  nntr2  6766  tridc  7194  nnnninfeq  7458  exmidontriimlem2  7568  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprprlemnkj  8049  caucvgprprlemnbj  8050  caucvgsr  8159  npnflt  10196  nmnfgt  10199  xleadd1a  10254  xltadd1  10257  xlt2add  10261  xsubge0  10262  xleaddadd  10268  addmodlteq  10813  iseqf1olemkle  10912  hashfiv01gt1  11199  iswrdiz  11289  xrmaxltsup  12002  xrmaxadd  12005  xrbdtri  12020  cvgratz  12277  zdvdsdc  12557  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  divalg  12669  znege1  12934  ennnfonelemk  13269  isxmet2d  15372  trilpolemres  16996  trirec0  16998