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 206  df-an 396

This theorem is referenced by:  reximd2a  3261  rabeqsnd  4667  tfindsg2  7860  tz7.49c  8460  domssl  9010  domssr  9011  ssenen  9167  pssnn  9184  unfi  9188  pssnnOLD  9281  unwdomg  9599  cff1  10273  cfsmolem  10285  cfpwsdom  10599  wunex2  10753  mulgt0sr  11120  uzwo  12917  shftfval  15041  fsum2dlem  15740  fprod2dlem  15948  prmpwdvds  16864  ghmquskerlem2  19227  quscrng  21164  ring2idlqusb  21189  chfacfscmul0  22747  chfacfpmmul0  22751  tgtop  22863  neitr  23071  bwth  23301  tx1stc  23541  cnextcn  23958  logfac2  27137  2sqmo  27357  outpasch  28546  trgcopyeu  28597  axcontlem12  28773  spanuni  31341  pjnmopi  31945  superpos  32151  atcvat4i  32194  2ndresdju  32418  fpwrelmap  32499  nsgqusf1olem2  33064  ssmxidl  33123  r1plmhm  33212  r1pquslmic  33213  ply1degltdimlem  33252  locfinreflem  33377  cmpcref  33387  loop1cycl  34683  fneint  35768  neibastop3  35782  isbasisrelowllem1  36770  isbasisrelowllem2  36771  relowlssretop  36778  finxpreclem6  36811  ralssiun  36822  fin2so  37015  matunitlindflem2  37025  poimirlem26  37054  poimirlem27  37055  heicant  37063  ismblfin  37069  ovoliunnfl  37070  itg2gt0cn  37083  cvrat4  38853  pell14qrexpcl  42209  cantnfresb  42676  liminflimsupxrre  45128  odz2prm2pw  46826  prelrrx2b  47710  opnneilv  47850  intubeu  47918  unilbeu  47919