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  3272  rabeqsnd  4629  tfindsg2  7873  tz7.49c  8456  domssl  9025  domssr  9026  ssenen  9170  pssnn  9184  unfi  9186  unwdomg  9578  cff1  10336  cfsmolem  10348  cfpwsdom  10669  wunex2  10823  mulgt0sr  11190  uzwo  13038  shftfval  15223  fsum2dlem  15936  fprod2dlem  16147  prmpwdvds  17082  chnind  18795  ghmqusnsglem2  19495  ghmquskerlem2  19499  quscrng  21579  ring2idlqusb  21606  matunitlindflem2  22995  chfacfscmul0  23176  chfacfpmmul0  23180  tgtop  23291  neitr  23498  bwth  23728  tx1stc  23969  cnextcn  24386  logfac2  27544  2sqmo  27764  oldss  28256  tgsegconeu  28949  tglnpt3  29122  tglnpt4  29123  outpasch  29233  trgcopyeu  29313  angmgmlem  29395  prlngmo2  29434  axcontlem12  29553  loop1cycl  30744  spanuni  32146  pjnmopi  32750  superpos  32956  atcvat4i  32999  2ndresdju  33285  fpwrelmap  33367  gsumwun  33679  gsumwrd2dccatlem  33680  wrdpmtrlast  33696  nsgqusf1olem2  34007  ssmxidl  34041  r1plmhm  34183  r1pquslmic  34184  ply1degltdimlem  34296  locfinreflem  34514  cmpcref  34524  fneint  37178  neibastop3  37192  isbasisrelowllem1  38321  isbasisrelowllem2  38322  relowlssretop  38329  finxpreclem6  38362  ralssiun  38373  fin2so  38573  poimirlem26  38607  poimirlem27  38608  heicant  38616  ismblfin  38622  ovoliunnfl  38623  itg2gt0cn  38636  cvrat4  40543  pell14qrexpcl  43917  cantnfresb  44369  liminflimsupxrre  46870  modlt0b  48482  odz2prm2pw  48691  prelrrx2b  49869  opnneilv  50060  intubeu  50135  unilbeu  50136