Theorem expl 458

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  reximd2a  3245  tfindsg2  7708  tz7.49c  8277  ssenen  8938  pssnn  8951  unfi  8955  pssnnOLD  9040  unwdomg  9343  cff1  10014  cfsmolem  10026  cfpwsdom  10340  wunex2  10494  mulgt0sr  10861  uzwo  12651  shftfval  14781  fsum2dlem  15482  fprod2dlem  15690  prmpwdvds  16605  quscrng  20511  chfacfscmul0  22007  chfacfpmmul0  22011  tgtop  22123  neitr  22331  bwth  22561  tx1stc  22801  cnextcn  23218  logfac2  26365  2sqmo  26585  outpasch  27116  trgcopyeu  27167  axcontlem12  27343  spanuni  29906  pjnmopi  30510  superpos  30716  atcvat4i  30759  rabeqsnd  30848  2ndresdju  30986  fpwrelmap  31068  nsgqusf1olem2  31599  ssmxidl  31642  locfinreflem  31790  cmpcref  31800  loop1cycl  33099  fneint  34537  neibastop3  34551  isbasisrelowllem1  35526  isbasisrelowllem2  35527  relowlssretop  35534  finxpreclem6  35567  ralssiun  35578  fin2so  35764  matunitlindflem2  35774  poimirlem26  35803  poimirlem27  35804  heicant  35812  ismblfin  35818  ovoliunnfl  35819  itg2gt0cn  35832  cvrat4  37457  pell14qrexpcl  40689  liminflimsupxrre  43358  odz2prm2pw  45015  prelrrx2b  46060  opnneilv  46202  intubeu  46270  unilbeu  46271