Theorem mpjao3dan 1243

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 746	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 925	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 120	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 747	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 102   \/ wo 664   \/ w3o 923

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665

This theorem depends on definitions:  df-bi 115  df-3or 925

This theorem is referenced by:  wetriext  4392  nntri3  6258  nntri2or2  6259  tridc  6613  caucvgprlemnkj  7223  caucvgprlemnbj  7224  caucvgprprlemnkj  7249  caucvgprprlemnbj  7250  caucvgsr  7345  addmodlteq  9801  iseqf1olemkle  9909  hashfiv01gt1  10186  cvgratz  10922  zdvdsdc  11091  divalglemeunn  11195  divalglemex  11196  divalglemeuneg  11197  divalg  11198  znege1  11430  nninfalllemn  11853