Theorem expl 646

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 628	. 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 196  df-an 385

This theorem is referenced by:  reximd2a  2996  tfindsg2  6953  tz7.49c  7428  ssenen  8019  pssnn  8063  unwdomg  8372  cff1  8963  cfsmolem  8975  cfpwsdom  9285  wunex2  9439  mulgt0sr  9805  uzwo  11627  shftfval  13658  fsum2dlem  14343  fprod2dlem  14549  prmpwdvds  15446  quscrng  19061  chfacfscmul0  20482  chfacfpmmul0  20486  tgtop  20588  neitr  20794  bwth  21023  tx1stc  21263  cnextcn  21681  logfac2  24742  axcontlem12  25655  numclwwlkun  26606  spanuni  27787  pjnmopi  28391  superpos  28597  atcvat4i  28640  fpwrelmap  28896  2sqmo  28980  locfinreflem  29235  cmpcref  29245  fneint  31513  neibastop3  31527  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  finxpreclem6  32409  fin2so  32566  matunitlindflem2  32576  poimirlem26  32605  poimirlem27  32606  heicant  32614  ismblfin  32620  ovoliunnfl  32621  itg2gt0cn  32635  cvrat4  33747  pell14qrexpcl  36449  odz2prm2pw  40013