Theorem jaodan 954

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 855	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843

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 206  df-an 396  df-or 844

This theorem is referenced by:  mpjaodan  955  andi  1004  ccase  1034  mpjao3danOLD  1430  axpr  5346  relop  5748  poltletr  6026  ordnbtwn  6341  oeoa  8390  oeoe  8392  phplem3  8894  ssnnfi  8914  ssnnfiOLD  8915  unwdomg  9273  numwdom  9746  infpssrlem5  9994  fin23lem24  10009  fin23lem28  10027  fin1a2lem10  10096  zornn0g  10192  gchdomtri  10316  fpwwe2lem11  10328  fpwwe2lem12  10329  msqgt0  11425  recextlem2  11536  lemul1a  11759  nnnn0addcl  12193  un0addcl  12196  un0mulcl  12197  elz2  12267  mul2lt0bi  12765  xaddnemnf  12899  xaddnepnf  12900  rexmul  12934  xlemul1a  12951  xrsupsslem  12970  xrinfmsslem  12971  ixxun  13024  fzsplit2  13210  fzsuc2  13243  elfzp12  13264  seqf1olem2  13691  expp1  13717  expneg  13718  expcllem  13721  mulexpz  13751  expaddz  13755  expmulz  13757  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd4  13939  bcpasc  13963  ccatass  14221  ccatrn  14222  ccatswrd  14309  ccatpfx  14342  cats1un  14362  revccat  14407  summo  15357  sumss2  15366  fsumsplit  15381  geomulcvg  15516  fprodsplit  15604  bpoly2  15695  bpoly3  15696  ef0lem  15716  odd2np1  15978  sadcaddlem  16092  gcdcllem3  16136  dvdslcm  16231  lcmeq0  16233  lcmcl  16234  lcmneg  16236  lcmgcd  16240  rpexp1i  16356  pcid  16502  4sqlem16  16589  funcres2c  17533  lubun  18148  mulgneg  18637  mulgnn0z  18645  frgpup3lem  19298  gsumzunsnd  19472  gsumunsnfd  19473  dprddisj2  19557  dmdprdsplit2  19564  dprdsplit  19566  gsumdixp  19763  lssvs0or  20287  evlslem4  21194  refun0  22574  txhaus  22706  xkoptsub  22713  ptunhmeo  22867  xpsxmetlem  23440  xpsmet  23443  mbfss  24715  itg1addlem2  24766  iblss2  24875  itgsplit  24905  limcres  24955  ftc1lem5  25109  coe1mul3  25169  dgrlt  25332  abelthlem3  25497  atanlogaddlem  25968  atanlogsub  25971  atans2  25986  efrlim  26024  bposlem2  26338  lgsdir2lem4  26381  2sqb  26485  pntpbnd1  26639  ostthlem1  26680  hlbtwn  26876  cgracol  27093  inaghl  27110  brbtwn2  27176  axcontlem2  27236  isoun  30936  eliccelico  31000  elicoelioo  31001  fzsplit3  31017  prodpr  31042  zarclsun  31722  xrge0iifhom  31789  esumsplit  31921  esumpad2  31924  sibfinima  32206  circlemethhgt  32523  bnj1137  32875  subfacp1lem4  33045  subfacp1lem5  33046  mclsax  33431  nosepdm  33814  nosupbnd2lem1  33845  poimirlem2  35706  poimirlem8  35712  poimirlem22  35726  poimirlem28  35732  ftc1cnnc  35776  ftc1anclem2  35778  eqfnun  35807  fdc  35830  incsequz2  35834  unichnidl  36116  lkrss2N  37110  cdlemg27b  38637  tendoex  38916  dihmeetlem2N  39240  dvh3dim3N  39390  sticksstones1  40030  sticksstones2  40031  metakunt9  40061  ofun  40137  rexzrexnn0  40542  pell14qrexpcl  40605  elpell1qr2  40610  acongeq  40721  jm2.23  40734  rpnnen3  40770  mnringmulrcld  41735  mnuprdlem3  41781  radcnvrat  41821  sumpair  42467  cncfiooicclem1  43324  fourierdlem80  43617  fourierdlem93  43630  fullthinc  46215