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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  mpjaodan  973  andi  1025  ccase  1053  axprOLD  5405  relop  5838  poltletr  6134  ordnbtwn  6460  eqfnun  7036  oeoa  8589  oeoe  8591  ssnnfi  9161  domnsymfi  9191  unwdomg  9553  numwdom  10059  infpssrlem5  10306  fin23lem24  10321  fin23lem28  10339  fin1a2lem10  10408  zornn0g  10504  gchdomtri  10631  fpwwe2lem11  10643  fpwwe2lem12  10644  msqgt0  11751  recextlem2  11862  lemul1a  12086  nnne0  12287  nnnn0addcl  12551  un0addcl  12554  un0mulcl  12555  elz2  12626  mul2lt0bi  13142  xaddnemnf  13280  xaddnepnf  13281  rexmul  13315  xlemul1a  13332  xrsupsslem  13351  xrinfmsslem  13352  ixxun  13406  fzsplit2  13596  fzsuc2  13629  elfzp12  13650  seqf1olem2  14098  expp1  14124  expneg  14125  expcllem  14128  mulexpz  14158  expaddz  14162  expmulz  14164  zzlesq  14262  faclbnd4lem3  14351  faclbnd4lem4  14352  faclbnd4  14353  bcpasc  14377  ccatass  14646  ccatrn  14647  ccatswrd  14730  ccatpfx  14762  cats1un  14782  revccat  14827  summo  15793  sumss2  15802  fsumsplit  15817  geomulcvg  15955  fprodsplit  16045  bpoly2  16135  bpoly3  16136  ef0lem  16156  odd2np1  16423  sadcaddlem  16539  gcdcllem3  16583  dvdslcm  16680  lcmeq0  16682  lcmcl  16683  lcmneg  16685  lcmgcd  16689  rpexp1i  16806  pcid  16957  4sqlem16  17044  funcres2c  17984  lubun  18595  mulgneg  19204  mulgnn0z  19213  frgpup3lem  19893  gsumzunsnd  20072  gsumunsnfd  20073  dprddisj2  20157  dmdprdsplit2  20164  dprdsplit  20166  gsumdixp  20448  lssvs0or  21286  evlslem4  22279  refun0  23725  txhaus  23857  xkoptsub  23864  ptunhmeo  24018  xpsxmetlem  24589  xpsmet  24592  mbfss  25858  itg1addlem2  25909  iblss2  26018  itgsplit  26048  limcres  26098  ftc1lem5  26252  coe1mul3  26309  dgrlt  26476  abelthlem3  26649  atanlogaddlem  27131  atanlogsub  27134  atans2  27149  efrlim  27187  bposlem2  27502  lgsdir2lem4  27545  2sqb  27649  pntpbnd1  27803  ostthlem1  27844  nosepdm  27901  nosupbnd2lem1  27932  negsid  28287  elzn0s  28644  zsbday  28652  zcuts  28653  expsp1  28675  hlbtwn  28936  cgracol  29192  inaghl  29219  brbtwn2  29312  axcontlem2  29372  ifnebib  32968  isoun  33120  eliccelico  33194  elicoelioo  33195  fzsplit3  33210  prodpr  33242  zarclsun  34326  xrge0iifhom  34393  esumsplit  34509  esumpad2  34512  sibfinima  34796  circlemethhgt  35097  bnj1137  35450  subfacp1lem4  35714  subfacp1lem5  35715  mclsax  36100  poimirlem2  38332  poimirlem8  38338  poimirlem22  38352  poimirlem28  38358  ftc1cnnc  38402  ftc1anclem2  38404  fdc  38456  incsequz2  38460  unichnidl  38742  lkrss2N  40003  cdlemg27b  41530  tendoex  41809  dihmeetlem2N  42133  dvh3dim3N  42283  aks6d1c2p2  42946  hashscontpow  42949  aks6d1c5  42966  sticksstones1  42973  sticksstones2  42974  unitscyglem2  43023  ofun  43066  sn-nnne0  43294  nn0addcom  43296  nn0mulcom  43300  zmulcomlem  43301  rexzrexnn0  43591  pell14qrexpcl  43654  elpell1qr2  43659  acongeq  43770  jm2.23  43783  rpnnen3  43819  mnringmulrcld  45012  mnuprdlem3  45044  radcnvrat  45084  sumpair  45815  cncfiooicclem1  46667  fourierdlem80  46960  fourierdlem93  46973  fullthinc  50287