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  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  phplem3  7015  ssfilem  7037  diffitest  7049  pr1or2  7367  reapmul1  8742  apsqgt0  8748  recexaplem2  8799  nnnn0addcl  9399  un0addcl  9402  un0mulcl  9403  elz2  9518  xrltso  9992  xaddnemnf  10053  xaddnepnf  10054  fzsplit2  10246  fzsuc2  10275  elfzp12  10295  seqf1oglem2  10742  expp1  10768  expnegap0  10769  expcllem  10772  mulexpzap  10801  expaddzap  10805  expmulzap  10807  zzlesq  10930  bcpasc  10988  ccatass  11143  ccatrn  11144  ccatswrd  11202  ccatpfx  11233  cats1un  11253  xrltmaxsup  11768  xrmaxaddlem  11771  summodc  11894  fsumsplit  11918  fprodsplitdc  12107  ef0lem  12171  odd2np1  12384  dvdslcm  12591  lcmeq0  12593  lcmcl  12594  lcmneg  12596  lcmgcd  12600  rpexp1i  12676  pcid  12847  4sqlem16  12929  xpsfeq  13378  mulgneg  13677  mulgnn0z  13686  lgsdir2lem4  15710  lgsdir2  15712  lgsdirnn0  15726  lgsdinn0  15727