Theorem mpjao3dan 1302

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

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 703   \/ w3o 972

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 704

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

This theorem is referenced by:  wetriext  4561  nntri3  6476  nntri2or2  6477  nntr2  6482  tridc  6877  nnnninfeq  7104  exmidontriimlem2  7199  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprprlemnkj  7654  caucvgprprlemnbj  7655  caucvgsr  7764  npnflt  9772  nmnfgt  9775  xleadd1a  9830  xltadd1  9833  xlt2add  9837  xsubge0  9838  xleaddadd  9844  addmodlteq  10354  iseqf1olemkle  10440  hashfiv01gt1  10716  xrmaxltsup  11221  xrmaxadd  11224  xrbdtri  11239  cvgratz  11495  zdvdsdc  11774  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  divalg  11883  znege1  12132  ennnfonelemk  12355  isxmet2d  13142  trilpolemres  14074  trirec0  14076