Theorem expl 460

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reximd2a  3262  rabeqsnd  4618  tfindsg2  7827  tz7.49c  8401  domssl  8964  domssr  8965  ssenen  9108  pssnn  9122  unfi  9124  unwdomg  9518  cff1  10201  cfsmolem  10213  cfpwsdom  10528  wunex2  10682  mulgt0sr  11049  uzwo  12898  shftfval  15069  fsum2dlem  15769  fprod2dlem  15982  prmpwdvds  16912  chnind  18625  ghmqusnsglem2  19293  ghmquskerlem2  19297  quscrng  21322  ring2idlqusb  21349  chfacfscmul0  22887  chfacfpmmul0  22891  tgtop  23002  neitr  23209  bwth  23439  tx1stc  23679  cnextcn  24096  logfac2  27247  2sqmo  27467  oldss  27929  outpasch  28890  trgcopyeu  28941  axcontlem12  29111  spanuni  31682  pjnmopi  32286  superpos  32492  atcvat4i  32535  2ndresdju  32790  fpwrelmap  32874  gsumwun  33206  gsumwrd2dccatlem  33207  wrdpmtrlast  33223  nsgqusf1olem2  33546  ssmxidl  33606  r1plmhm  33750  r1pquslmic  33751  ply1degltdimlem  33863  locfinreflem  34081  cmpcref  34091  loop1cycl  35425  fneint  36646  neibastop3  36660  isbasisrelowllem1  37787  isbasisrelowllem2  37788  relowlssretop  37795  finxpreclem6  37828  ralssiun  37839  fin2so  38044  matunitlindflem2  38054  poimirlem26  38083  poimirlem27  38084  heicant  38092  ismblfin  38098  ovoliunnfl  38099  itg2gt0cn  38112  cvrat4  40005  pell14qrexpcl  43382  cantnfresb  43839  liminflimsupxrre  46329  modlt0b  47901  odz2prm2pw  48110  prelrrx2b  49274  opnneilv  49468  intubeu  49543  unilbeu  49544