Theorem jaodan 959

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 412	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 859	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  mpjaodan  960  andi  1009  ccase  1037  axprOLD  5401  relop  5830  poltletr  6121  ordnbtwn  6446  eqfnun  7026  oeoa  8607  oeoe  8609  ssnnfi  9181  domnsymfi  9212  phplem3OLD  9228  unwdomg  9596  numwdom  10071  infpssrlem5  10319  fin23lem24  10334  fin23lem28  10352  fin1a2lem10  10421  zornn0g  10517  gchdomtri  10641  fpwwe2lem11  10653  fpwwe2lem12  10654  msqgt0  11755  recextlem2  11866  lemul1a  12093  nnne0  12272  nnnn0addcl  12529  un0addcl  12532  un0mulcl  12533  elz2  12604  mul2lt0bi  13113  xaddnemnf  13250  xaddnepnf  13251  rexmul  13285  xlemul1a  13302  xrsupsslem  13321  xrinfmsslem  13322  ixxun  13376  fzsplit2  13564  fzsuc2  13597  elfzp12  13618  seqf1olem2  14058  expp1  14084  expneg  14085  expcllem  14088  mulexpz  14118  expaddz  14122  expmulz  14124  zzlesq  14222  faclbnd4lem3  14311  faclbnd4lem4  14312  faclbnd4  14313  bcpasc  14337  ccatass  14604  ccatrn  14605  ccatswrd  14684  ccatpfx  14717  cats1un  14737  revccat  14782  summo  15731  sumss2  15740  fsumsplit  15755  geomulcvg  15890  fprodsplit  15980  bpoly2  16071  bpoly3  16072  ef0lem  16092  odd2np1  16358  sadcaddlem  16474  gcdcllem3  16518  dvdslcm  16615  lcmeq0  16617  lcmcl  16618  lcmneg  16620  lcmgcd  16624  rpexp1i  16740  pcid  16891  4sqlem16  16978  funcres2c  17914  lubun  18523  mulgneg  19073  mulgnn0z  19082  frgpup3lem  19756  gsumzunsnd  19935  gsumunsnfd  19936  dprddisj2  20020  dmdprdsplit2  20027  dprdsplit  20029  gsumdixp  20277  lssvs0or  21069  evlslem4  22032  refun0  23451  txhaus  23583  xkoptsub  23590  ptunhmeo  23744  xpsxmetlem  24316  xpsmet  24319  mbfss  25597  itg1addlem2  25648  iblss2  25757  itgsplit  25787  limcres  25837  ftc1lem5  25997  coe1mul3  26054  dgrlt  26222  abelthlem3  26393  atanlogaddlem  26873  atanlogsub  26876  atans2  26891  efrlim  26929  efrlimOLD  26930  bposlem2  27246  lgsdir2lem4  27289  2sqb  27393  pntpbnd1  27547  ostthlem1  27588  nosepdm  27646  nosupbnd2lem1  27677  negsid  27990  elzn0s  28301  zsbday  28309  zscut  28310  expsp1  28329  hlbtwn  28536  cgracol  28753  inaghl  28770  brbtwn2  28830  axcontlem2  28890  ifnebib  32476  isoun  32625  eliccelico  32700  elicoelioo  32701  fzsplit3  32716  prodpr  32751  zarclsun  33847  xrge0iifhom  33914  esumsplit  34030  esumpad2  34033  sibfinima  34317  circlemethhgt  34621  bnj1137  34972  subfacp1lem4  35151  subfacp1lem5  35152  mclsax  35537  poimirlem2  37592  poimirlem8  37598  poimirlem22  37612  poimirlem28  37618  ftc1cnnc  37662  ftc1anclem2  37664  fdc  37715  incsequz2  37719  unichnidl  38001  lkrss2N  39133  cdlemg27b  40661  tendoex  40940  dihmeetlem2N  41264  dvh3dim3N  41414  aks6d1c2p2  42078  hashscontpow  42081  aks6d1c5  42098  sticksstones1  42105  sticksstones2  42106  unitscyglem2  42155  metakunt9  42172  ofun  42234  sn-nnne0  42438  nn0addcom  42440  nn0mulcom  42444  zmulcomlem  42445  rexzrexnn0  42774  pell14qrexpcl  42837  elpell1qr2  42842  acongeq  42954  jm2.23  42967  rpnnen3  43003  mnringmulrcld  44200  mnuprdlem3  44246  radcnvrat  44286  sumpair  45007  cncfiooicclem1  45870  fourierdlem80  46163  fourierdlem93  46176  fullthinc  49284