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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaodan  810  ordi  828  andi  830  dcor  948  ccase  977  mpjao3dan  1348  relop  4930  poltletr  5188  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  phplem3  7155  ssfilem  7177  ssfilemd  7179  diffitest  7191  pr1or2  7541  reapmul1  8926  apsqgt0  8932  recexaplem2  8983  nnnn0addcl  9598  un0addcl  9601  un0mulcl  9602  elz2  9721  xrltso  10209  xaddnemnf  10270  xaddnepnf  10271  fzsplit2  10466  fzsplit3  10469  fzsuc2  10497  elfzp12  10517  seqf1oglem2  10972  expp1  10998  expnegap0  10999  expcllem  11002  mulexpzap  11031  expaddzap  11035  expmulzap  11037  zzlesq  11161  bcpasc  11220  ccatass  11392  ccatrn  11393  ccatswrd  11458  ccatpfx  11489  cats1un  11509  xrltmaxsup  12042  xrmaxaddlem  12045  summodc  12169  fsumsplit  12193  fprodsplitdc  12382  ef0lem  12446  odd2np1  12659  dvdslcm  12866  lcmeq0  12868  lcmcl  12869  lcmneg  12871  lcmgcd  12875  rpexp1i  12952  pcid  13126  4sqlem16  13208  xpsfeq  13719  mulgneg  13996  mulgnn0z  14005  bposlem2  16273  lgsdir2lem4  16316  lgsdir2  16318  lgsdirnn0  16332  lgsdinn0  16333