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  4643  nntri3  6606  nntri2or2  6607  nntr2  6612  tridc  7022  nnnninfeq  7256  exmidontriimlem2  7365  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprprlemnkj  7840  caucvgprprlemnbj  7841  caucvgsr  7950  npnflt  9972  nmnfgt  9975  xleadd1a  10030  xltadd1  10033  xlt2add  10037  xsubge0  10038  xleaddadd  10044  addmodlteq  10580  iseqf1olemkle  10679  hashfiv01gt1  10964  iswrdiz  11038  xrmaxltsup  11684  xrmaxadd  11687  xrbdtri  11702  cvgratz  11958  zdvdsdc  12238  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  divalg  12350  znege1  12615  ennnfonelemk  12886  isxmet2d  14935  trilpolemres  16183  trirec0  16185