Theorem jaodan 802

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  803  ordi  821  andi  823  dcor  941  ccase  970  mpjao3dan  1341  relop  4872  poltletr  5129  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  phplem3  7023  ssfilem  7045  diffitest  7057  pr1or2  7378  reapmul1  8753  apsqgt0  8759  recexaplem2  8810  nnnn0addcl  9410  un0addcl  9413  un0mulcl  9414  elz2  9529  xrltso  10004  xaddnemnf  10065  xaddnepnf  10066  fzsplit2  10258  fzsuc2  10287  elfzp12  10307  seqf1oglem2  10754  expp1  10780  expnegap0  10781  expcllem  10784  mulexpzap  10813  expaddzap  10817  expmulzap  10819  zzlesq  10942  bcpasc  11000  ccatass  11156  ccatrn  11157  ccatswrd  11218  ccatpfx  11249  cats1un  11269  xrltmaxsup  11784  xrmaxaddlem  11787  summodc  11910  fsumsplit  11934  fprodsplitdc  12123  ef0lem  12187  odd2np1  12400  dvdslcm  12607  lcmeq0  12609  lcmcl  12610  lcmneg  12612  lcmgcd  12616  rpexp1i  12692  pcid  12863  4sqlem16  12945  xpsfeq  13394  mulgneg  13693  mulgnn0z  13702  lgsdir2lem4  15726  lgsdir2  15728  lgsdirnn0  15742  lgsdinn0  15743