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  3271  tfindsg2  7556  tz7.49c  8065  ssenen  8675  pssnn  8720  unwdomg  9032  cff1  9669  cfsmolem  9681  cfpwsdom  9995  wunex2  10149  mulgt0sr  10516  uzwo  12299  shftfval  14421  fsum2dlem  15117  fprod2dlem  15326  prmpwdvds  16230  quscrng  20006  chfacfscmul0  21463  chfacfpmmul0  21467  tgtop  21578  neitr  21785  bwth  22015  tx1stc  22255  cnextcn  22672  logfac2  25801  2sqmo  26021  outpasch  26549  trgcopyeu  26600  axcontlem12  26769  spanuni  29327  pjnmopi  29931  superpos  30137  atcvat4i  30180  rabeqsnd  30271  2ndresdju  30411  fpwrelmap  30495  ssmxidl  31050  locfinreflem  31193  cmpcref  31203  loop1cycl  32497  fneint  33809  neibastop3  33823  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlssretop  34780  finxpreclem6  34813  ralssiun  34824  fin2so  35044  matunitlindflem2  35054  poimirlem26  35083  poimirlem27  35084  heicant  35092  ismblfin  35098  ovoliunnfl  35099  itg2gt0cn  35112  cvrat4  36739  pell14qrexpcl  39808  liminflimsupxrre  42459  odz2prm2pw  44080  prelrrx2b  45128