Theorem expl 462

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

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

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 401

This theorem is used by:  reximd2a  3274  rabeqsnd  4634  tfindsg2  7856  tz7.49c  8431  domssl  8993  domssr  8994  ssenen  9137  pssnn  9151  unfi  9153  unwdomg  9544  cff1  10248  cfsmolem  10260  cfpwsdom  10575  wunex2  10729  mulgt0sr  11096  uzwo  12941  shftfval  15114  fsum2dlem  15828  fprod2dlem  16041  prmpwdvds  16970  chnind  18683  ghmqusnsglem2  19357  ghmquskerlem2  19361  quscrng  21434  ring2idlqusb  21461  chfacfscmul0  23026  chfacfpmmul0  23030  tgtop  23141  neitr  23348  bwth  23578  tx1stc  23818  cnextcn  24235  logfac2  27392  2sqmo  27612  oldss  28074  tglnpt3  28938  tglnpt4  28939  outpasch  29048  trgcopyeu  29128  prlngmo2  29217  axcontlem12  29336  spanuni  31907  pjnmopi  32511  superpos  32717  atcvat4i  32760  2ndresdju  33005  fpwrelmap  33089  gsumwun  33405  gsumwrd2dccatlem  33406  wrdpmtrlast  33422  nsgqusf1olem2  33732  ssmxidl  33766  r1plmhm  33908  r1pquslmic  33909  ply1degltdimlem  34021  locfinreflem  34239  cmpcref  34249  loop1cycl  35637  fneint  36887  neibastop3  36901  isbasisrelowllem1  38029  isbasisrelowllem2  38030  relowlssretop  38037  finxpreclem6  38070  ralssiun  38081  fin2so  38286  matunitlindflem2  38296  poimirlem26  38325  poimirlem27  38326  heicant  38334  ismblfin  38340  ovoliunnfl  38341  itg2gt0cn  38354  cvrat4  40245  pell14qrexpcl  43622  cantnfresb  44079  liminflimsupxrre  46559  modlt0b  48134  odz2prm2pw  48343  prelrrx2b  49522  opnneilv  49715  intubeu  49790  unilbeu  49791