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  3248  rabeqsnd  4614  tfindsg2  7813  tz7.49c  8385  domssl  8945  domssr  8946  ssenen  9089  pssnn  9103  unfi  9105  unwdomg  9499  cff1  10180  cfsmolem  10192  cfpwsdom  10507  wunex2  10661  mulgt0sr  11028  uzwo  12861  shftfval  15032  fsum2dlem  15732  fprod2dlem  15945  prmpwdvds  16875  chnind  18587  ghmqusnsglem2  19256  ghmquskerlem2  19260  quscrng  21281  ring2idlqusb  21308  chfacfscmul0  22823  chfacfpmmul0  22827  tgtop  22938  neitr  23145  bwth  23375  tx1stc  23615  cnextcn  24032  logfac2  27180  2sqmo  27400  oldss  27862  outpasch  28823  trgcopyeu  28874  axcontlem12  29044  spanuni  31615  pjnmopi  32219  superpos  32425  atcvat4i  32468  2ndresdju  32722  fpwrelmap  32806  gsumwun  33137  gsumwrd2dccatlem  33138  wrdpmtrlast  33154  nsgqusf1olem2  33474  ssmxidl  33534  r1plmhm  33670  r1pquslmic  33671  ply1degltdimlem  33766  locfinreflem  33984  cmpcref  33994  loop1cycl  35319  fneint  36530  neibastop3  36544  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  finxpreclem6  37712  ralssiun  37723  fin2so  37928  matunitlindflem2  37938  poimirlem26  37967  poimirlem27  37968  heicant  37976  ismblfin  37982  ovoliunnfl  37983  itg2gt0cn  37996  cvrat4  39889  pell14qrexpcl  43295  cantnfresb  43752  liminflimsupxrre  46245  modlt0b  47811  odz2prm2pw  48020  prelrrx2b  49184  opnneilv  49378  intubeu  49453  unilbeu  49454