Theorem jaodan 970

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 416	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 416	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 870	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 410	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858

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 209  df-an 400  df-or 859

This theorem is referenced by:  mpjaodan  971  andi  1021  ccase  1049  axprOLD  5389  relop  5822  poltletr  6119  ordnbtwn  6441  eqfnun  7018  oeoa  8567  oeoe  8569  ssnnfi  9138  domnsymfi  9168  unwdomg  9532  numwdom  10015  infpssrlem5  10264  fin23lem24  10279  fin23lem28  10297  fin1a2lem10  10366  zornn0g  10462  gchdomtri  10587  fpwwe2lem11  10599  fpwwe2lem12  10600  msqgt0  11707  recextlem2  11818  lemul1a  12045  nnne0  12247  nnnn0addcl  12511  un0addcl  12514  un0mulcl  12515  elz2  12586  mul2lt0bi  13101  xaddnemnf  13239  xaddnepnf  13240  rexmul  13274  xlemul1a  13291  xrsupsslem  13310  xrinfmsslem  13311  ixxun  13365  fzsplit2  13554  fzsuc2  13587  elfzp12  13608  seqf1olem2  14055  expp1  14081  expneg  14082  expcllem  14085  mulexpz  14115  expaddz  14119  expmulz  14121  zzlesq  14219  faclbnd4lem3  14308  faclbnd4lem4  14309  faclbnd4  14310  bcpasc  14334  ccatass  14602  ccatrn  14603  ccatswrd  14682  ccatpfx  14714  cats1un  14734  revccat  14779  summo  15744  sumss2  15753  fsumsplit  15768  geomulcvg  15906  fprodsplit  15996  bpoly2  16087  bpoly3  16088  ef0lem  16108  odd2np1  16375  sadcaddlem  16491  gcdcllem3  16535  dvdslcm  16632  lcmeq0  16634  lcmcl  16635  lcmneg  16637  lcmgcd  16641  rpexp1i  16758  pcid  16909  4sqlem16  16996  funcres2c  17936  lubun  18547  mulgneg  19134  mulgnn0z  19143  frgpup3lem  19817  gsumzunsnd  19996  gsumunsnfd  19997  dprddisj2  20081  dmdprdsplit2  20088  dprdsplit  20090  gsumdixp  20367  lssvs0or  21180  evlslem4  22129  refun0  23575  txhaus  23707  xkoptsub  23714  ptunhmeo  23868  xpsxmetlem  24439  xpsmet  24442  mbfss  25708  itg1addlem2  25759  iblss2  25868  itgsplit  25898  limcres  25948  ftc1lem5  26102  coe1mul3  26159  dgrlt  26326  abelthlem3  26496  atanlogaddlem  26978  atanlogsub  26981  atans2  26996  efrlim  27034  bposlem2  27349  lgsdir2lem4  27392  2sqb  27496  pntpbnd1  27650  ostthlem1  27691  nosepdm  27748  nosupbnd2lem1  27779  negsid  28134  elzn0s  28491  zsbday  28499  zcuts  28500  expsp1  28522  hlbtwn  28780  cgracol  29022  inaghl  29039  brbtwn2  29106  axcontlem2  29166  ifnebib  32748  isoun  32904  eliccelico  32979  elicoelioo  32980  fzsplit3  32995  prodpr  33028  zarclsun  34167  xrge0iifhom  34234  esumsplit  34350  esumpad2  34353  sibfinima  34636  circlemethhgt  34937  bnj1137  35290  subfacp1lem4  35533  subfacp1lem5  35534  mclsax  35919  poimirlem2  38121  poimirlem8  38127  poimirlem22  38141  poimirlem28  38147  ftc1cnnc  38191  ftc1anclem2  38193  fdc  38244  incsequz2  38248  unichnidl  38530  lkrss2N  39793  cdlemg27b  41320  tendoex  41599  dihmeetlem2N  41923  dvh3dim3N  42073  aks6d1c2p2  42736  hashscontpow  42739  aks6d1c5  42756  sticksstones1  42763  sticksstones2  42764  unitscyglem2  42813  ofun  42854  sn-nnne0  43082  nn0addcom  43084  nn0mulcom  43088  zmulcomlem  43089  rexzrexnn0  43381  pell14qrexpcl  43444  elpell1qr2  43449  acongeq  43560  jm2.23  43573  rpnnen3  43609  mnringmulrcld  44804  mnuprdlem3  44850  radcnvrat  44890  sumpair  45615  cncfiooicclem1  46467  fourierdlem80  46760  fourierdlem93  46773  fullthinc  50071