Theorem jaodan 809

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

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

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4925  poltletr  5183  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  phplem3  7145  ssfilem  7167  ssfilemd  7169  diffitest  7181  pr1or2  7530  reapmul1  8913  apsqgt0  8919  recexaplem2  8970  nnnn0addcl  9572  un0addcl  9575  un0mulcl  9576  elz2  9695  xrltso  10177  xaddnemnf  10238  xaddnepnf  10239  fzsplit2  10433  fzsplit3  10436  fzsuc2  10464  elfzp12  10484  seqf1oglem2  10935  expp1  10961  expnegap0  10962  expcllem  10965  mulexpzap  10994  expaddzap  10998  expmulzap  11000  zzlesq  11124  bcpasc  11182  ccatass  11354  ccatrn  11355  ccatswrd  11420  ccatpfx  11451  cats1un  11471  xrltmaxsup  12001  xrmaxaddlem  12004  summodc  12128  fsumsplit  12152  fprodsplitdc  12341  ef0lem  12405  odd2np1  12618  dvdslcm  12825  lcmeq0  12827  lcmcl  12828  lcmneg  12830  lcmgcd  12834  rpexp1i  12910  pcid  13081  4sqlem16  13163  xpsfeq  13643  mulgneg  13920  mulgnn0z  13929  lgsdir2lem4  16064  lgsdir2  16066  lgsdirnn0  16080  lgsdinn0  16081