Theorem jaodan 792

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 114	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 114	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 712	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 123	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  793  ordi  811  andi  813  dcor  930  ccase  959  mpjao3dan  1302  relop  4761  poltletr  5011  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  phplem3  6832  ssfilem  6853  diffitest  6865  reapmul1  8514  apsqgt0  8520  recexaplem2  8570  nnnn0addcl  9165  un0addcl  9168  un0mulcl  9169  elz2  9283  xrltso  9753  xaddnemnf  9814  xaddnepnf  9815  fzsplit2  10006  fzsuc2  10035  elfzp12  10055  expp1  10483  expnegap0  10484  expcllem  10487  mulexpzap  10516  expaddzap  10520  expmulzap  10522  bcpasc  10700  xrltmaxsup  11220  xrmaxaddlem  11223  summodc  11346  fsumsplit  11370  fprodsplitdc  11559  ef0lem  11623  odd2np1  11832  dvdslcm  12023  lcmeq0  12025  lcmcl  12026  lcmneg  12028  lcmgcd  12032  rpexp1i  12108  pcid  12277  lgsdir2lem4  13726  lgsdir2  13728  lgsdirnn0  13742  lgsdinn0  13743