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  5411  relop  5841  poltletr  6132  ordnbtwn  6457  eqfnun  7037  oeoa  8617  oeoe  8619  ssnnfi  9191  domnsymfi  9222  phplem3OLD  9238  unwdomg  9606  numwdom  10081  infpssrlem5  10329  fin23lem24  10344  fin23lem28  10362  fin1a2lem10  10431  zornn0g  10527  gchdomtri  10651  fpwwe2lem11  10663  fpwwe2lem12  10664  msqgt0  11765  recextlem2  11876  lemul1a  12103  nnne0  12282  nnnn0addcl  12539  un0addcl  12542  un0mulcl  12543  elz2  12614  mul2lt0bi  13123  xaddnemnf  13260  xaddnepnf  13261  rexmul  13295  xlemul1a  13312  xrsupsslem  13331  xrinfmsslem  13332  ixxun  13385  fzsplit2  13571  fzsuc2  13604  elfzp12  13625  seqf1olem2  14065  expp1  14091  expneg  14092  expcllem  14095  mulexpz  14125  expaddz  14129  expmulz  14131  zzlesq  14227  faclbnd4lem3  14316  faclbnd4lem4  14317  faclbnd4  14318  bcpasc  14342  ccatass  14608  ccatrn  14609  ccatswrd  14688  ccatpfx  14721  cats1un  14741  revccat  14786  summo  15735  sumss2  15744  fsumsplit  15759  geomulcvg  15894  fprodsplit  15984  bpoly2  16075  bpoly3  16076  ef0lem  16096  odd2np1  16360  sadcaddlem  16476  gcdcllem3  16520  dvdslcm  16617  lcmeq0  16619  lcmcl  16620  lcmneg  16622  lcmgcd  16626  rpexp1i  16742  pcid  16893  4sqlem16  16980  funcres2c  17919  lubun  18529  mulgneg  19079  mulgnn0z  19088  frgpup3lem  19763  gsumzunsnd  19942  gsumunsnfd  19943  dprddisj2  20027  dmdprdsplit2  20034  dprdsplit  20036  gsumdixp  20284  lssvs0or  21080  evlslem4  22048  refun0  23469  txhaus  23601  xkoptsub  23608  ptunhmeo  23762  xpsxmetlem  24334  xpsmet  24337  mbfss  25617  itg1addlem2  25668  iblss2  25777  itgsplit  25807  limcres  25857  ftc1lem5  26017  coe1mul3  26074  dgrlt  26242  abelthlem3  26413  atanlogaddlem  26892  atanlogsub  26895  atans2  26910  efrlim  26948  efrlimOLD  26949  bposlem2  27265  lgsdir2lem4  27308  2sqb  27412  pntpbnd1  27566  ostthlem1  27607  nosepdm  27665  nosupbnd2lem1  27696  negsid  28009  elzn0s  28320  zsbday  28328  zscut  28329  expsp1  28348  hlbtwn  28555  cgracol  28772  inaghl  28789  brbtwn2  28850  axcontlem2  28910  ifnebib  32497  isoun  32646  eliccelico  32718  elicoelioo  32719  fzsplit3  32734  prodpr  32768  zarclsun  33828  xrge0iifhom  33895  esumsplit  34013  esumpad2  34016  sibfinima  34300  circlemethhgt  34617  bnj1137  34968  subfacp1lem4  35147  subfacp1lem5  35148  mclsax  35533  poimirlem2  37588  poimirlem8  37594  poimirlem22  37608  poimirlem28  37614  ftc1cnnc  37658  ftc1anclem2  37660  fdc  37711  incsequz2  37715  unichnidl  37997  lkrss2N  39129  cdlemg27b  40657  tendoex  40936  dihmeetlem2N  41260  dvh3dim3N  41410  aks6d1c2p2  42079  hashscontpow  42082  aks6d1c5  42099  sticksstones1  42106  sticksstones2  42107  unitscyglem2  42156  metakunt9  42173  ofun  42235  sn-nnne0  42441  nn0addcom  42443  nn0mulcom  42447  zmulcomlem  42448  rexzrexnn0  42778  pell14qrexpcl  42841  elpell1qr2  42846  acongeq  42958  jm2.23  42971  rpnnen3  43007  mnringmulrcld  44204  mnuprdlem3  44250  radcnvrat  44290  sumpair  44997  cncfiooicclem1  45865  fourierdlem80  46158  fourierdlem93  46171  fullthinc  49077