Theorem expl 462

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 424	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 415	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reximd2a  3273  rabeqsnd  4634  tfindsg2  7857  tz7.49c  8432  domssl  8994  domssr  8995  ssenen  9138  pssnn  9152  unfi  9154  unwdomg  9545  cff1  10241  cfsmolem  10253  cfpwsdom  10568  wunex2  10722  mulgt0sr  11089  uzwo  12934  shftfval  15106  fsum2dlem  15820  fprod2dlem  16033  prmpwdvds  16963  chnind  18676  ghmqusnsglem2  19350  ghmquskerlem2  19354  quscrng  21402  ring2idlqusb  21429  chfacfscmul0  22994  chfacfpmmul0  22998  tgtop  23109  neitr  23316  bwth  23546  tx1stc  23786  cnextcn  24203  logfac2  27357  2sqmo  27577  oldss  28039  tglnpt3  28903  tglnpt4  28904  outpasch  29012  trgcopyeu  29090  prlngmo2  29179  axcontlem12  29291  spanuni  31862  pjnmopi  32466  superpos  32672  atcvat4i  32715  2ndresdju  32960  fpwrelmap  33044  gsumwun  33362  gsumwrd2dccatlem  33363  wrdpmtrlast  33379  nsgqusf1olem2  33689  ssmxidl  33723  r1plmhm  33865  r1pquslmic  33866  ply1degltdimlem  33978  locfinreflem  34196  cmpcref  34206  loop1cycl  35583  fneint  36803  neibastop3  36817  isbasisrelowllem1  37945  isbasisrelowllem2  37946  relowlssretop  37953  finxpreclem6  37986  ralssiun  37997  fin2so  38202  matunitlindflem2  38212  poimirlem26  38241  poimirlem27  38242  heicant  38250  ismblfin  38256  ovoliunnfl  38257  itg2gt0cn  38270  cvrat4  40163  pell14qrexpcl  43542  cantnfresb  43999  liminflimsupxrre  46479  modlt0b  48051  odz2prm2pw  48260  prelrrx2b  49439  opnneilv  49632  intubeu  49707  unilbeu  49708