Theorem jaodan 799

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaodan  800  ordi  818  andi  820  dcor  938  ccase  967  mpjao3dan  1320  relop  4829  poltletr  5084  tfrlemisucaccv  6413  tfr1onlemsucaccv  6429  tfrcllemsucaccv  6442  phplem3  6953  ssfilem  6974  diffitest  6986  reapmul1  8670  apsqgt0  8676  recexaplem2  8727  nnnn0addcl  9327  un0addcl  9330  un0mulcl  9331  elz2  9446  xrltso  9920  xaddnemnf  9981  xaddnepnf  9982  fzsplit2  10174  fzsuc2  10203  elfzp12  10223  seqf1oglem2  10667  expp1  10693  expnegap0  10694  expcllem  10697  mulexpzap  10726  expaddzap  10730  expmulzap  10732  zzlesq  10855  bcpasc  10913  ccatass  11067  ccatrn  11068  ccatswrd  11126  ccatpfx  11155  xrltmaxsup  11601  xrmaxaddlem  11604  summodc  11727  fsumsplit  11751  fprodsplitdc  11940  ef0lem  12004  odd2np1  12217  dvdslcm  12424  lcmeq0  12426  lcmcl  12427  lcmneg  12429  lcmgcd  12433  rpexp1i  12509  pcid  12680  4sqlem16  12762  xpsfeq  13210  mulgneg  13509  mulgnn0z  13518  lgsdir2lem4  15541  lgsdir2  15543  lgsdirnn0  15557  lgsdinn0  15558