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  3239  rabeqsnd  4623  tfindsg2  7802  tz7.49c  8375  domssl  8930  domssr  8931  ssenen  9075  pssnn  9092  unfi  9095  unwdomg  9495  cff1  10171  cfsmolem  10183  cfpwsdom  10497  wunex2  10651  mulgt0sr  11018  uzwo  12830  shftfval  14995  fsum2dlem  15695  fprod2dlem  15905  prmpwdvds  16834  ghmqusnsglem2  19178  ghmquskerlem2  19182  quscrng  21208  ring2idlqusb  21235  chfacfscmul0  22761  chfacfpmmul0  22765  tgtop  22876  neitr  23083  bwth  23313  tx1stc  23553  cnextcn  23970  logfac2  27144  2sqmo  27364  oldss  27810  outpasch  28718  trgcopyeu  28769  axcontlem12  28938  spanuni  31506  pjnmopi  32110  superpos  32316  atcvat4i  32359  2ndresdju  32606  fpwrelmap  32689  chnind  32966  gsumwun  33031  gsumwrd2dccatlem  33032  wrdpmtrlast  33048  nsgqusf1olem2  33361  ssmxidl  33421  r1plmhm  33551  r1pquslmic  33552  ply1degltdimlem  33594  locfinreflem  33806  cmpcref  33816  loop1cycl  35109  fneint  36321  neibastop3  36335  isbasisrelowllem1  37328  isbasisrelowllem2  37329  relowlssretop  37336  finxpreclem6  37369  ralssiun  37380  fin2so  37586  matunitlindflem2  37596  poimirlem26  37625  poimirlem27  37626  heicant  37634  ismblfin  37640  ovoliunnfl  37641  itg2gt0cn  37654  cvrat4  39422  pell14qrexpcl  42840  cantnfresb  43297  liminflimsupxrre  45799  modlt0b  47348  odz2prm2pw  47548  prelrrx2b  48687  opnneilv  48881  intubeu  48956  unilbeu  48957