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  5386  relop  5814  poltletr  6105  ordnbtwn  6427  eqfnun  7009  oeoa  8561  oeoe  8563  ssnnfi  9133  domnsymfi  9164  unwdomg  9537  numwdom  10012  infpssrlem5  10260  fin23lem24  10275  fin23lem28  10293  fin1a2lem10  10362  zornn0g  10458  gchdomtri  10582  fpwwe2lem11  10594  fpwwe2lem12  10595  msqgt0  11698  recextlem2  11809  lemul1a  12036  nnne0  12220  nnnn0addcl  12472  un0addcl  12475  un0mulcl  12476  elz2  12547  mul2lt0bi  13059  xaddnemnf  13196  xaddnepnf  13197  rexmul  13231  xlemul1a  13248  xrsupsslem  13267  xrinfmsslem  13268  ixxun  13322  fzsplit2  13510  fzsuc2  13543  elfzp12  13564  seqf1olem2  14007  expp1  14033  expneg  14034  expcllem  14037  mulexpz  14067  expaddz  14071  expmulz  14073  zzlesq  14171  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd4  14262  bcpasc  14286  ccatass  14553  ccatrn  14554  ccatswrd  14633  ccatpfx  14666  cats1un  14686  revccat  14731  summo  15683  sumss2  15692  fsumsplit  15707  geomulcvg  15842  fprodsplit  15932  bpoly2  16023  bpoly3  16024  ef0lem  16044  odd2np1  16311  sadcaddlem  16427  gcdcllem3  16471  dvdslcm  16568  lcmeq0  16570  lcmcl  16571  lcmneg  16573  lcmgcd  16577  rpexp1i  16693  pcid  16844  4sqlem16  16931  funcres2c  17865  lubun  18474  mulgneg  19024  mulgnn0z  19033  frgpup3lem  19707  gsumzunsnd  19886  gsumunsnfd  19887  dprddisj2  19971  dmdprdsplit2  19978  dprdsplit  19980  gsumdixp  20228  lssvs0or  21020  evlslem4  21983  refun0  23402  txhaus  23534  xkoptsub  23541  ptunhmeo  23695  xpsxmetlem  24267  xpsmet  24270  mbfss  25547  itg1addlem2  25598  iblss2  25707  itgsplit  25737  limcres  25787  ftc1lem5  25947  coe1mul3  26004  dgrlt  26172  abelthlem3  26343  atanlogaddlem  26823  atanlogsub  26826  atans2  26841  efrlim  26879  efrlimOLD  26880  bposlem2  27196  lgsdir2lem4  27239  2sqb  27343  pntpbnd1  27497  ostthlem1  27538  nosepdm  27596  nosupbnd2lem1  27627  negsid  27947  elzn0s  28286  zsbday  28294  zscut  28295  expsp1  28315  hlbtwn  28538  cgracol  28755  inaghl  28772  brbtwn2  28832  axcontlem2  28892  ifnebib  32478  isoun  32625  eliccelico  32700  elicoelioo  32701  fzsplit3  32716  prodpr  32751  zarclsun  33860  xrge0iifhom  33927  esumsplit  34043  esumpad2  34046  sibfinima  34330  circlemethhgt  34634  bnj1137  34985  subfacp1lem4  35170  subfacp1lem5  35171  mclsax  35556  poimirlem2  37616  poimirlem8  37622  poimirlem22  37636  poimirlem28  37642  ftc1cnnc  37686  ftc1anclem2  37688  fdc  37739  incsequz2  37743  unichnidl  38025  lkrss2N  39162  cdlemg27b  40690  tendoex  40969  dihmeetlem2N  41293  dvh3dim3N  41443  aks6d1c2p2  42107  hashscontpow  42110  aks6d1c5  42127  sticksstones1  42134  sticksstones2  42135  unitscyglem2  42184  ofun  42224  sn-nnne0  42448  nn0addcom  42450  nn0mulcom  42454  zmulcomlem  42455  rexzrexnn0  42792  pell14qrexpcl  42855  elpell1qr2  42860  acongeq  42972  jm2.23  42985  rpnnen3  43021  mnringmulrcld  44217  mnuprdlem3  44263  radcnvrat  44303  sumpair  45029  cncfiooicclem1  45891  fourierdlem80  46184  fourierdlem93  46197  fullthinc  49439