Theorem jaodan 783

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 434	. . 3 |- ( ph -> ( ps -> ch ) )
3		jaodan.2	. . . 4 |- ( ( ph /\ th ) -> ch )
4	3	ex 434	. . 3 |- ( ph -> ( th -> ch ) )
5	2, 4	jaod 380	. 2 |- ( ph -> ( ( ps \/ th ) -> ch ) )
6	5	imp 429	1 |- ( ( ph /\ ( ps \/ th ) ) -> ch )

Syntax hints:   -> wi 4   \/ wo 368   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371

This theorem is referenced by:  mpjaodan  784  andi  865  ccase  944  mpjao3dan  1295  relop  5153  poltletr  5402  oeoa  7246  oeoe  7248  phplem3  7698  ssnnfi  7739  unwdomg  8010  numwdom  8440  infpssrlem5  8687  fin23lem24  8702  fin23lem28  8720  fin1a2lem10  8789  zornn0g  8885  gchdomtri  9007  fpwwe2lem12  9019  fpwwe2lem13  9020  msqgt0  10073  recextlem2  10180  lemul1a  10396  nnnn0addcl  10826  un0addcl  10829  un0mulcl  10830  elz2  10881  xaddnemnf  11433  xaddnepnf  11434  rexmul  11463  xlemul1a  11480  xrsupsslem  11498  xrinfmsslem  11499  ixxun  11545  fzsplit2  11710  fzsuc2  11737  elfzp12  11757  seqf1olem2  12115  expp1  12141  expneg  12142  expcllem  12145  mulexpz  12174  expaddz  12178  expmulz  12180  faclbnd4lem3  12341  faclbnd4lem4  12342  faclbnd4  12343  bcpasc  12367  wrdsymb0  12540  ccatass  12570  ccatswrd  12644  cats1un  12664  revccat  12703  summo  13502  sumss2  13511  fsumsplit  13525  geomulcvg  13648  ef0lem  13676  dvdseq  13892  odd2np1  13905  sadcaddlem  13966  gcdcllem3  14010  rpexp1i  14121  pcid  14255  4sqlem16  14337  funcres2c  15128  lubun  15610  mulgneg  15970  mulgnn0z  15972  frgpup3lem  16601  gsumzunsnd  16785  gsumunsnfd  16786  dprddisj2  16889  dprddisj2OLD  16890  dmdprdsplit2  16897  dprdsplit  16899  gsumdixpOLD  17058  gsumdixp  17059  lssvs0or  17556  evlslem4OLD  17972  evlslem4  17973  txhaus  19911  xkoptsub  19918  ptunhmeo  20072  xpsxmetlem  20645  xpsmet  20648  mbfss  21816  itg1addlem2  21867  iblss2  21975  itgsplit  22005  limcres  22053  ftc1lem5  22204  coe1mul3  22263  dgrlt  22425  abelthlem3  22590  atanlogaddlem  23000  atanlogsub  23003  atans2  23018  efrlim  23055  bposlem2  23316  lgsdir2lem4  23357  2sqb  23409  pntpbnd1  23527  ostthlem1  23568  brbtwn2  23912  axcontlem2  23972  uvtx01vtx  24196  isoun  27220  mul2lt0bi  27265  eliccelico  27284  elicoelioo  27285  fzsplit3  27295  xrge0iifhom  27583  esumsplit  27731  sibfinima  27949  subfacp1lem4  28295  subfacp1lem5  28296  fprodsplit  28700  bpoly2  29424  bpoly3  29425  ftc1cnnc  29694  ftc1anclem2  29696  eqfnun  29843  fdc  29869  incsequz2  29873  unichnidl  30059  rexzrexnn0  30369  pell14qrexpcl  30435  elpell1qr2  30440  acongeq  30553  jm2.23  30570  rpnnen3  30606  dvdslcm  30832  lcmeq0  30834  lcmcl  30835  lcmneg  30837  lcmgcd  30841  sumpair  31016  cncfiooicclem1  31260  fourierdlem80  31515  fourierdlem93  31528  bnj1137  33148  lkrss2N  33984  cdlemg27b  35510  tendoex  35789  dihmeetlem2N  36114  dvh3dim3N  36264