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

Syntax hints:   → wi 4   ∧ wa 398   ∨ 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 209  df-an 399  df-or 844

This theorem is referenced by:  mpjaodan  955  andi  1004  ccase  1032  mpjao3danOLD  1428  axpr  5329  relop  5721  poltletr  5992  ordnbtwn  6281  oeoa  8223  oeoe  8225  phplem3  8698  ssnnfi  8737  unwdomg  9048  numwdom  9485  infpssrlem5  9729  fin23lem24  9744  fin23lem28  9762  fin1a2lem10  9831  zornn0g  9927  gchdomtri  10051  fpwwe2lem12  10063  fpwwe2lem13  10064  msqgt0  11160  recextlem2  11271  lemul1a  11494  nnnn0addcl  11928  un0addcl  11931  un0mulcl  11932  elz2  12000  mul2lt0bi  12496  xaddnemnf  12630  xaddnepnf  12631  rexmul  12665  xlemul1a  12682  xrsupsslem  12701  xrinfmsslem  12702  ixxun  12755  fzsplit2  12933  fzsuc2  12966  elfzp12  12987  seqf1olem2  13411  expp1  13437  expneg  13438  expcllem  13441  mulexpz  13470  expaddz  13474  expmulz  13476  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd4  13658  bcpasc  13682  ccatass  13942  ccatrn  13943  ccatswrd  14030  ccatpfx  14063  cats1un  14083  revccat  14128  summo  15074  sumss2  15083  fsumsplit  15097  geomulcvg  15232  fprodsplit  15320  bpoly2  15411  bpoly3  15412  ef0lem  15432  odd2np1  15690  sadcaddlem  15806  gcdcllem3  15850  dvdslcm  15942  lcmeq0  15944  lcmcl  15945  lcmneg  15947  lcmgcd  15951  rpexp1i  16065  pcid  16209  4sqlem16  16296  funcres2c  17171  lubun  17733  mulgneg  18246  mulgnn0z  18254  frgpup3lem  18903  gsumzunsnd  19076  gsumunsnfd  19077  dprddisj2  19161  dmdprdsplit2  19168  dprdsplit  19170  gsumdixp  19359  lssvs0or  19882  evlslem4  20288  refun0  22123  txhaus  22255  xkoptsub  22262  ptunhmeo  22416  xpsxmetlem  22989  xpsmet  22992  mbfss  24247  itg1addlem2  24298  iblss2  24406  itgsplit  24436  limcres  24484  ftc1lem5  24637  coe1mul3  24693  dgrlt  24856  abelthlem3  25021  atanlogaddlem  25491  atanlogsub  25494  atans2  25509  efrlim  25547  bposlem2  25861  lgsdir2lem4  25904  2sqb  26008  pntpbnd1  26162  ostthlem1  26203  hlbtwn  26397  cgracol  26614  inaghl  26631  brbtwn2  26691  axcontlem2  26751  isoun  30437  eliccelico  30500  elicoelioo  30501  fzsplit3  30517  prodpr  30542  xrge0iifhom  31180  esumsplit  31312  esumpad2  31315  sibfinima  31597  circlemethhgt  31914  bnj1137  32267  subfacp1lem4  32430  subfacp1lem5  32431  mclsax  32816  nosepdm  33188  nosupbnd2lem1  33215  poimirlem2  34909  poimirlem8  34915  poimirlem22  34929  poimirlem28  34935  ftc1cnnc  34981  ftc1anclem2  34983  eqfnun  35012  fdc  35035  incsequz2  35039  unichnidl  35324  lkrss2N  36320  cdlemg27b  37847  tendoex  38126  dihmeetlem2N  38450  dvh3dim3N  38600  rexzrexnn0  39450  pell14qrexpcl  39513  elpell1qr2  39518  acongeq  39629  jm2.23  39642  rpnnen3  39678  mnuprdlem3  40659  radcnvrat  40695  sumpair  41341  cncfiooicclem1  42225  fourierdlem80  42520  fourierdlem93  42533