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  3256  rabeqsnd  4650  tfindsg2  7862  tz7.49c  8465  domssl  9017  domssr  9018  ssenen  9170  pssnn  9187  unfi  9190  unwdomg  9603  cff1  10277  cfsmolem  10289  cfpwsdom  10603  wunex2  10757  mulgt0sr  11124  uzwo  12932  shftfval  15094  fsum2dlem  15791  fprod2dlem  16001  prmpwdvds  16929  ghmqusnsglem2  19269  ghmquskerlem2  19273  quscrng  21249  ring2idlqusb  21276  chfacfscmul0  22801  chfacfpmmul0  22805  tgtop  22916  neitr  23123  bwth  23353  tx1stc  23593  cnextcn  24010  logfac2  27185  2sqmo  27405  outpasch  28739  trgcopyeu  28790  axcontlem12  28959  spanuni  31530  pjnmopi  32134  superpos  32340  atcvat4i  32383  2ndresdju  32632  fpwrelmap  32715  chnind  32996  gsumwun  33064  gsumwrd2dccatlem  33065  wrdpmtrlast  33109  nsgqusf1olem2  33434  ssmxidl  33494  r1plmhm  33624  r1pquslmic  33625  ply1degltdimlem  33667  locfinreflem  33876  cmpcref  33886  loop1cycl  35164  fneint  36371  neibastop3  36385  isbasisrelowllem1  37378  isbasisrelowllem2  37379  relowlssretop  37386  finxpreclem6  37419  ralssiun  37430  fin2so  37636  matunitlindflem2  37646  poimirlem26  37675  poimirlem27  37676  heicant  37684  ismblfin  37690  ovoliunnfl  37691  itg2gt0cn  37704  cvrat4  39467  pell14qrexpcl  42857  cantnfresb  43315  liminflimsupxrre  45813  odz2prm2pw  47544  prelrrx2b  48661  opnneilv  48850  intubeu  48925  unilbeu  48926