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  3242  rabeqsnd  4621  tfindsg2  7798  tz7.49c  8371  domssl  8926  domssr  8927  ssenen  9070  pssnn  9084  unfi  9086  unwdomg  9476  cff1  10155  cfsmolem  10167  cfpwsdom  10481  wunex2  10635  mulgt0sr  11002  uzwo  12815  shftfval  14983  fsum2dlem  15683  fprod2dlem  15893  prmpwdvds  16822  chnind  18533  ghmqusnsglem2  19199  ghmquskerlem2  19203  quscrng  21226  ring2idlqusb  21253  chfacfscmul0  22779  chfacfpmmul0  22783  tgtop  22894  neitr  23101  bwth  23331  tx1stc  23571  cnextcn  23988  logfac2  27161  2sqmo  27381  oldss  27829  outpasch  28739  trgcopyeu  28790  axcontlem12  28960  spanuni  31531  pjnmopi  32135  superpos  32341  atcvat4i  32384  2ndresdju  32638  fpwrelmap  32723  gsumwun  33052  gsumwrd2dccatlem  33053  wrdpmtrlast  33069  nsgqusf1olem2  33386  ssmxidl  33446  r1plmhm  33577  r1pquslmic  33578  ply1degltdimlem  33642  locfinreflem  33860  cmpcref  33870  loop1cycl  35188  fneint  36399  neibastop3  36413  isbasisrelowllem1  37406  isbasisrelowllem2  37407  relowlssretop  37414  finxpreclem6  37447  ralssiun  37458  fin2so  37653  matunitlindflem2  37663  poimirlem26  37692  poimirlem27  37693  heicant  37701  ismblfin  37707  ovoliunnfl  37708  itg2gt0cn  37721  cvrat4  39548  pell14qrexpcl  42965  cantnfresb  43422  liminflimsupxrre  45920  modlt0b  47468  odz2prm2pw  47668  prelrrx2b  48820  opnneilv  49014  intubeu  49089  unilbeu  49090