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  4729  poltletr  4979  tfrlemisucaccv  6262  tfr1onlemsucaccv  6278  tfrcllemsucaccv  6291  phplem3  6788  ssfilem  6809  diffitest  6821  reapmul1  8449  apsqgt0  8455  recexaplem2  8505  nnnn0addcl  9099  un0addcl  9102  un0mulcl  9103  elz2  9214  xrltso  9681  xaddnemnf  9739  xaddnepnf  9740  fzsplit2  9930  fzsuc2  9959  elfzp12  9979  expp1  10404  expnegap0  10405  expcllem  10408  mulexpzap  10437  expaddzap  10441  expmulzap  10443  bcpasc  10617  xrltmaxsup  11131  xrmaxaddlem  11134  summodc  11257  fsumsplit  11281  fprodsplitdc  11470  ef0lem  11534  odd2np1  11737  dvdslcm  11917  lcmeq0  11919  lcmcl  11920  lcmneg  11922  lcmgcd  11926  rpexp1i  11999