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  5367  relop  5789  poltletr  6078  ordnbtwn  6401  eqfnun  6970  oeoa  8512  oeoe  8514  ssnnfi  9079  domnsymfi  9109  unwdomg  9470  numwdom  9950  infpssrlem5  10198  fin23lem24  10213  fin23lem28  10231  fin1a2lem10  10300  zornn0g  10396  gchdomtri  10520  fpwwe2lem11  10532  fpwwe2lem12  10533  msqgt0  11637  recextlem2  11748  lemul1a  11975  nnne0  12159  nnnn0addcl  12411  un0addcl  12414  un0mulcl  12415  elz2  12486  mul2lt0bi  12998  xaddnemnf  13135  xaddnepnf  13136  rexmul  13170  xlemul1a  13187  xrsupsslem  13206  xrinfmsslem  13207  ixxun  13261  fzsplit2  13449  fzsuc2  13482  elfzp12  13503  seqf1olem2  13949  expp1  13975  expneg  13976  expcllem  13979  mulexpz  14009  expaddz  14013  expmulz  14015  zzlesq  14113  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd4  14204  bcpasc  14228  ccatass  14496  ccatrn  14497  ccatswrd  14576  ccatpfx  14608  cats1un  14628  revccat  14673  summo  15624  sumss2  15633  fsumsplit  15648  geomulcvg  15783  fprodsplit  15873  bpoly2  15964  bpoly3  15965  ef0lem  15985  odd2np1  16252  sadcaddlem  16368  gcdcllem3  16412  dvdslcm  16509  lcmeq0  16511  lcmcl  16512  lcmneg  16514  lcmgcd  16518  rpexp1i  16634  pcid  16785  4sqlem16  16872  funcres2c  17810  lubun  18421  mulgneg  19005  mulgnn0z  19014  frgpup3lem  19689  gsumzunsnd  19868  gsumunsnfd  19869  dprddisj2  19953  dmdprdsplit2  19960  dprdsplit  19962  gsumdixp  20237  lssvs0or  21047  evlslem4  22011  refun0  23430  txhaus  23562  xkoptsub  23569  ptunhmeo  23723  xpsxmetlem  24294  xpsmet  24297  mbfss  25574  itg1addlem2  25625  iblss2  25734  itgsplit  25764  limcres  25814  ftc1lem5  25974  coe1mul3  26031  dgrlt  26199  abelthlem3  26370  atanlogaddlem  26850  atanlogsub  26853  atans2  26868  efrlim  26906  efrlimOLD  26907  bposlem2  27223  lgsdir2lem4  27266  2sqb  27370  pntpbnd1  27524  ostthlem1  27565  nosepdm  27623  nosupbnd2lem1  27654  negsid  27983  elzn0s  28322  zsbday  28330  zscut  28331  expsp1  28352  hlbtwn  28589  cgracol  28806  inaghl  28823  brbtwn2  28883  axcontlem2  28943  ifnebib  32529  isoun  32683  eliccelico  32760  elicoelioo  32761  fzsplit3  32776  prodpr  32809  zarclsun  33883  xrge0iifhom  33950  esumsplit  34066  esumpad2  34069  sibfinima  34352  circlemethhgt  34656  bnj1137  35007  subfacp1lem4  35227  subfacp1lem5  35228  mclsax  35613  poimirlem2  37672  poimirlem8  37678  poimirlem22  37692  poimirlem28  37698  ftc1cnnc  37742  ftc1anclem2  37744  fdc  37795  incsequz2  37799  unichnidl  38081  lkrss2N  39278  cdlemg27b  40805  tendoex  41084  dihmeetlem2N  41408  dvh3dim3N  41558  aks6d1c2p2  42222  hashscontpow  42225  aks6d1c5  42242  sticksstones1  42249  sticksstones2  42250  unitscyglem2  42299  ofun  42339  sn-nnne0  42563  nn0addcom  42565  nn0mulcom  42569  zmulcomlem  42570  rexzrexnn0  42907  pell14qrexpcl  42970  elpell1qr2  42975  acongeq  43086  jm2.23  43099  rpnnen3  43135  mnringmulrcld  44331  mnuprdlem3  44377  radcnvrat  44417  sumpair  45142  cncfiooicclem1  46001  fourierdlem80  46294  fourierdlem93  46307  fullthinc  49561