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  4779  poltletr  5031  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  phplem3  6856  ssfilem  6877  diffitest  6889  reapmul1  8554  apsqgt0  8560  recexaplem2  8611  nnnn0addcl  9208  un0addcl  9211  un0mulcl  9212  elz2  9326  xrltso  9798  xaddnemnf  9859  xaddnepnf  9860  fzsplit2  10052  fzsuc2  10081  elfzp12  10101  expp1  10529  expnegap0  10530  expcllem  10533  mulexpzap  10562  expaddzap  10566  expmulzap  10568  bcpasc  10748  xrltmaxsup  11267  xrmaxaddlem  11270  summodc  11393  fsumsplit  11417  fprodsplitdc  11606  ef0lem  11670  odd2np1  11880  dvdslcm  12071  lcmeq0  12073  lcmcl  12074  lcmneg  12076  lcmgcd  12080  rpexp1i  12156  pcid  12325  xpsfeq  12769  mulgneg  13006  mulgnn0z  13015  lgsdir2lem4  14471  lgsdir2  14473  lgsdirnn0  14487  lgsdinn0  14488