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  4777  poltletr  5029  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  phplem3  6853  ssfilem  6874  diffitest  6886  reapmul1  8551  apsqgt0  8557  recexaplem2  8608  nnnn0addcl  9205  un0addcl  9208  un0mulcl  9209  elz2  9323  xrltso  9795  xaddnemnf  9856  xaddnepnf  9857  fzsplit2  10049  fzsuc2  10078  elfzp12  10098  expp1  10526  expnegap0  10527  expcllem  10530  mulexpzap  10559  expaddzap  10563  expmulzap  10565  bcpasc  10745  xrltmaxsup  11264  xrmaxaddlem  11267  summodc  11390  fsumsplit  11414  fprodsplitdc  11603  ef0lem  11667  odd2np1  11877  dvdslcm  12068  lcmeq0  12070  lcmcl  12071  lcmneg  12073  lcmgcd  12077  rpexp1i  12153  pcid  12322  xpsfeq  12763  mulgneg  13000  mulgnn0z  13008  lgsdir2lem4  14402  lgsdir2  14404  lgsdirnn0  14418  lgsdinn0  14419