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  3240  tfindsg2  7683  tz7.49c  8247  ssenen  8887  pssnn  8913  unfi  8917  pssnnOLD  8969  unwdomg  9273  cff1  9945  cfsmolem  9957  cfpwsdom  10271  wunex2  10425  mulgt0sr  10792  uzwo  12580  shftfval  14709  fsum2dlem  15410  fprod2dlem  15618  prmpwdvds  16533  quscrng  20424  chfacfscmul0  21915  chfacfpmmul0  21919  tgtop  22031  neitr  22239  bwth  22469  tx1stc  22709  cnextcn  23126  logfac2  26270  2sqmo  26490  outpasch  27020  trgcopyeu  27071  axcontlem12  27246  spanuni  29807  pjnmopi  30411  superpos  30617  atcvat4i  30660  rabeqsnd  30749  2ndresdju  30887  fpwrelmap  30970  nsgqusf1olem2  31501  ssmxidl  31544  locfinreflem  31692  cmpcref  31702  loop1cycl  32999  fneint  34464  neibastop3  34478  isbasisrelowllem1  35453  isbasisrelowllem2  35454  relowlssretop  35461  finxpreclem6  35494  ralssiun  35505  fin2so  35691  matunitlindflem2  35701  poimirlem26  35730  poimirlem27  35731  heicant  35739  ismblfin  35745  ovoliunnfl  35746  itg2gt0cn  35759  cvrat4  37384  pell14qrexpcl  40605  liminflimsupxrre  43248  odz2prm2pw  44903  prelrrx2b  45948  opnneilv  46090  intubeu  46158  unilbeu  46159