Theorem jaodan 959

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

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

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 848

This theorem is referenced by:  mpjaodan  960  andi  1009  ccase  1037  axprOLD  5389  relop  5817  poltletr  6108  ordnbtwn  6430  eqfnun  7012  oeoa  8564  oeoe  8566  ssnnfi  9139  domnsymfi  9170  unwdomg  9544  numwdom  10019  infpssrlem5  10267  fin23lem24  10282  fin23lem28  10300  fin1a2lem10  10369  zornn0g  10465  gchdomtri  10589  fpwwe2lem11  10601  fpwwe2lem12  10602  msqgt0  11705  recextlem2  11816  lemul1a  12043  nnne0  12227  nnnn0addcl  12479  un0addcl  12482  un0mulcl  12483  elz2  12554  mul2lt0bi  13066  xaddnemnf  13203  xaddnepnf  13204  rexmul  13238  xlemul1a  13255  xrsupsslem  13274  xrinfmsslem  13275  ixxun  13329  fzsplit2  13517  fzsuc2  13550  elfzp12  13571  seqf1olem2  14014  expp1  14040  expneg  14041  expcllem  14044  mulexpz  14074  expaddz  14078  expmulz  14080  zzlesq  14178  faclbnd4lem3  14267  faclbnd4lem4  14268  faclbnd4  14269  bcpasc  14293  ccatass  14560  ccatrn  14561  ccatswrd  14640  ccatpfx  14673  cats1un  14693  revccat  14738  summo  15690  sumss2  15699  fsumsplit  15714  geomulcvg  15849  fprodsplit  15939  bpoly2  16030  bpoly3  16031  ef0lem  16051  odd2np1  16318  sadcaddlem  16434  gcdcllem3  16478  dvdslcm  16575  lcmeq0  16577  lcmcl  16578  lcmneg  16580  lcmgcd  16584  rpexp1i  16700  pcid  16851  4sqlem16  16938  funcres2c  17872  lubun  18481  mulgneg  19031  mulgnn0z  19040  frgpup3lem  19714  gsumzunsnd  19893  gsumunsnfd  19894  dprddisj2  19978  dmdprdsplit2  19985  dprdsplit  19987  gsumdixp  20235  lssvs0or  21027  evlslem4  21990  refun0  23409  txhaus  23541  xkoptsub  23548  ptunhmeo  23702  xpsxmetlem  24274  xpsmet  24277  mbfss  25554  itg1addlem2  25605  iblss2  25714  itgsplit  25744  limcres  25794  ftc1lem5  25954  coe1mul3  26011  dgrlt  26179  abelthlem3  26350  atanlogaddlem  26830  atanlogsub  26833  atans2  26848  efrlim  26886  efrlimOLD  26887  bposlem2  27203  lgsdir2lem4  27246  2sqb  27350  pntpbnd1  27504  ostthlem1  27545  nosepdm  27603  nosupbnd2lem1  27634  negsid  27954  elzn0s  28293  zsbday  28301  zscut  28302  expsp1  28322  hlbtwn  28545  cgracol  28762  inaghl  28779  brbtwn2  28839  axcontlem2  28899  ifnebib  32485  isoun  32632  eliccelico  32707  elicoelioo  32708  fzsplit3  32723  prodpr  32758  zarclsun  33867  xrge0iifhom  33934  esumsplit  34050  esumpad2  34053  sibfinima  34337  circlemethhgt  34641  bnj1137  34992  subfacp1lem4  35177  subfacp1lem5  35178  mclsax  35563  poimirlem2  37623  poimirlem8  37629  poimirlem22  37643  poimirlem28  37649  ftc1cnnc  37693  ftc1anclem2  37695  fdc  37746  incsequz2  37750  unichnidl  38032  lkrss2N  39169  cdlemg27b  40697  tendoex  40976  dihmeetlem2N  41300  dvh3dim3N  41450  aks6d1c2p2  42114  hashscontpow  42117  aks6d1c5  42134  sticksstones1  42141  sticksstones2  42142  unitscyglem2  42191  ofun  42231  sn-nnne0  42455  nn0addcom  42457  nn0mulcom  42461  zmulcomlem  42462  rexzrexnn0  42799  pell14qrexpcl  42862  elpell1qr2  42867  acongeq  42979  jm2.23  42992  rpnnen3  43028  mnringmulrcld  44224  mnuprdlem3  44270  radcnvrat  44310  sumpair  45036  cncfiooicclem1  45898  fourierdlem80  46191  fourierdlem93  46204  fullthinc  49443