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  5376  relop  5799  poltletr  6089  ordnbtwn  6412  eqfnun  6982  oeoa  8525  oeoe  8527  ssnnfi  9094  domnsymfi  9124  unwdomg  9489  numwdom  9969  infpssrlem5  10217  fin23lem24  10232  fin23lem28  10250  fin1a2lem10  10319  zornn0g  10415  gchdomtri  10540  fpwwe2lem11  10552  fpwwe2lem12  10553  msqgt0  11657  recextlem2  11768  lemul1a  11995  nnne0  12179  nnnn0addcl  12431  un0addcl  12434  un0mulcl  12435  elz2  12506  mul2lt0bi  13013  xaddnemnf  13151  xaddnepnf  13152  rexmul  13186  xlemul1a  13203  xrsupsslem  13222  xrinfmsslem  13223  ixxun  13277  fzsplit2  13465  fzsuc2  13498  elfzp12  13519  seqf1olem2  13965  expp1  13991  expneg  13992  expcllem  13995  mulexpz  14025  expaddz  14029  expmulz  14031  zzlesq  14129  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd4  14220  bcpasc  14244  ccatass  14512  ccatrn  14513  ccatswrd  14592  ccatpfx  14624  cats1un  14644  revccat  14689  summo  15640  sumss2  15649  fsumsplit  15664  geomulcvg  15799  fprodsplit  15889  bpoly2  15980  bpoly3  15981  ef0lem  16001  odd2np1  16268  sadcaddlem  16384  gcdcllem3  16428  dvdslcm  16525  lcmeq0  16527  lcmcl  16528  lcmneg  16530  lcmgcd  16534  rpexp1i  16650  pcid  16801  4sqlem16  16888  funcres2c  17827  lubun  18438  mulgneg  19022  mulgnn0z  19031  frgpup3lem  19706  gsumzunsnd  19885  gsumunsnfd  19886  dprddisj2  19970  dmdprdsplit2  19977  dprdsplit  19979  gsumdixp  20254  lssvs0or  21065  evlslem4  22031  refun0  23459  txhaus  23591  xkoptsub  23598  ptunhmeo  23752  xpsxmetlem  24323  xpsmet  24326  mbfss  25603  itg1addlem2  25654  iblss2  25763  itgsplit  25793  limcres  25843  ftc1lem5  26003  coe1mul3  26060  dgrlt  26228  abelthlem3  26399  atanlogaddlem  26879  atanlogsub  26882  atans2  26897  efrlim  26935  efrlimOLD  26936  bposlem2  27252  lgsdir2lem4  27295  2sqb  27399  pntpbnd1  27553  ostthlem1  27594  nosepdm  27652  nosupbnd2lem1  27683  negsid  28037  elzn0s  28394  zsbday  28402  zcuts  28403  expsp1  28425  hlbtwn  28683  cgracol  28900  inaghl  28917  brbtwn2  28978  axcontlem2  29038  ifnebib  32624  isoun  32781  eliccelico  32857  elicoelioo  32858  fzsplit3  32873  prodpr  32907  zarclsun  34027  xrge0iifhom  34094  esumsplit  34210  esumpad2  34213  sibfinima  34496  circlemethhgt  34800  bnj1137  35151  subfacp1lem4  35377  subfacp1lem5  35378  mclsax  35763  poimirlem2  37823  poimirlem8  37829  poimirlem22  37843  poimirlem28  37849  ftc1cnnc  37893  ftc1anclem2  37895  fdc  37946  incsequz2  37950  unichnidl  38232  lkrss2N  39439  cdlemg27b  40966  tendoex  41245  dihmeetlem2N  41569  dvh3dim3N  41719  aks6d1c2p2  42383  hashscontpow  42386  aks6d1c5  42403  sticksstones1  42410  sticksstones2  42411  unitscyglem2  42460  ofun  42502  sn-nnne0  42725  nn0addcom  42727  nn0mulcom  42731  zmulcomlem  42732  rexzrexnn0  43056  pell14qrexpcl  43119  elpell1qr2  43124  acongeq  43235  jm2.23  43248  rpnnen3  43284  mnringmulrcld  44479  mnuprdlem3  44525  radcnvrat  44565  sumpair  45290  cncfiooicclem1  46147  fourierdlem80  46440  fourierdlem93  46453  fullthinc  49705