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  3248  rabeqsnd  4614  tfindsg2  7804  tz7.49c  8376  domssl  8936  domssr  8937  ssenen  9080  pssnn  9094  unfi  9096  unwdomg  9490  cff1  10169  cfsmolem  10181  cfpwsdom  10496  wunex2  10650  mulgt0sr  11017  uzwo  12825  shftfval  14994  fsum2dlem  15694  fprod2dlem  15904  prmpwdvds  16833  chnind  18545  ghmqusnsglem2  19214  ghmquskerlem2  19218  quscrng  21240  ring2idlqusb  21267  chfacfscmul0  22801  chfacfpmmul0  22805  tgtop  22916  neitr  23123  bwth  23353  tx1stc  23593  cnextcn  24010  logfac2  27168  2sqmo  27388  oldss  27850  outpasch  28811  trgcopyeu  28862  axcontlem12  29032  spanuni  31604  pjnmopi  32208  superpos  32414  atcvat4i  32457  2ndresdju  32711  fpwrelmap  32795  gsumwun  33142  gsumwrd2dccatlem  33143  wrdpmtrlast  33159  nsgqusf1olem2  33479  ssmxidl  33539  r1plmhm  33675  r1pquslmic  33676  ply1degltdimlem  33772  locfinreflem  33990  cmpcref  34000  loop1cycl  35325  fneint  36536  neibastop3  36550  isbasisrelowllem1  37667  isbasisrelowllem2  37668  relowlssretop  37675  finxpreclem6  37708  ralssiun  37719  fin2so  37919  matunitlindflem2  37929  poimirlem26  37958  poimirlem27  37959  heicant  37967  ismblfin  37973  ovoliunnfl  37974  itg2gt0cn  37987  cvrat4  39880  pell14qrexpcl  43298  cantnfresb  43755  liminflimsupxrre  46249  modlt0b  47797  odz2prm2pw  47997  prelrrx2b  49148  opnneilv  49342  intubeu  49417  unilbeu  49418