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  3268  rabeqsnd  4668  tfindsg2  7884  tz7.49c  8487  domssl  9039  domssr  9040  ssenen  9192  pssnn  9209  unfi  9212  unwdomg  9625  cff1  10299  cfsmolem  10311  cfpwsdom  10625  wunex2  10779  mulgt0sr  11146  uzwo  12954  shftfval  15110  fsum2dlem  15807  fprod2dlem  16017  prmpwdvds  16943  ghmqusnsglem2  19300  ghmquskerlem2  19304  quscrng  21294  ring2idlqusb  21321  chfacfscmul0  22865  chfacfpmmul0  22869  tgtop  22981  neitr  23189  bwth  23419  tx1stc  23659  cnextcn  24076  logfac2  27262  2sqmo  27482  outpasch  28764  trgcopyeu  28815  axcontlem12  28991  spanuni  31564  pjnmopi  32168  superpos  32374  atcvat4i  32417  2ndresdju  32660  fpwrelmap  32745  chnind  33002  gsumwun  33069  gsumwrd2dccatlem  33070  wrdpmtrlast  33114  nsgqusf1olem2  33443  ssmxidl  33503  r1plmhm  33631  r1pquslmic  33632  ply1degltdimlem  33674  locfinreflem  33840  cmpcref  33850  loop1cycl  35143  fneint  36350  neibastop3  36364  isbasisrelowllem1  37357  isbasisrelowllem2  37358  relowlssretop  37365  finxpreclem6  37398  ralssiun  37409  fin2so  37615  matunitlindflem2  37625  poimirlem26  37654  poimirlem27  37655  heicant  37663  ismblfin  37669  ovoliunnfl  37670  itg2gt0cn  37683  cvrat4  39446  pell14qrexpcl  42883  cantnfresb  43342  liminflimsupxrre  45837  odz2prm2pw  47555  prelrrx2b  48640  opnneilv  48813  intubeu  48888  unilbeu  48889