Theorem jaodan 749

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaodan  750  ordi  768  andi  770  dcor  884  ccase  913  mpjao3dan  1250  relop  4617  poltletr  4865  tfrlemisucaccv  6128  tfr1onlemsucaccv  6144  tfrcllemsucaccv  6157  phplem3  6650  ssfilem  6671  diffitest  6683  reapmul1  8169  apsqgt0  8175  recexaplem2  8218  nnnn0addcl  8801  un0addcl  8804  un0mulcl  8805  elz2  8916  xrltso  9365  xaddnemnf  9423  xaddnepnf  9424  fzsplit2  9613  fzsuc2  9642  elfzp12  9662  expp1  10093  expnegap0  10094  expcllem  10097  mulexpzap  10126  expaddzap  10130  expmulzap  10132  bcpasc  10305  xrltmaxsup  10816  xrmaxaddlem  10819  summodc  10942  fsumsplit  10966  ef0lem  11115  odd2np1  11316  dvdslcm  11494  lcmeq0  11496  lcmcl  11497  lcmneg  11499  lcmgcd  11503  rpexp1i  11576