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  3245  rabeqsnd  4603  tfindsg2  7802  tz7.49c  8374  domssl  8934  domssr  8935  ssenen  9078  pssnn  9092  unfi  9094  unwdomg  9488  cff1  10169  cfsmolem  10181  cfpwsdom  10496  wunex2  10650  mulgt0sr  11017  uzwo  12850  shftfval  15021  fsum2dlem  15721  fprod2dlem  15934  prmpwdvds  16864  chnind  18576  ghmqusnsglem2  19245  ghmquskerlem2  19249  quscrng  21270  ring2idlqusb  21297  chfacfscmul0  22811  chfacfpmmul0  22815  tgtop  22926  neitr  23133  bwth  23363  tx1stc  23603  cnextcn  24020  logfac2  27168  2sqmo  27388  oldss  27850  outpasch  28811  trgcopyeu  28862  axcontlem12  29032  spanuni  31603  pjnmopi  32207  superpos  32413  atcvat4i  32456  2ndresdju  32710  fpwrelmap  32794  gsumwun  33125  gsumwrd2dccatlem  33126  wrdpmtrlast  33142  nsgqusf1olem2  33462  ssmxidl  33522  r1plmhm  33658  r1pquslmic  33659  ply1degltdimlem  33754  locfinreflem  33972  cmpcref  33982  loop1cycl  35307  fneint  36518  neibastop3  36532  isbasisrelowllem1  37659  isbasisrelowllem2  37660  relowlssretop  37667  finxpreclem6  37700  ralssiun  37711  fin2so  37916  matunitlindflem2  37926  poimirlem26  37955  poimirlem27  37956  heicant  37964  ismblfin  37970  ovoliunnfl  37971  itg2gt0cn  37984  cvrat4  39877  pell14qrexpcl  43283  cantnfresb  43740  liminflimsupxrre  46233  modlt0b  47805  odz2prm2pw  48014  prelrrx2b  49178  opnneilv  49372  intubeu  49447  unilbeu  49448