Theorem jaodan 797

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 115	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 115	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 717	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 124	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  798  ordi  816  andi  818  dcor  935  ccase  964  mpjao3dan  1307  relop  4774  poltletr  5026  tfrlemisucaccv  6321  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  phplem3  6849  ssfilem  6870  diffitest  6882  reapmul1  8546  apsqgt0  8552  recexaplem2  8603  nnnn0addcl  9200  un0addcl  9203  un0mulcl  9204  elz2  9318  xrltso  9790  xaddnemnf  9851  xaddnepnf  9852  fzsplit2  10043  fzsuc2  10072  elfzp12  10092  expp1  10520  expnegap0  10521  expcllem  10524  mulexpzap  10553  expaddzap  10557  expmulzap  10559  bcpasc  10737  xrltmaxsup  11256  xrmaxaddlem  11259  summodc  11382  fsumsplit  11406  fprodsplitdc  11595  ef0lem  11659  odd2np1  11868  dvdslcm  12059  lcmeq0  12061  lcmcl  12062  lcmneg  12064  lcmgcd  12068  rpexp1i  12144  pcid  12313  mulgneg  12929  mulgnn0z  12937  lgsdir2lem4  14214  lgsdir2  14216  lgsdirnn0  14230  lgsdinn0  14231