Theorem mpjao3dan 1344

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716   \/ w3o 1004

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 717

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

This theorem is referenced by:  wetriext  4681  nntri3  6708  nntri2or2  6709  nntr2  6714  tridc  7132  nnnninfeq  7387  exmidontriimlem2  7497  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprprlemnkj  7972  caucvgprprlemnbj  7973  caucvgsr  8082  npnflt  10111  nmnfgt  10114  xleadd1a  10169  xltadd1  10172  xlt2add  10176  xsubge0  10177  xleaddadd  10183  addmodlteq  10723  iseqf1olemkle  10822  hashfiv01gt1  11107  iswrdiz  11186  xrmaxltsup  11898  xrmaxadd  11901  xrbdtri  11916  cvgratz  12173  zdvdsdc  12453  divalglemeunn  12562  divalglemex  12563  divalglemeuneg  12564  divalg  12565  znege1  12830  ennnfonelemk  13101  isxmet2d  15159  trilpolemres  16774  trirec0  16776