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  4633  tfindsg2  7838  tz7.49c  8414  domssl  8969  domssr  8970  ssenen  9115  pssnn  9132  unfi  9135  unwdomg  9537  cff1  10211  cfsmolem  10223  cfpwsdom  10537  wunex2  10691  mulgt0sr  11058  uzwo  12870  shftfval  15036  fsum2dlem  15736  fprod2dlem  15946  prmpwdvds  16875  ghmqusnsglem2  19213  ghmquskerlem2  19217  quscrng  21193  ring2idlqusb  21220  chfacfscmul0  22745  chfacfpmmul0  22749  tgtop  22860  neitr  23067  bwth  23297  tx1stc  23537  cnextcn  23954  logfac2  27128  2sqmo  27348  outpasch  28682  trgcopyeu  28733  axcontlem12  28902  spanuni  31473  pjnmopi  32077  superpos  32283  atcvat4i  32326  2ndresdju  32573  fpwrelmap  32656  chnind  32937  gsumwun  33005  gsumwrd2dccatlem  33006  wrdpmtrlast  33050  nsgqusf1olem2  33385  ssmxidl  33445  r1plmhm  33575  r1pquslmic  33576  ply1degltdimlem  33618  locfinreflem  33830  cmpcref  33840  loop1cycl  35124  fneint  36336  neibastop3  36350  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlssretop  37351  finxpreclem6  37384  ralssiun  37395  fin2so  37601  matunitlindflem2  37611  poimirlem26  37640  poimirlem27  37641  heicant  37649  ismblfin  37655  ovoliunnfl  37656  itg2gt0cn  37669  cvrat4  39437  pell14qrexpcl  42855  cantnfresb  43313  liminflimsupxrre  45815  modlt0b  47361  odz2prm2pw  47561  prelrrx2b  48700  opnneilv  48894  intubeu  48969  unilbeu  48970