Theorem expl 463

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 425	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 416	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reximd2a  3272  rabeqsnd  4629  tfindsg2  7856  tz7.49c  8434  domssl  9003  domssr  9004  ssenen  9148  pssnn  9162  unfi  9164  unwdomg  9556  cff1  10307  cfsmolem  10319  cfpwsdom  10640  wunex2  10794  mulgt0sr  11161  uzwo  13007  shftfval  15190  fsum2dlem  15903  fprod2dlem  16114  prmpwdvds  17043  chnind  18756  ghmqusnsglem2  19456  ghmquskerlem2  19460  quscrng  21540  ring2idlqusb  21567  matunitlindflem2  22956  chfacfscmul0  23137  chfacfpmmul0  23141  tgtop  23252  neitr  23459  bwth  23689  tx1stc  23930  cnextcn  24347  logfac2  27507  2sqmo  27727  oldss  28189  tgsegconeu  28882  tglnpt3  29055  tglnpt4  29056  outpasch  29166  trgcopyeu  29246  angmgmlem  29328  prlngmo2  29367  axcontlem12  29486  loop1cycl  30677  spanuni  32079  pjnmopi  32683  superpos  32889  atcvat4i  32932  2ndresdju  33176  fpwrelmap  33258  gsumwun  33570  gsumwrd2dccatlem  33571  wrdpmtrlast  33587  nsgqusf1olem2  33898  ssmxidl  33932  r1plmhm  34074  r1pquslmic  34075  ply1degltdimlem  34187  locfinreflem  34405  cmpcref  34415  fneint  37058  neibastop3  37072  isbasisrelowllem1  38198  isbasisrelowllem2  38199  relowlssretop  38206  finxpreclem6  38239  ralssiun  38250  fin2so  38450  poimirlem26  38484  poimirlem27  38485  heicant  38493  ismblfin  38499  ovoliunnfl  38500  itg2gt0cn  38513  cvrat4  40420  pell14qrexpcl  43812  cantnfresb  44269  liminflimsupxrre  46749  modlt0b  48361  odz2prm2pw  48570  prelrrx2b  49748  opnneilv  49939  intubeu  50014  unilbeu  50015