Theorem mpjao3dan 1286

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 787	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
4		mpjao3dan.3	. 2 |- ( ( ph /\ ta ) -> ch )
5		mpjao3dan.4	. . 3 |- ( ph -> ( ps \/ th \/ ta ) )
6		df-3or 964	. . 3 |- ( ( ps \/ th \/ ta ) <-> ( ( ps \/ th ) \/ ta ) )
7	5, 6	sylib 121	. 2 |- ( ph -> ( ( ps \/ th ) \/ ta ) )
8	3, 4, 7	mpjaodan 788	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 698   \/ w3o 962

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

This theorem depends on definitions:  df-bi 116  df-3or 964

This theorem is referenced by:  wetriext  4499  nntri3  6401  nntri2or2  6402  nntr2  6407  tridc  6801  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprprlemnkj  7524  caucvgprprlemnbj  7525  caucvgsr  7634  npnflt  9628  nmnfgt  9631  xleadd1a  9686  xltadd1  9689  xlt2add  9693  xsubge0  9694  xleaddadd  9700  addmodlteq  10202  iseqf1olemkle  10288  hashfiv01gt1  10560  xrmaxltsup  11059  xrmaxadd  11062  xrbdtri  11077  cvgratz  11333  zdvdsdc  11550  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  divalg  11657  znege1  11892  ennnfonelemk  11949  isxmet2d  12556  nninfalllemn  13377  trilpolemres  13410  trirec0  13412