Theorem mpjao3dan 1341

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 713   \/ w3o 1001

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 714

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

This theorem is referenced by:  wetriext  4669  nntri3  6651  nntri2or2  6652  nntr2  6657  tridc  7070  nnnninfeq  7306  exmidontriimlem2  7415  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprprlemnkj  7890  caucvgprprlemnbj  7891  caucvgsr  8000  npnflt  10023  nmnfgt  10026  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xsubge0  10089  xleaddadd  10095  addmodlteq  10632  iseqf1olemkle  10731  hashfiv01gt1  11016  iswrdiz  11091  xrmaxltsup  11785  xrmaxadd  11788  xrbdtri  11803  cvgratz  12059  zdvdsdc  12339  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  divalg  12451  znege1  12716  ennnfonelemk  12987  isxmet2d  15038  trilpolemres  16498  trirec0  16500