Theorem expl 457

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  reximd2a  3240  rabeqsnd  4620  tfindsg2  7787  tz7.49c  8360  domssl  8915  domssr  8916  ssenen  9059  pssnn  9073  unfi  9075  unwdomg  9465  cff1  10141  cfsmolem  10153  cfpwsdom  10467  wunex2  10621  mulgt0sr  10988  uzwo  12801  shftfval  14969  fsum2dlem  15669  fprod2dlem  15879  prmpwdvds  16808  chnind  18519  ghmqusnsglem2  19186  ghmquskerlem2  19190  quscrng  21213  ring2idlqusb  21240  chfacfscmul0  22766  chfacfpmmul0  22770  tgtop  22881  neitr  23088  bwth  23318  tx1stc  23558  cnextcn  23975  logfac2  27148  2sqmo  27368  oldss  27816  outpasch  28726  trgcopyeu  28777  axcontlem12  28946  spanuni  31514  pjnmopi  32118  superpos  32324  atcvat4i  32367  2ndresdju  32621  fpwrelmap  32706  gsumwun  33035  gsumwrd2dccatlem  33036  wrdpmtrlast  33052  nsgqusf1olem2  33369  ssmxidl  33429  r1plmhm  33560  r1pquslmic  33561  ply1degltdimlem  33625  locfinreflem  33843  cmpcref  33853  loop1cycl  35149  fneint  36361  neibastop3  36375  isbasisrelowllem1  37368  isbasisrelowllem2  37369  relowlssretop  37376  finxpreclem6  37409  ralssiun  37420  fin2so  37626  matunitlindflem2  37636  poimirlem26  37665  poimirlem27  37666  heicant  37674  ismblfin  37680  ovoliunnfl  37681  itg2gt0cn  37694  cvrat4  39461  pell14qrexpcl  42879  cantnfresb  43336  liminflimsupxrre  45834  modlt0b  47373  odz2prm2pw  47573  prelrrx2b  48725  opnneilv  48919  intubeu  48994  unilbeu  48995