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  5378  relop  5807  poltletr  6097  ordnbtwn  6420  eqfnun  6991  oeoa  8535  oeoe  8537  ssnnfi  9106  domnsymfi  9136  unwdomg  9501  numwdom  9981  infpssrlem5  10229  fin23lem24  10244  fin23lem28  10262  fin1a2lem10  10331  zornn0g  10427  gchdomtri  10552  fpwwe2lem11  10564  fpwwe2lem12  10565  msqgt0  11669  recextlem2  11780  lemul1a  12007  nnne0  12191  nnnn0addcl  12443  un0addcl  12446  un0mulcl  12447  elz2  12518  mul2lt0bi  13025  xaddnemnf  13163  xaddnepnf  13164  rexmul  13198  xlemul1a  13215  xrsupsslem  13234  xrinfmsslem  13235  ixxun  13289  fzsplit2  13477  fzsuc2  13510  elfzp12  13531  seqf1olem2  13977  expp1  14003  expneg  14004  expcllem  14007  mulexpz  14037  expaddz  14041  expmulz  14043  zzlesq  14141  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd4  14232  bcpasc  14256  ccatass  14524  ccatrn  14525  ccatswrd  14604  ccatpfx  14636  cats1un  14656  revccat  14701  summo  15652  sumss2  15661  fsumsplit  15676  geomulcvg  15811  fprodsplit  15901  bpoly2  15992  bpoly3  15993  ef0lem  16013  odd2np1  16280  sadcaddlem  16396  gcdcllem3  16440  dvdslcm  16537  lcmeq0  16539  lcmcl  16540  lcmneg  16542  lcmgcd  16546  rpexp1i  16662  pcid  16813  4sqlem16  16900  funcres2c  17839  lubun  18450  mulgneg  19034  mulgnn0z  19043  frgpup3lem  19718  gsumzunsnd  19897  gsumunsnfd  19898  dprddisj2  19982  dmdprdsplit2  19989  dprdsplit  19991  gsumdixp  20266  lssvs0or  21077  evlslem4  22043  refun0  23471  txhaus  23603  xkoptsub  23610  ptunhmeo  23764  xpsxmetlem  24335  xpsmet  24338  mbfss  25615  itg1addlem2  25666  iblss2  25775  itgsplit  25805  limcres  25855  ftc1lem5  26015  coe1mul3  26072  dgrlt  26240  abelthlem3  26411  atanlogaddlem  26891  atanlogsub  26894  atans2  26909  efrlim  26947  efrlimOLD  26948  bposlem2  27264  lgsdir2lem4  27307  2sqb  27411  pntpbnd1  27565  ostthlem1  27606  nosepdm  27664  nosupbnd2lem1  27695  negsid  28049  elzn0s  28406  zsbday  28414  zcuts  28415  expsp1  28437  hlbtwn  28695  cgracol  28912  inaghl  28929  brbtwn2  28990  axcontlem2  29050  ifnebib  32636  isoun  32792  eliccelico  32868  elicoelioo  32869  fzsplit3  32884  prodpr  32918  zarclsun  34048  xrge0iifhom  34115  esumsplit  34231  esumpad2  34234  sibfinima  34517  circlemethhgt  34821  bnj1137  35171  subfacp1lem4  35399  subfacp1lem5  35400  mclsax  35785  poimirlem2  37873  poimirlem8  37879  poimirlem22  37893  poimirlem28  37899  ftc1cnnc  37943  ftc1anclem2  37945  fdc  37996  incsequz2  38000  unichnidl  38282  lkrss2N  39545  cdlemg27b  41072  tendoex  41351  dihmeetlem2N  41675  dvh3dim3N  41825  aks6d1c2p2  42489  hashscontpow  42492  aks6d1c5  42509  sticksstones1  42516  sticksstones2  42517  unitscyglem2  42566  ofun  42608  sn-nnne0  42830  nn0addcom  42832  nn0mulcom  42836  zmulcomlem  42837  rexzrexnn0  43161  pell14qrexpcl  43224  elpell1qr2  43229  acongeq  43340  jm2.23  43353  rpnnen3  43389  mnringmulrcld  44584  mnuprdlem3  44630  radcnvrat  44670  sumpair  45395  cncfiooicclem1  46251  fourierdlem80  46544  fourierdlem93  46557  fullthinc  49809