Theorem expl 647

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  reximd2a  3042  tfindsg2  7103  tz7.49c  7586  ssenen  8175  pssnn  8219  unwdomg  8530  cff1  9118  cfsmolem  9130  cfpwsdom  9444  wunex2  9598  mulgt0sr  9964  uzwo  11789  shftfval  13854  fsum2dlem  14545  fprod2dlem  14754  prmpwdvds  15655  quscrng  19288  chfacfscmul0  20711  chfacfpmmul0  20715  tgtop  20825  neitr  21032  bwth  21261  tx1stc  21501  cnextcn  21918  logfac2  24987  axcontlem12  25900  spanuni  28531  pjnmopi  29135  superpos  29341  atcvat4i  29384  rabeqsnd  29468  fpwrelmap  29636  2sqmo  29777  locfinreflem  30035  cmpcref  30045  fneint  32468  neibastop3  32482  bj-ismooredr2  33190  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlssretop  33341  finxpreclem6  33363  fin2so  33526  matunitlindflem2  33536  poimirlem26  33565  poimirlem27  33566  heicant  33574  ismblfin  33580  ovoliunnfl  33581  itg2gt0cn  33595  cvrat4  35047  pell14qrexpcl  37748  odz2prm2pw  41800