Theorem jaodan 940

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

Syntax hints:   → wi 4   ∧ wa 387   ∨ wo 833

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 199  df-an 388  df-or 834

This theorem is referenced by:  mpjaodan  941  andi  990  ccase  1018  mpjao3dan  1411  axpr  5179  relop  5564  poltletr  5826  ordnbtwn  6113  oeoa  8016  oeoe  8018  phplem3  8486  ssnnfi  8524  unwdomg  8835  numwdom  9271  infpssrlem5  9519  fin23lem24  9534  fin23lem28  9552  fin1a2lem10  9621  zornn0g  9717  gchdomtri  9841  fpwwe2lem12  9853  fpwwe2lem13  9854  msqgt0  10953  recextlem2  11064  lemul1a  11287  nnnn0addcl  11732  un0addcl  11735  un0mulcl  11736  elz2  11804  mul2lt0bi  12305  xaddnemnf  12439  xaddnepnf  12440  rexmul  12473  xlemul1a  12490  xrsupsslem  12509  xrinfmsslem  12510  ixxun  12563  fzsplit2  12741  fzsuc2  12774  elfzp12  12795  seqf1olem2  13218  expp1  13244  expneg  13245  expcllem  13248  mulexpz  13277  expaddz  13281  expmulz  13283  faclbnd4lem3  13463  faclbnd4lem4  13464  faclbnd4  13465  bcpasc  13489  ccatass  13741  ccatrn  13742  ccatswrd  13839  ccatpfx  13873  cats1un  13904  revccat  13975  summo  14924  sumss2  14933  fsumsplit  14947  geomulcvg  15082  fprodsplit  15170  bpoly2  15261  bpoly3  15262  ef0lem  15282  odd2np1  15540  sadcaddlem  15656  gcdcllem3  15700  dvdslcm  15788  lcmeq0  15790  lcmcl  15791  lcmneg  15793  lcmgcd  15797  rpexp1i  15911  pcid  16055  4sqlem16  16142  funcres2c  17019  lubun  17581  mulgneg  18021  mulgnn0z  18028  frgpup3lem  18653  gsumzunsnd  18819  gsumunsnfd  18820  dprddisj2  18901  dmdprdsplit2  18908  dprdsplit  18910  gsumdixp  19072  lssvs0or  19594  evlslem4  19991  refun0  21817  txhaus  21949  xkoptsub  21956  ptunhmeo  22110  xpsxmetlem  22682  xpsmet  22685  mbfss  23940  itg1addlem2  23991  iblss2  24099  itgsplit  24129  limcres  24177  ftc1lem5  24330  coe1mul3  24386  dgrlt  24549  abelthlem3  24714  atanlogaddlem  25182  atanlogsub  25185  atans2  25200  efrlim  25239  bposlem2  25553  lgsdir2lem4  25596  2sqb  25700  pntpbnd1  25854  ostthlem1  25895  hlbtwn  26089  cgracol  26306  inaghl  26324  brbtwn2  26384  axcontlem2  26444  isoun  30178  eliccelico  30241  elicoelioo  30242  fzsplit3  30255  prodpr  30277  xrge0iifhom  30781  esumsplit  30913  esumpad2  30916  sibfinima  31199  circlemethhgt  31523  bnj1137  31873  subfacp1lem4  31975  subfacp1lem5  31976  mclsax  32276  nosepdm  32649  nosupbnd2lem1  32676  poimirlem2  34283  poimirlem8  34289  poimirlem22  34303  poimirlem28  34309  ftc1cnnc  34355  ftc1anclem2  34357  eqfnun  34387  fdc  34410  incsequz2  34414  unichnidl  34699  lkrss2N  35698  cdlemg27b  37225  tendoex  37504  dihmeetlem2N  37828  dvh3dim3N  37978  rexzrexnn0  38742  pell14qrexpcl  38805  elpell1qr2  38810  acongeq  38921  jm2.23  38934  rpnnen3  38970  mnuprdlem3  39930  radcnvrat  40006  sumpair  40655  cncfiooicclem1  41552  fourierdlem80  41848  fourierdlem93  41861