Theorem jaodan 965

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  mpjaodan  966  andi  1015  ccase  1043  axprOLD  5361  relop  5792  poltletr  6082  ordnbtwn  6405  eqfnun  6978  oeoa  8523  oeoe  8525  ssnnfi  9094  domnsymfi  9124  unwdomg  9489  numwdom  9972  infpssrlem5  10220  fin23lem24  10235  fin23lem28  10253  fin1a2lem10  10322  zornn0g  10418  gchdomtri  10543  fpwwe2lem11  10555  fpwwe2lem12  10556  msqgt0  11661  recextlem2  11772  lemul1a  12000  nnne0  12202  nnnn0addcl  12458  un0addcl  12461  un0mulcl  12462  elz2  12533  mul2lt0bi  13041  xaddnemnf  13179  xaddnepnf  13180  rexmul  13214  xlemul1a  13231  xrsupsslem  13250  xrinfmsslem  13251  ixxun  13305  fzsplit2  13494  fzsuc2  13527  elfzp12  13548  seqf1olem2  13995  expp1  14021  expneg  14022  expcllem  14025  mulexpz  14055  expaddz  14059  expmulz  14061  zzlesq  14159  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd4  14250  bcpasc  14274  ccatass  14542  ccatrn  14543  ccatswrd  14622  ccatpfx  14654  cats1un  14674  revccat  14719  summo  15670  sumss2  15679  fsumsplit  15694  geomulcvg  15832  fprodsplit  15922  bpoly2  16013  bpoly3  16014  ef0lem  16034  odd2np1  16301  sadcaddlem  16417  gcdcllem3  16461  dvdslcm  16558  lcmeq0  16560  lcmcl  16561  lcmneg  16563  lcmgcd  16567  rpexp1i  16684  pcid  16835  4sqlem16  16922  funcres2c  17861  lubun  18472  mulgneg  19059  mulgnn0z  19068  frgpup3lem  19743  gsumzunsnd  19922  gsumunsnfd  19923  dprddisj2  20007  dmdprdsplit2  20014  dprdsplit  20016  gsumdixp  20289  lssvs0or  21103  evlslem4  22052  refun0  23498  txhaus  23630  xkoptsub  23637  ptunhmeo  23791  xpsxmetlem  24362  xpsmet  24365  mbfss  25631  itg1addlem2  25682  iblss2  25791  itgsplit  25821  limcres  25871  ftc1lem5  26025  coe1mul3  26082  dgrlt  26249  abelthlem3  26416  atanlogaddlem  26895  atanlogsub  26898  atans2  26913  efrlim  26951  bposlem2  27266  lgsdir2lem4  27309  2sqb  27413  pntpbnd1  27567  ostthlem1  27608  nosepdm  27666  nosupbnd2lem1  27697  negsid  28051  elzn0s  28408  zsbday  28416  zcuts  28417  expsp1  28439  hlbtwn  28697  cgracol  28914  inaghl  28931  brbtwn2  28992  axcontlem2  29052  ifnebib  32637  isoun  32794  eliccelico  32869  elicoelioo  32870  fzsplit3  32885  prodpr  32918  zarclsun  34054  xrge0iifhom  34121  esumsplit  34237  esumpad2  34240  sibfinima  34523  circlemethhgt  34827  bnj1137  35177  subfacp1lem4  35411  subfacp1lem5  35412  mclsax  35797  poimirlem2  37989  poimirlem8  37995  poimirlem22  38009  poimirlem28  38015  ftc1cnnc  38059  ftc1anclem2  38061  fdc  38112  incsequz2  38116  unichnidl  38398  lkrss2N  39661  cdlemg27b  41188  tendoex  41467  dihmeetlem2N  41791  dvh3dim3N  41941  aks6d1c2p2  42604  hashscontpow  42607  aks6d1c5  42624  sticksstones1  42631  sticksstones2  42632  unitscyglem2  42681  ofun  42722  sn-nnne0  42950  nn0addcom  42952  nn0mulcom  42956  zmulcomlem  42957  rexzrexnn0  43249  pell14qrexpcl  43312  elpell1qr2  43317  acongeq  43428  jm2.23  43441  rpnnen3  43477  mnringmulrcld  44672  mnuprdlem3  44718  radcnvrat  44758  sumpair  45483  cncfiooicclem1  46336  fourierdlem80  46629  fourierdlem93  46642  fullthinc  49940