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  3258  rabeqsnd  4663  tfindsg2  7844  tz7.49c  8441  domssl  8989  domssr  8990  ssenen  9146  pssnn  9163  unfi  9167  pssnnOLD  9260  unwdomg  9574  cff1  10248  cfsmolem  10260  cfpwsdom  10574  wunex2  10728  mulgt0sr  11095  uzwo  12891  shftfval  15013  fsum2dlem  15712  fprod2dlem  15920  prmpwdvds  16833  quscrng  21123  ring2idlqusb  21148  chfacfscmul0  22670  chfacfpmmul0  22674  tgtop  22786  neitr  22994  bwth  23224  tx1stc  23464  cnextcn  23881  logfac2  27054  2sqmo  27274  outpasch  28430  trgcopyeu  28481  axcontlem12  28657  spanuni  31221  pjnmopi  31825  superpos  32031  atcvat4i  32074  2ndresdju  32298  fpwrelmap  32382  nsgqusf1olem2  32956  ghmquskerlem2  32961  ssmxidl  33021  r1plmhm  33112  r1pquslmic  33113  ply1degltdimlem  33152  locfinreflem  33275  cmpcref  33285  loop1cycl  34583  fneint  35689  neibastop3  35703  isbasisrelowllem1  36692  isbasisrelowllem2  36693  relowlssretop  36700  finxpreclem6  36733  ralssiun  36744  fin2so  36931  matunitlindflem2  36941  poimirlem26  36970  poimirlem27  36971  heicant  36979  ismblfin  36985  ovoliunnfl  36986  itg2gt0cn  36999  cvrat4  38770  pell14qrexpcl  42060  cantnfresb  42529  liminflimsupxrre  44984  odz2prm2pw  46682  prelrrx2b  47554  opnneilv  47695  intubeu  47763  unilbeu  47764