Theorem mpjao3dan 1343

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 715   \/ w3o 1003

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 716

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

This theorem is referenced by:  wetriext  4675  nntri3  6664  nntri2or2  6665  nntr2  6670  tridc  7088  nnnninfeq  7326  exmidontriimlem2  7436  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprprlemnkj  7911  caucvgprprlemnbj  7912  caucvgsr  8021  npnflt  10049  nmnfgt  10052  xleadd1a  10107  xltadd1  10110  xlt2add  10114  xsubge0  10115  xleaddadd  10121  addmodlteq  10659  iseqf1olemkle  10758  hashfiv01gt1  11043  iswrdiz  11119  xrmaxltsup  11818  xrmaxadd  11821  xrbdtri  11836  cvgratz  12092  zdvdsdc  12372  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  divalg  12484  znege1  12749  ennnfonelemk  13020  isxmet2d  15071  trilpolemres  16646  trirec0  16648