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 207  df-an 396

This theorem is referenced by:  reximd2a  3247  rabeqsnd  4627  tfindsg2  7806  tz7.49c  8379  domssl  8939  domssr  8940  ssenen  9083  pssnn  9097  unfi  9099  unwdomg  9493  cff1  10172  cfsmolem  10184  cfpwsdom  10499  wunex2  10653  mulgt0sr  11020  uzwo  12828  shftfval  14997  fsum2dlem  15697  fprod2dlem  15907  prmpwdvds  16836  chnind  18548  ghmqusnsglem2  19214  ghmquskerlem2  19218  quscrng  21242  ring2idlqusb  21269  chfacfscmul0  22806  chfacfpmmul0  22810  tgtop  22921  neitr  23128  bwth  23358  tx1stc  23598  cnextcn  24015  logfac2  27188  2sqmo  27408  oldss  27860  outpasch  28810  trgcopyeu  28861  axcontlem12  29031  spanuni  31602  pjnmopi  32206  superpos  32412  atcvat4i  32455  2ndresdju  32709  fpwrelmap  32793  gsumwun  33139  gsumwrd2dccatlem  33140  wrdpmtrlast  33156  nsgqusf1olem2  33476  ssmxidl  33536  r1plmhm  33672  r1pquslmic  33673  ply1degltdimlem  33760  locfinreflem  33978  cmpcref  33988  loop1cycl  35312  fneint  36523  neibastop3  36537  isbasisrelowllem1  37531  isbasisrelowllem2  37532  relowlssretop  37539  finxpreclem6  37572  ralssiun  37583  fin2so  37779  matunitlindflem2  37789  poimirlem26  37818  poimirlem27  37819  heicant  37827  ismblfin  37833  ovoliunnfl  37834  itg2gt0cn  37847  cvrat4  39740  pell14qrexpcl  43145  cantnfresb  43602  liminflimsupxrre  46097  modlt0b  47645  odz2prm2pw  47845  prelrrx2b  48996  opnneilv  49190  intubeu  49265  unilbeu  49266