Theorem jaodan 798

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 718	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 124	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  799  ordi  817  andi  819  dcor  937  ccase  966  mpjao3dan  1318  relop  4812  poltletr  5066  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  phplem3  6910  ssfilem  6931  diffitest  6943  reapmul1  8614  apsqgt0  8620  recexaplem2  8671  nnnn0addcl  9270  un0addcl  9273  un0mulcl  9274  elz2  9388  xrltso  9862  xaddnemnf  9923  xaddnepnf  9924  fzsplit2  10116  fzsuc2  10145  elfzp12  10165  seqf1oglem2  10591  expp1  10617  expnegap0  10618  expcllem  10621  mulexpzap  10650  expaddzap  10654  expmulzap  10656  zzlesq  10779  bcpasc  10837  xrltmaxsup  11400  xrmaxaddlem  11403  summodc  11526  fsumsplit  11550  fprodsplitdc  11739  ef0lem  11803  odd2np1  12014  dvdslcm  12207  lcmeq0  12209  lcmcl  12210  lcmneg  12212  lcmgcd  12216  rpexp1i  12292  pcid  12462  4sqlem16  12544  xpsfeq  12928  mulgneg  13210  mulgnn0z  13219  lgsdir2lem4  15147  lgsdir2  15149  lgsdirnn0  15163  lgsdinn0  15164