Theorem expl 461

Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)

Hypothesis

Ref	Expression
expl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
expl	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem expl

Step	Hyp	Ref	Expression
1		expl.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 414	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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

This theorem is referenced by:  reximd2a  3273  rabeqsnd  4629  tfindsg2  7842  tz7.49c  8417  domssl  8979  domssr  8980  ssenen  9123  pssnn  9137  unfi  9139  unwdomg  9530  cff1  10226  cfsmolem  10238  cfpwsdom  10553  wunex2  10707  mulgt0sr  11074  uzwo  12922  shftfval  15093  fsum2dlem  15807  fprod2dlem  16020  prmpwdvds  16950  chnind  18663  ghmqusnsglem2  19331  ghmquskerlem2  19335  quscrng  21360  ring2idlqusb  21387  chfacfscmul0  22925  chfacfpmmul0  22929  tgtop  23040  neitr  23247  bwth  23477  tx1stc  23717  cnextcn  24134  logfac2  27288  2sqmo  27508  oldss  27970  tglnpt3  28830  tglnpt4  28831  outpasch  28935  trgcopyeu  28986  axcontlem12  29183  spanuni  31754  pjnmopi  32358  superpos  32564  atcvat4i  32607  2ndresdju  32857  fpwrelmap  32941  gsumwun  33262  gsumwrd2dccatlem  33263  wrdpmtrlast  33279  nsgqusf1olem2  33603  ssmxidl  33665  r1plmhm  33808  r1pquslmic  33809  ply1degltdimlem  33921  locfinreflem  34139  cmpcref  34149  loop1cycl  35492  fneint  36713  neibastop3  36727  isbasisrelowllem1  37854  isbasisrelowllem2  37855  relowlssretop  37862  finxpreclem6  37895  ralssiun  37906  fin2so  38111  matunitlindflem2  38121  poimirlem26  38150  poimirlem27  38151  heicant  38159  ismblfin  38165  ovoliunnfl  38166  itg2gt0cn  38179  cvrat4  40072  pell14qrexpcl  43449  cantnfresb  43906  liminflimsupxrre  46382  modlt0b  47954  odz2prm2pw  48163  prelrrx2b  49327  opnneilv  49521  intubeu  49596  unilbeu  49597