Theorem jaodan 972

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 417	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 417	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 872	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 411	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860

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 210  df-an 401  df-or 861

This theorem is referenced by:  mpjaodan  973  andi  1025  ccase  1053  axprOLD  5403  relop  5836  poltletr  6132  ordnbtwn  6456  eqfnun  7032  oeoa  8579  oeoe  8581  ssnnfi  9150  domnsymfi  9180  unwdomg  9542  numwdom  10039  infpssrlem5  10286  fin23lem24  10301  fin23lem28  10319  fin1a2lem10  10388  zornn0g  10484  gchdomtri  10609  fpwwe2lem11  10621  fpwwe2lem12  10622  msqgt0  11729  recextlem2  11840  lemul1a  12064  nnne0  12265  nnnn0addcl  12529  un0addcl  12532  un0mulcl  12533  elz2  12604  mul2lt0bi  13119  xaddnemnf  13257  xaddnepnf  13258  rexmul  13292  xlemul1a  13309  xrsupsslem  13328  xrinfmsslem  13329  ixxun  13383  fzsplit2  13573  fzsuc2  13606  elfzp12  13627  seqf1olem2  14074  expp1  14100  expneg  14101  expcllem  14104  mulexpz  14134  expaddz  14138  expmulz  14140  zzlesq  14238  faclbnd4lem3  14327  faclbnd4lem4  14328  faclbnd4  14329  bcpasc  14353  ccatass  14622  ccatrn  14623  ccatswrd  14702  ccatpfx  14734  cats1un  14754  revccat  14799  summo  15764  sumss2  15773  fsumsplit  15788  geomulcvg  15926  fprodsplit  16016  bpoly2  16106  bpoly3  16107  ef0lem  16127  odd2np1  16394  sadcaddlem  16510  gcdcllem3  16554  dvdslcm  16651  lcmeq0  16653  lcmcl  16654  lcmneg  16656  lcmgcd  16660  rpexp1i  16777  pcid  16928  4sqlem16  17015  funcres2c  17955  lubun  18566  mulgneg  19153  mulgnn0z  19162  frgpup3lem  19842  gsumzunsnd  20021  gsumunsnfd  20022  dprddisj2  20106  dmdprdsplit2  20113  dprdsplit  20115  gsumdixp  20396  lssvs0or  21234  evlslem4  22227  refun0  23672  txhaus  23804  xkoptsub  23811  ptunhmeo  23965  xpsxmetlem  24536  xpsmet  24539  mbfss  25805  itg1addlem2  25856  iblss2  25965  itgsplit  25995  limcres  26045  ftc1lem5  26199  coe1mul3  26256  dgrlt  26423  abelthlem3  26596  atanlogaddlem  27078  atanlogsub  27081  atans2  27096  efrlim  27134  bposlem2  27449  lgsdir2lem4  27492  2sqb  27596  pntpbnd1  27750  ostthlem1  27791  nosepdm  27848  nosupbnd2lem1  27879  negsid  28234  elzn0s  28591  zsbday  28599  zcuts  28600  expsp1  28622  hlbtwn  28883  cgracol  29139  inaghl  29162  brbtwn2  29255  axcontlem2  29315  ifnebib  32895  isoun  33047  eliccelico  33122  elicoelioo  33123  fzsplit3  33138  prodpr  33170  zarclsun  34260  xrge0iifhom  34327  esumsplit  34443  esumpad2  34446  sibfinima  34729  circlemethhgt  35030  bnj1137  35383  subfacp1lem4  35675  subfacp1lem5  35676  mclsax  36061  poimirlem2  38293  poimirlem8  38299  poimirlem22  38313  poimirlem28  38319  ftc1cnnc  38363  ftc1anclem2  38365  fdc  38416  incsequz2  38420  unichnidl  38702  lkrss2N  39963  cdlemg27b  41490  tendoex  41769  dihmeetlem2N  42093  dvh3dim3N  42243  aks6d1c2p2  42906  hashscontpow  42909  aks6d1c5  42926  sticksstones1  42933  sticksstones2  42934  unitscyglem2  42983  ofun  43026  sn-nnne0  43254  nn0addcom  43256  nn0mulcom  43260  zmulcomlem  43261  rexzrexnn0  43551  pell14qrexpcl  43614  elpell1qr2  43619  acongeq  43730  jm2.23  43743  rpnnen3  43779  mnringmulrcld  44972  mnuprdlem3  45004  radcnvrat  45044  sumpair  45775  cncfiooicclem1  46627  fourierdlem80  46920  fourierdlem93  46933  fullthinc  50248