Theorem jaodan 787

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	|- ( ( ph /\ ps ) -> ch )
jaodan.2	|- ( ( ph /\ th ) -> ch )

Assertion

Ref	Expression
jaodan	|- ( ( ph /\ ( ps \/ th ) ) -> ch )

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 |- ( ( ph /\ ps ) -> ch )
2	1	ex 114	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 114	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 707	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 123	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

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

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

This theorem is referenced by:  mpjaodan  788  ordi  806  andi  808  dcor  920  ccase  949  mpjao3dan  1286  relop  4697  poltletr  4947  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  phplem3  6756  ssfilem  6777  diffitest  6789  reapmul1  8381  apsqgt0  8387  recexaplem2  8437  nnnn0addcl  9031  un0addcl  9034  un0mulcl  9035  elz2  9146  xrltso  9612  xaddnemnf  9670  xaddnepnf  9671  fzsplit2  9861  fzsuc2  9890  elfzp12  9910  expp1  10331  expnegap0  10332  expcllem  10335  mulexpzap  10364  expaddzap  10368  expmulzap  10370  bcpasc  10544  xrltmaxsup  11058  xrmaxaddlem  11061  summodc  11184  fsumsplit  11208  ef0lem  11403  odd2np1  11606  dvdslcm  11786  lcmeq0  11788  lcmcl  11789  lcmneg  11791  lcmgcd  11795  rpexp1i  11868