Theorem jaodan 826

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

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  mpjaodan  827  andi  911  ccase  987  mpjao3dan  1395  relop  5272  poltletr  5528  ordnbtwn  5816  oeoa  7677  oeoe  7679  phplem3  8141  ssnnfi  8179  unwdomg  8489  numwdom  8882  infpssrlem5  9129  fin23lem24  9144  fin23lem28  9162  fin1a2lem10  9231  zornn0g  9327  gchdomtri  9451  fpwwe2lem12  9463  fpwwe2lem13  9464  msqgt0  10548  recextlem2  10658  lemul1a  10877  nnnn0addcl  11323  un0addcl  11326  un0mulcl  11327  elz2  11394  mul2lt0bi  11936  xaddnemnf  12067  xaddnepnf  12068  rexmul  12101  xlemul1a  12118  xrsupsslem  12137  xrinfmsslem  12138  ixxun  12191  fzsplit2  12366  fzsuc2  12398  elfzp12  12419  seqf1olem2  12841  expp1  12867  expneg  12868  expcllem  12871  mulexpz  12900  expaddz  12904  expmulz  12906  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd4  13084  bcpasc  13108  ccatass  13371  ccatrn  13372  ccatswrd  13456  cats1un  13475  revccat  13515  summo  14448  sumss2  14457  fsumsplit  14471  geomulcvg  14607  fprodsplit  14696  bpoly2  14788  bpoly3  14789  ef0lem  14809  odd2np1  15065  sadcaddlem  15179  gcdcllem3  15223  dvdslcm  15311  lcmeq0  15313  lcmcl  15314  lcmneg  15316  lcmgcd  15320  rpexp1i  15433  pcid  15577  4sqlem16  15664  funcres2c  16561  lubun  17123  mulgneg  17560  mulgnn0z  17567  frgpup3lem  18190  gsumzunsnd  18355  gsumunsnfd  18356  dprddisj2  18438  dmdprdsplit2  18445  dprdsplit  18447  gsumdixp  18609  lssvs0or  19110  evlslem4  19508  refun0  21318  txhaus  21450  xkoptsub  21457  ptunhmeo  21611  xpsxmetlem  22184  xpsmet  22187  mbfss  23413  itg1addlem2  23464  iblss2  23572  itgsplit  23602  limcres  23650  ftc1lem5  23803  coe1mul3  23859  dgrlt  24022  abelthlem3  24187  atanlogaddlem  24640  atanlogsub  24643  atans2  24658  efrlim  24696  bposlem2  25010  lgsdir2lem4  25053  2sqb  25157  pntpbnd1  25275  ostthlem1  25316  hlbtwn  25506  cgracol  25719  inaghl  25731  brbtwn2  25785  axcontlem2  25845  isoun  29479  nn0sqeq1  29513  eliccelico  29539  elicoelioo  29540  fzsplit3  29553  prodpr  29572  xrge0iifhom  29983  esumsplit  30115  esumpad2  30118  sibfinima  30401  circlemethhgt  30721  bnj1137  31063  subfacp1lem4  31165  subfacp1lem5  31166  mclsax  31466  nosepdm  31834  nosupbnd2lem1  31861  poimirlem2  33411  poimirlem8  33417  poimirlem22  33431  poimirlem28  33437  ftc1cnnc  33484  ftc1anclem2  33486  eqfnun  33516  fdc  33541  incsequz2  33545  unichnidl  33830  lkrss2N  34456  cdlemg27b  35984  tendoex  36263  dihmeetlem2N  36588  dvh3dim3N  36738  rexzrexnn0  37368  pell14qrexpcl  37431  elpell1qr2  37436  acongeq  37550  jm2.23  37563  rpnnen3  37599  radcnvrat  38513  sumpair  39194  cncfiooicclem1  40106  fourierdlem80  40403  fourierdlem93  40416  ccatpfx  41409