Theorem jaodan 958

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 858	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

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

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 847

This theorem is referenced by:  mpjaodan  959  andi  1008  ccase  1038  axpr  5446  relop  5875  poltletr  6164  ordnbtwn  6488  eqfnun  7070  oeoa  8653  oeoe  8655  ssnnfi  9235  ssnnfiOLD  9236  domnsymfi  9266  phplem3OLD  9282  unwdomg  9653  numwdom  10128  infpssrlem5  10376  fin23lem24  10391  fin23lem28  10409  fin1a2lem10  10478  zornn0g  10574  gchdomtri  10698  fpwwe2lem11  10710  fpwwe2lem12  10711  msqgt0  11810  recextlem2  11921  lemul1a  12148  nnne0  12327  nnnn0addcl  12583  un0addcl  12586  un0mulcl  12587  elz2  12657  mul2lt0bi  13163  xaddnemnf  13298  xaddnepnf  13299  rexmul  13333  xlemul1a  13350  xrsupsslem  13369  xrinfmsslem  13370  ixxun  13423  fzsplit2  13609  fzsuc2  13642  elfzp12  13663  seqf1olem2  14093  expp1  14119  expneg  14120  expcllem  14123  mulexpz  14153  expaddz  14157  expmulz  14159  zzlesq  14255  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd4  14346  bcpasc  14370  ccatass  14636  ccatrn  14637  ccatswrd  14716  ccatpfx  14749  cats1un  14769  revccat  14814  summo  15765  sumss2  15774  fsumsplit  15789  geomulcvg  15924  fprodsplit  16014  bpoly2  16105  bpoly3  16106  ef0lem  16126  odd2np1  16389  sadcaddlem  16503  gcdcllem3  16547  dvdslcm  16645  lcmeq0  16647  lcmcl  16648  lcmneg  16650  lcmgcd  16654  rpexp1i  16770  pcid  16920  4sqlem16  17007  funcres2c  17968  lubun  18585  mulgneg  19132  mulgnn0z  19141  frgpup3lem  19819  gsumzunsnd  19998  gsumunsnfd  19999  dprddisj2  20083  dmdprdsplit2  20090  dprdsplit  20092  gsumdixp  20342  lssvs0or  21135  evlslem4  22123  refun0  23544  txhaus  23676  xkoptsub  23683  ptunhmeo  23837  xpsxmetlem  24410  xpsmet  24413  mbfss  25700  itg1addlem2  25751  iblss2  25861  itgsplit  25891  limcres  25941  ftc1lem5  26101  coe1mul3  26158  dgrlt  26326  abelthlem3  26495  atanlogaddlem  26974  atanlogsub  26977  atans2  26992  efrlim  27030  efrlimOLD  27031  bposlem2  27347  lgsdir2lem4  27390  2sqb  27494  pntpbnd1  27648  ostthlem1  27689  nosepdm  27747  nosupbnd2lem1  27778  negsid  28091  elzn0s  28402  zsbday  28410  zscut  28411  expsp1  28430  hlbtwn  28637  cgracol  28854  inaghl  28871  brbtwn2  28938  axcontlem2  28998  ifnebib  32572  isoun  32713  eliccelico  32782  elicoelioo  32783  fzsplit3  32799  prodpr  32830  zarclsun  33816  xrge0iifhom  33883  esumsplit  34017  esumpad2  34020  sibfinima  34304  circlemethhgt  34620  bnj1137  34971  subfacp1lem4  35151  subfacp1lem5  35152  mclsax  35537  poimirlem2  37582  poimirlem8  37588  poimirlem22  37602  poimirlem28  37608  ftc1cnnc  37652  ftc1anclem2  37654  fdc  37705  incsequz2  37709  unichnidl  37991  lkrss2N  39125  cdlemg27b  40653  tendoex  40932  dihmeetlem2N  41256  dvh3dim3N  41406  aks6d1c2p2  42076  hashscontpow  42079  aks6d1c5  42096  sticksstones1  42103  sticksstones2  42104  unitscyglem2  42153  metakunt9  42170  ofun  42231  sn-nnne0  42424  nn0addcom  42426  nn0mulcom  42430  zmulcomlem  42431  rexzrexnn0  42760  pell14qrexpcl  42823  elpell1qr2  42828  acongeq  42940  jm2.23  42953  rpnnen3  42989  mnringmulrcld  44197  mnuprdlem3  44243  radcnvrat  44283  sumpair  44935  cncfiooicclem1  45814  fourierdlem80  46107  fourierdlem93  46120  fullthinc  48713