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  4778  poltletr  5030  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  phplem3  6854  ssfilem  6875  diffitest  6887  reapmul1  8552  apsqgt0  8558  recexaplem2  8609  nnnn0addcl  9206  un0addcl  9209  un0mulcl  9210  elz2  9324  xrltso  9796  xaddnemnf  9857  xaddnepnf  9858  fzsplit2  10050  fzsuc2  10079  elfzp12  10099  expp1  10527  expnegap0  10528  expcllem  10531  mulexpzap  10560  expaddzap  10564  expmulzap  10566  bcpasc  10746  xrltmaxsup  11265  xrmaxaddlem  11268  summodc  11391  fsumsplit  11415  fprodsplitdc  11604  ef0lem  11668  odd2np1  11878  dvdslcm  12069  lcmeq0  12071  lcmcl  12072  lcmneg  12074  lcmgcd  12078  rpexp1i  12154  pcid  12323  xpsfeq  12764  mulgneg  13001  mulgnn0z  13010  lgsdir2lem4  14435  lgsdir2  14437  lgsdirnn0  14451  lgsdinn0  14452