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  3247  rabeqsnd  4627  tfindsg2  7807  tz7.49c  8380  domssl  8940  domssr  8941  ssenen  9084  pssnn  9098  unfi  9100  unwdomg  9494  cff1  10173  cfsmolem  10185  cfpwsdom  10500  wunex2  10654  mulgt0sr  11021  uzwo  12829  shftfval  14998  fsum2dlem  15698  fprod2dlem  15908  prmpwdvds  16837  chnind  18549  ghmqusnsglem2  19215  ghmquskerlem2  19219  quscrng  21243  ring2idlqusb  21270  chfacfscmul0  22807  chfacfpmmul0  22811  tgtop  22922  neitr  23129  bwth  23359  tx1stc  23599  cnextcn  24016  logfac2  27189  2sqmo  27409  oldss  27871  outpasch  28832  trgcopyeu  28883  axcontlem12  29053  spanuni  31624  pjnmopi  32228  superpos  32434  atcvat4i  32477  2ndresdju  32731  fpwrelmap  32815  gsumwun  33162  gsumwrd2dccatlem  33163  wrdpmtrlast  33179  nsgqusf1olem2  33499  ssmxidl  33559  r1plmhm  33695  r1pquslmic  33696  ply1degltdimlem  33792  locfinreflem  34010  cmpcref  34020  loop1cycl  35344  fneint  36555  neibastop3  36569  isbasisrelowllem1  37573  isbasisrelowllem2  37574  relowlssretop  37581  finxpreclem6  37614  ralssiun  37625  fin2so  37821  matunitlindflem2  37831  poimirlem26  37860  poimirlem27  37861  heicant  37869  ismblfin  37875  ovoliunnfl  37876  itg2gt0cn  37889  cvrat4  39782  pell14qrexpcl  43187  cantnfresb  43644  liminflimsupxrre  46138  modlt0b  47686  odz2prm2pw  47886  prelrrx2b  49037  opnneilv  49231  intubeu  49306  unilbeu  49307