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  1023  ccase  1051  axprOLD  5404  relop  5837  poltletr  6133  ordnbtwn  6457  eqfnun  7033  oeoa  8583  oeoe  8585  ssnnfi  9154  domnsymfi  9184  unwdomg  9546  numwdom  10043  infpssrlem5  10291  fin23lem24  10306  fin23lem28  10324  fin1a2lem10  10393  zornn0g  10489  gchdomtri  10614  fpwwe2lem11  10626  fpwwe2lem12  10627  msqgt0  11734  recextlem2  11845  lemul1a  12069  nnne0  12270  nnnn0addcl  12534  un0addcl  12537  un0mulcl  12538  elz2  12609  mul2lt0bi  13124  xaddnemnf  13262  xaddnepnf  13263  rexmul  13297  xlemul1a  13314  xrsupsslem  13333  xrinfmsslem  13334  ixxun  13388  fzsplit2  13577  fzsuc2  13610  elfzp12  13631  seqf1olem2  14078  expp1  14104  expneg  14105  expcllem  14108  mulexpz  14138  expaddz  14142  expmulz  14144  zzlesq  14242  faclbnd4lem3  14331  faclbnd4lem4  14332  faclbnd4  14333  bcpasc  14357  ccatass  14626  ccatrn  14627  ccatswrd  14706  ccatpfx  14738  cats1un  14758  revccat  14803  summo  15768  sumss2  15777  fsumsplit  15792  geomulcvg  15930  fprodsplit  16020  bpoly2  16111  bpoly3  16112  ef0lem  16132  odd2np1  16399  sadcaddlem  16515  gcdcllem3  16559  dvdslcm  16656  lcmeq0  16658  lcmcl  16659  lcmneg  16661  lcmgcd  16665  rpexp1i  16782  pcid  16933  4sqlem16  17020  funcres2c  17960  lubun  18571  mulgneg  19158  mulgnn0z  19167  frgpup3lem  19847  gsumzunsnd  20026  gsumunsnfd  20027  dprddisj2  20111  dmdprdsplit2  20118  dprdsplit  20120  gsumdixp  20400  lssvs0or  21212  evlslem4  22196  refun0  23641  txhaus  23773  xkoptsub  23780  ptunhmeo  23934  xpsxmetlem  24505  xpsmet  24508  mbfss  25774  itg1addlem2  25825  iblss2  25934  itgsplit  25964  limcres  26014  ftc1lem5  26168  coe1mul3  26225  dgrlt  26392  abelthlem3  26562  atanlogaddlem  27044  atanlogsub  27047  atans2  27062  efrlim  27100  bposlem2  27415  lgsdir2lem4  27458  2sqb  27562  pntpbnd1  27716  ostthlem1  27757  nosepdm  27814  nosupbnd2lem1  27845  negsid  28200  elzn0s  28557  zsbday  28565  zcuts  28566  expsp1  28588  hlbtwn  28846  cgracol  29096  inaghl  29117  brbtwn2  29196  axcontlem2  29256  ifnebib  32836  isoun  32988  eliccelico  33063  elicoelioo  33064  fzsplit3  33079  prodpr  33111  zarclsun  34205  xrge0iifhom  34272  esumsplit  34388  esumpad2  34391  sibfinima  34674  circlemethhgt  34975  bnj1137  35328  subfacp1lem4  35574  subfacp1lem5  35575  mclsax  35960  poimirlem2  38161  poimirlem8  38167  poimirlem22  38181  poimirlem28  38187  ftc1cnnc  38231  ftc1anclem2  38233  fdc  38284  incsequz2  38288  unichnidl  38570  lkrss2N  39833  cdlemg27b  41360  tendoex  41639  dihmeetlem2N  41963  dvh3dim3N  42113  aks6d1c2p2  42776  hashscontpow  42779  aks6d1c5  42796  sticksstones1  42803  sticksstones2  42804  unitscyglem2  42853  ofun  42896  sn-nnne0  43124  nn0addcom  43126  nn0mulcom  43130  zmulcomlem  43131  rexzrexnn0  43423  pell14qrexpcl  43486  elpell1qr2  43491  acongeq  43602  jm2.23  43615  rpnnen3  43651  mnringmulrcld  44844  mnuprdlem3  44876  radcnvrat  44916  sumpair  45647  cncfiooicclem1  46499  fourierdlem80  46792  fourierdlem93  46805  fullthinc  50113