Theorem jaodan 804

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  805  ordi  823  andi  825  dcor  943  ccase  972  mpjao3dan  1343  relop  4880  poltletr  5137  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  phplem3  7040  ssfilem  7062  ssfilemd  7064  diffitest  7076  pr1or2  7399  reapmul1  8775  apsqgt0  8781  recexaplem2  8832  nnnn0addcl  9432  un0addcl  9435  un0mulcl  9436  elz2  9551  xrltso  10031  xaddnemnf  10092  xaddnepnf  10093  fzsplit2  10285  fzsuc2  10314  elfzp12  10334  seqf1oglem2  10783  expp1  10809  expnegap0  10810  expcllem  10813  mulexpzap  10842  expaddzap  10846  expmulzap  10848  zzlesq  10971  bcpasc  11029  ccatass  11189  ccatrn  11190  ccatswrd  11255  ccatpfx  11286  cats1un  11306  xrltmaxsup  11835  xrmaxaddlem  11838  summodc  11962  fsumsplit  11986  fprodsplitdc  12175  ef0lem  12239  odd2np1  12452  dvdslcm  12659  lcmeq0  12661  lcmcl  12662  lcmneg  12664  lcmgcd  12668  rpexp1i  12744  pcid  12915  4sqlem16  12997  xpsfeq  13446  mulgneg  13745  mulgnn0z  13754  lgsdir2lem4  15779  lgsdir2  15781  lgsdirnn0  15795  lgsdinn0  15796