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  3267  rabeqsnd  4674  tfindsg2  7883  tz7.49c  8485  domssl  9037  domssr  9038  ssenen  9190  pssnn  9207  unfi  9210  unwdomg  9622  cff1  10296  cfsmolem  10308  cfpwsdom  10622  wunex2  10776  mulgt0sr  11143  uzwo  12951  shftfval  15106  fsum2dlem  15803  fprod2dlem  16013  prmpwdvds  16938  ghmqusnsglem2  19312  ghmquskerlem2  19316  quscrng  21311  ring2idlqusb  21338  chfacfscmul0  22880  chfacfpmmul0  22884  tgtop  22996  neitr  23204  bwth  23434  tx1stc  23674  cnextcn  24091  logfac2  27276  2sqmo  27496  outpasch  28778  trgcopyeu  28829  axcontlem12  29005  spanuni  31573  pjnmopi  32177  superpos  32383  atcvat4i  32426  2ndresdju  32666  fpwrelmap  32751  chnind  32985  gsumwun  33051  gsumwrd2dccatlem  33052  wrdpmtrlast  33096  nsgqusf1olem2  33422  ssmxidl  33482  r1plmhm  33610  r1pquslmic  33611  ply1degltdimlem  33650  locfinreflem  33801  cmpcref  33811  loop1cycl  35122  fneint  36331  neibastop3  36345  isbasisrelowllem1  37338  isbasisrelowllem2  37339  relowlssretop  37346  finxpreclem6  37379  ralssiun  37390  fin2so  37594  matunitlindflem2  37604  poimirlem26  37633  poimirlem27  37634  heicant  37642  ismblfin  37648  ovoliunnfl  37649  itg2gt0cn  37662  cvrat4  39426  pell14qrexpcl  42855  cantnfresb  43314  liminflimsupxrre  45773  odz2prm2pw  47488  prelrrx2b  48564  opnneilv  48705  intubeu  48773  unilbeu  48774