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  3255  rabeqsnd  4649  tfindsg2  7865  tz7.49c  8468  domssl  9020  domssr  9021  ssenen  9173  pssnn  9190  unfi  9193  unwdomg  9606  cff1  10280  cfsmolem  10292  cfpwsdom  10606  wunex2  10760  mulgt0sr  11127  uzwo  12935  shftfval  15092  fsum2dlem  15789  fprod2dlem  15999  prmpwdvds  16925  ghmqusnsglem2  19269  ghmquskerlem2  19273  quscrng  21256  ring2idlqusb  21283  chfacfscmul0  22813  chfacfpmmul0  22817  tgtop  22928  neitr  23135  bwth  23365  tx1stc  23605  cnextcn  24022  logfac2  27198  2sqmo  27418  outpasch  28700  trgcopyeu  28751  axcontlem12  28921  spanuni  31492  pjnmopi  32096  superpos  32302  atcvat4i  32345  2ndresdju  32595  fpwrelmap  32680  chnind  32945  gsumwun  33012  gsumwrd2dccatlem  33013  wrdpmtrlast  33057  nsgqusf1olem2  33382  ssmxidl  33442  r1plmhm  33570  r1pquslmic  33571  ply1degltdimlem  33613  locfinreflem  33814  cmpcref  33824  loop1cycl  35117  fneint  36324  neibastop3  36338  isbasisrelowllem1  37331  isbasisrelowllem2  37332  relowlssretop  37339  finxpreclem6  37372  ralssiun  37383  fin2so  37589  matunitlindflem2  37599  poimirlem26  37628  poimirlem27  37629  heicant  37637  ismblfin  37643  ovoliunnfl  37644  itg2gt0cn  37657  cvrat4  39420  pell14qrexpcl  42856  cantnfresb  43314  liminflimsupxrre  45804  odz2prm2pw  47523  prelrrx2b  48608  opnneilv  48790  intubeu  48865  unilbeu  48866