Theorem expl 459

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  reximd2a  3267  rabeqsnd  4672  tfindsg2  7851  tz7.49c  8446  domssl  8994  domssr  8995  ssenen  9151  pssnn  9168  unfi  9172  pssnnOLD  9265  unwdomg  9579  cff1  10253  cfsmolem  10265  cfpwsdom  10579  wunex2  10733  mulgt0sr  11100  uzwo  12895  shftfval  15017  fsum2dlem  15716  fprod2dlem  15924  prmpwdvds  16837  quscrng  20878  chfacfscmul0  22360  chfacfpmmul0  22364  tgtop  22476  neitr  22684  bwth  22914  tx1stc  23154  cnextcn  23571  logfac2  26720  2sqmo  26940  outpasch  28006  trgcopyeu  28057  axcontlem12  28233  spanuni  30797  pjnmopi  31401  superpos  31607  atcvat4i  31650  2ndresdju  31874  fpwrelmap  31958  nsgqusf1olem2  32525  ghmquskerlem2  32530  ssmxidl  32590  ply1degltdimlem  32707  locfinreflem  32820  cmpcref  32830  loop1cycl  34128  fneint  35233  neibastop3  35247  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlssretop  36244  finxpreclem6  36277  ralssiun  36288  fin2so  36475  matunitlindflem2  36485  poimirlem26  36514  poimirlem27  36515  heicant  36523  ismblfin  36529  ovoliunnfl  36530  itg2gt0cn  36543  cvrat4  38314  pell14qrexpcl  41605  cantnfresb  42074  liminflimsupxrre  44533  odz2prm2pw  46231  ring2idlqusb  46795  prelrrx2b  47400  opnneilv  47541  intubeu  47609  unilbeu  47610