Theorem mpjao3dan 1320

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 710   \/ w3o 980

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 711

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

This theorem is referenced by:  wetriext  4625  nntri3  6583  nntri2or2  6584  nntr2  6589  tridc  6996  nnnninfeq  7230  exmidontriimlem2  7334  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprprlemnkj  7805  caucvgprprlemnbj  7806  caucvgsr  7915  npnflt  9937  nmnfgt  9940  xleadd1a  9995  xltadd1  9998  xlt2add  10002  xsubge0  10003  xleaddadd  10009  addmodlteq  10543  iseqf1olemkle  10642  hashfiv01gt1  10927  iswrdiz  11001  xrmaxltsup  11569  xrmaxadd  11572  xrbdtri  11587  cvgratz  11843  zdvdsdc  12123  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  divalg  12235  znege1  12500  ennnfonelemk  12771  isxmet2d  14820  trilpolemres  15981  trirec0  15983