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  5436  relop  5863  poltletr  6154  ordnbtwn  6478  eqfnun  7056  oeoa  8633  oeoe  8635  ssnnfi  9207  domnsymfi  9237  phplem3OLD  9253  unwdomg  9621  numwdom  10096  infpssrlem5  10344  fin23lem24  10359  fin23lem28  10377  fin1a2lem10  10446  zornn0g  10542  gchdomtri  10666  fpwwe2lem11  10678  fpwwe2lem12  10679  msqgt0  11780  recextlem2  11891  lemul1a  12118  nnne0  12297  nnnn0addcl  12553  un0addcl  12556  un0mulcl  12557  elz2  12628  mul2lt0bi  13138  xaddnemnf  13274  xaddnepnf  13275  rexmul  13309  xlemul1a  13326  xrsupsslem  13345  xrinfmsslem  13346  ixxun  13399  fzsplit2  13585  fzsuc2  13618  elfzp12  13639  seqf1olem2  14079  expp1  14105  expneg  14106  expcllem  14109  mulexpz  14139  expaddz  14143  expmulz  14145  zzlesq  14241  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd4  14332  bcpasc  14356  ccatass  14622  ccatrn  14623  ccatswrd  14702  ccatpfx  14735  cats1un  14755  revccat  14800  summo  15749  sumss2  15758  fsumsplit  15773  geomulcvg  15908  fprodsplit  15998  bpoly2  16089  bpoly3  16090  ef0lem  16110  odd2np1  16374  sadcaddlem  16490  gcdcllem3  16534  dvdslcm  16631  lcmeq0  16633  lcmcl  16634  lcmneg  16636  lcmgcd  16640  rpexp1i  16756  pcid  16906  4sqlem16  16993  funcres2c  17954  lubun  18572  mulgneg  19122  mulgnn0z  19131  frgpup3lem  19809  gsumzunsnd  19988  gsumunsnfd  19989  dprddisj2  20073  dmdprdsplit2  20080  dprdsplit  20082  gsumdixp  20332  lssvs0or  21129  evlslem4  22117  refun0  23538  txhaus  23670  xkoptsub  23677  ptunhmeo  23831  xpsxmetlem  24404  xpsmet  24407  mbfss  25694  itg1addlem2  25745  iblss2  25855  itgsplit  25885  limcres  25935  ftc1lem5  26095  coe1mul3  26152  dgrlt  26320  abelthlem3  26491  atanlogaddlem  26970  atanlogsub  26973  atans2  26988  efrlim  27026  efrlimOLD  27027  bposlem2  27343  lgsdir2lem4  27386  2sqb  27490  pntpbnd1  27644  ostthlem1  27685  nosepdm  27743  nosupbnd2lem1  27774  negsid  28087  elzn0s  28398  zsbday  28406  zscut  28407  expsp1  28426  hlbtwn  28633  cgracol  28850  inaghl  28867  brbtwn2  28934  axcontlem2  28994  ifnebib  32569  isoun  32716  eliccelico  32785  elicoelioo  32786  fzsplit3  32801  prodpr  32832  zarclsun  33830  xrge0iifhom  33897  esumsplit  34033  esumpad2  34036  sibfinima  34320  circlemethhgt  34636  bnj1137  34987  subfacp1lem4  35167  subfacp1lem5  35168  mclsax  35553  poimirlem2  37608  poimirlem8  37614  poimirlem22  37628  poimirlem28  37634  ftc1cnnc  37678  ftc1anclem2  37680  fdc  37731  incsequz2  37735  unichnidl  38017  lkrss2N  39150  cdlemg27b  40678  tendoex  40957  dihmeetlem2N  41281  dvh3dim3N  41431  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c5  42120  sticksstones1  42127  sticksstones2  42128  unitscyglem2  42177  metakunt9  42194  ofun  42255  sn-nnne0  42454  nn0addcom  42456  nn0mulcom  42460  zmulcomlem  42461  rexzrexnn0  42791  pell14qrexpcl  42854  elpell1qr2  42859  acongeq  42971  jm2.23  42984  rpnnen3  43020  mnringmulrcld  44223  mnuprdlem3  44269  radcnvrat  44309  sumpair  44972  cncfiooicclem1  45848  fourierdlem80  46141  fourierdlem93  46154  fullthinc  48845