Theorem mpjao3dan 1319

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 709   \/ w3o 979

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 710

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

This theorem is referenced by:  wetriext  4624  nntri3  6582  nntri2or2  6583  nntr2  6588  tridc  6995  nnnninfeq  7229  exmidontriimlem2  7333  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprprlemnkj  7804  caucvgprprlemnbj  7805  caucvgsr  7914  npnflt  9936  nmnfgt  9939  xleadd1a  9994  xltadd1  9997  xlt2add  10001  xsubge0  10002  xleaddadd  10008  addmodlteq  10541  iseqf1olemkle  10640  hashfiv01gt1  10925  iswrdiz  10999  xrmaxltsup  11540  xrmaxadd  11543  xrbdtri  11558  cvgratz  11814  zdvdsdc  12094  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  divalg  12206  znege1  12471  ennnfonelemk  12742  isxmet2d  14791  trilpolemres  15943  trirec0  15945