Theorem mpjao3dan 1341

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 713   \/ w3o 1001

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 714

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

This theorem is referenced by:  wetriext  4669  nntri3  6643  nntri2or2  6644  nntr2  6649  tridc  7061  nnnninfeq  7295  exmidontriimlem2  7404  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprprlemnkj  7879  caucvgprprlemnbj  7880  caucvgsr  7989  npnflt  10011  nmnfgt  10014  xleadd1a  10069  xltadd1  10072  xlt2add  10076  xsubge0  10077  xleaddadd  10083  addmodlteq  10620  iseqf1olemkle  10719  hashfiv01gt1  11004  iswrdiz  11078  xrmaxltsup  11769  xrmaxadd  11772  xrbdtri  11787  cvgratz  12043  zdvdsdc  12323  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  divalg  12435  znege1  12700  ennnfonelemk  12971  isxmet2d  15022  trilpolemres  16410  trirec0  16412