Theorem expl 461

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 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 414	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  reximd2a  3236  tfindsg2  7580  tz7.49c  8097  ssenen  8718  pssnn  8743  unfi  8746  pssnnOLD  8779  unwdomg  9086  cff1  9723  cfsmolem  9735  cfpwsdom  10049  wunex2  10203  mulgt0sr  10570  uzwo  12356  shftfval  14482  fsum2dlem  15178  fprod2dlem  15387  prmpwdvds  16300  quscrng  20086  chfacfscmul0  21563  chfacfpmmul0  21567  tgtop  21678  neitr  21885  bwth  22115  tx1stc  22355  cnextcn  22772  logfac2  25905  2sqmo  26125  outpasch  26653  trgcopyeu  26704  axcontlem12  26873  spanuni  29431  pjnmopi  30035  superpos  30241  atcvat4i  30284  rabeqsnd  30375  2ndresdju  30513  fpwrelmap  30596  nsgqusf1olem2  31124  ssmxidl  31167  locfinreflem  31315  cmpcref  31325  loop1cycl  32619  fneint  34112  neibastop3  34126  isbasisrelowllem1  35078  isbasisrelowllem2  35079  relowlssretop  35086  finxpreclem6  35119  ralssiun  35130  fin2so  35350  matunitlindflem2  35360  poimirlem26  35389  poimirlem27  35390  heicant  35398  ismblfin  35404  ovoliunnfl  35405  itg2gt0cn  35418  cvrat4  37045  pell14qrexpcl  40209  liminflimsupxrre  42853  odz2prm2pw  44476  prelrrx2b  45521  opnneilv  45620