Theorem expl 463

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reximd2a  3276  rabeqsnd  4630  tfindsg2  7897  tz7.49c  8484  domssl  9053  domssr  9054  ssenen  9198  pssnn  9212  unfi  9214  unwdomg  9605  cff1  10363  cfsmolem  10375  cfpwsdom  10696  wunex2  10850  mulgt0sr  11217  uzwo  13065  shftfval  15252  fsum2dlem  15965  fprod2dlem  16176  prmpwdvds  17111  chnind  18824  ghmqusnsglem2  19525  ghmquskerlem2  19529  quscrng  21609  ring2idlqusb  21636  matunitlindflem2  23025  chfacfscmul0  23206  chfacfpmmul0  23210  tgtop  23321  neitr  23528  bwth  23758  tx1stc  23999  cnextcn  24416  logfac2  27574  2sqmo  27794  oldss  28286  tgsegconeu  28979  tglnpt3  29152  tglnpt4  29153  outpasch  29263  trgcopyeu  29343  angmgmlem  29425  prlngmo2  29464  axcontlem12  29583  loop1cycl  30774  spanuni  32176  pjnmopi  32780  superpos  32986  atcvat4i  33029  2ndresdju  33315  fpwrelmap  33395  gsumwun  33707  gsumwrd2dccatlem  33708  wrdpmtrlast  33724  nsgqusf1olem2  34035  ssmxidl  34069  r1plmhm  34211  r1pquslmic  34212  ply1degltdimlem  34324  locfinreflem  34542  cmpcref  34552  fneint  37314  neibastop3  37328  isbasisrelowllem1  38470  isbasisrelowllem2  38471  relowlssretop  38478  finxpreclem6  38511  ralssiun  38522  fin2so  38722  poimirlem26  38756  poimirlem27  38757  heicant  38765  ismblfin  38771  ovoliunnfl  38772  itg2gt0cn  38785  cvrat4  40692  pell14qrexpcl  44067  cantnfresb  44518  liminflimsupxrre  47032  modlt0b  48644  odz2prm2pw  48853  opnneilv  50228  intubeu  50303  unilbeu  50304