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  4759  poltletr  5009  tfrlemisucaccv  6301  tfr1onlemsucaccv  6317  tfrcllemsucaccv  6330  phplem3  6828  ssfilem  6849  diffitest  6861  reapmul1  8501  apsqgt0  8507  recexaplem2  8557  nnnn0addcl  9152  un0addcl  9155  un0mulcl  9156  elz2  9270  xrltso  9740  xaddnemnf  9801  xaddnepnf  9802  fzsplit2  9993  fzsuc2  10022  elfzp12  10042  expp1  10470  expnegap0  10471  expcllem  10474  mulexpzap  10503  expaddzap  10507  expmulzap  10509  bcpasc  10687  xrltmaxsup  11207  xrmaxaddlem  11210  summodc  11333  fsumsplit  11357  fprodsplitdc  11546  ef0lem  11610  odd2np1  11819  dvdslcm  12010  lcmeq0  12012  lcmcl  12013  lcmneg  12015  lcmgcd  12019  rpexp1i  12095  pcid  12264  lgsdir2lem4  13647  lgsdir2  13649  lgsdirnn0  13663  lgsdinn0  13664