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  3275  rabeqsnd  4691  tfindsg2  7899  tz7.49c  8502  domssl  9058  domssr  9059  ssenen  9217  pssnn  9234  unfi  9238  unwdomg  9653  cff1  10327  cfsmolem  10339  cfpwsdom  10653  wunex2  10807  mulgt0sr  11174  uzwo  12976  shftfval  15119  fsum2dlem  15818  fprod2dlem  16028  prmpwdvds  16951  ghmqusnsglem2  19321  ghmquskerlem2  19325  quscrng  21316  ring2idlqusb  21343  chfacfscmul0  22885  chfacfpmmul0  22889  tgtop  23001  neitr  23209  bwth  23439  tx1stc  23679  cnextcn  24096  logfac2  27279  2sqmo  27499  outpasch  28781  trgcopyeu  28832  axcontlem12  29008  spanuni  31576  pjnmopi  32180  superpos  32386  atcvat4i  32429  2ndresdju  32667  fpwrelmap  32747  chnind  32983  wrdpmtrlast  33086  nsgqusf1olem2  33407  ssmxidl  33467  r1plmhm  33595  r1pquslmic  33596  ply1degltdimlem  33635  locfinreflem  33786  cmpcref  33796  loop1cycl  35105  fneint  36314  neibastop3  36328  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlssretop  37329  finxpreclem6  37362  ralssiun  37373  fin2so  37567  matunitlindflem2  37577  poimirlem26  37606  poimirlem27  37607  heicant  37615  ismblfin  37621  ovoliunnfl  37622  itg2gt0cn  37635  cvrat4  39400  pell14qrexpcl  42823  cantnfresb  43286  liminflimsupxrre  45738  odz2prm2pw  47437  prelrrx2b  48448  opnneilv  48588  intubeu  48656  unilbeu  48657