Theorem jaodan 960

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

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

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 849

This theorem is referenced by:  mpjaodan  961  andi  1010  ccase  1038  axprOLD  5367  relop  5797  poltletr  6087  ordnbtwn  6410  eqfnun  6981  oeoa  8524  oeoe  8526  ssnnfi  9095  domnsymfi  9125  unwdomg  9490  numwdom  9970  infpssrlem5  10218  fin23lem24  10233  fin23lem28  10251  fin1a2lem10  10320  zornn0g  10416  gchdomtri  10541  fpwwe2lem11  10553  fpwwe2lem12  10554  msqgt0  11658  recextlem2  11769  lemul1a  11996  nnne0  12180  nnnn0addcl  12432  un0addcl  12435  un0mulcl  12436  elz2  12507  mul2lt0bi  13014  xaddnemnf  13152  xaddnepnf  13153  rexmul  13187  xlemul1a  13204  xrsupsslem  13223  xrinfmsslem  13224  ixxun  13278  fzsplit2  13466  fzsuc2  13499  elfzp12  13520  seqf1olem2  13966  expp1  13992  expneg  13993  expcllem  13996  mulexpz  14026  expaddz  14030  expmulz  14032  zzlesq  14130  faclbnd4lem3  14219  faclbnd4lem4  14220  faclbnd4  14221  bcpasc  14245  ccatass  14513  ccatrn  14514  ccatswrd  14593  ccatpfx  14625  cats1un  14645  revccat  14690  summo  15641  sumss2  15650  fsumsplit  15665  geomulcvg  15800  fprodsplit  15890  bpoly2  15981  bpoly3  15982  ef0lem  16002  odd2np1  16269  sadcaddlem  16385  gcdcllem3  16429  dvdslcm  16526  lcmeq0  16528  lcmcl  16529  lcmneg  16531  lcmgcd  16535  rpexp1i  16651  pcid  16802  4sqlem16  16889  funcres2c  17828  lubun  18439  mulgneg  19026  mulgnn0z  19035  frgpup3lem  19710  gsumzunsnd  19889  gsumunsnfd  19890  dprddisj2  19974  dmdprdsplit2  19981  dprdsplit  19983  gsumdixp  20256  lssvs0or  21067  evlslem4  22032  refun0  23458  txhaus  23590  xkoptsub  23597  ptunhmeo  23751  xpsxmetlem  24322  xpsmet  24325  mbfss  25591  itg1addlem2  25642  iblss2  25751  itgsplit  25781  limcres  25831  ftc1lem5  25988  coe1mul3  26045  dgrlt  26212  abelthlem3  26383  atanlogaddlem  26863  atanlogsub  26866  atans2  26881  efrlim  26919  efrlimOLD  26920  bposlem2  27236  lgsdir2lem4  27279  2sqb  27383  pntpbnd1  27537  ostthlem1  27578  nosepdm  27636  nosupbnd2lem1  27667  negsid  28021  elzn0s  28378  zsbday  28386  zcuts  28387  expsp1  28409  hlbtwn  28667  cgracol  28884  inaghl  28901  brbtwn2  28962  axcontlem2  29022  ifnebib  32608  isoun  32764  eliccelico  32840  elicoelioo  32841  fzsplit3  32856  prodpr  32890  zarclsun  34020  xrge0iifhom  34087  esumsplit  34203  esumpad2  34206  sibfinima  34489  circlemethhgt  34793  bnj1137  35143  subfacp1lem4  35371  subfacp1lem5  35372  mclsax  35757  poimirlem2  37934  poimirlem8  37940  poimirlem22  37954  poimirlem28  37960  ftc1cnnc  38004  ftc1anclem2  38006  fdc  38057  incsequz2  38061  unichnidl  38343  lkrss2N  39606  cdlemg27b  41133  tendoex  41412  dihmeetlem2N  41736  dvh3dim3N  41886  aks6d1c2p2  42550  hashscontpow  42553  aks6d1c5  42570  sticksstones1  42577  sticksstones2  42578  unitscyglem2  42627  ofun  42669  sn-nnne0  42904  nn0addcom  42906  nn0mulcom  42910  zmulcomlem  42911  rexzrexnn0  43235  pell14qrexpcl  43298  elpell1qr2  43303  acongeq  43414  jm2.23  43427  rpnnen3  43463  mnringmulrcld  44658  mnuprdlem3  44704  radcnvrat  44744  sumpair  45469  cncfiooicclem1  46325  fourierdlem80  46618  fourierdlem93  46631  fullthinc  49883