Theorem expl 456

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  reximd2a  3257  rabeqsnd  4672  tfindsg2  7865  tz7.49c  8465  domssl  9017  domssr  9018  ssenen  9174  pssnn  9191  unfi  9195  pssnnOLD  9288  unwdomg  9607  cff1  10281  cfsmolem  10293  cfpwsdom  10607  wunex2  10761  mulgt0sr  11128  uzwo  12925  shftfval  15049  fsum2dlem  15748  fprod2dlem  15956  prmpwdvds  16872  ghmquskerlem2  19240  quscrng  21179  ring2idlqusb  21204  chfacfscmul0  22790  chfacfpmmul0  22794  tgtop  22906  neitr  23114  bwth  23344  tx1stc  23584  cnextcn  24001  logfac2  27180  2sqmo  27400  outpasch  28615  trgcopyeu  28666  axcontlem12  28842  spanuni  31410  pjnmopi  32014  superpos  32220  atcvat4i  32263  2ndresdju  32492  fpwrelmap  32572  nsgqusf1olem2  33186  ghmqusnsglem2  33192  ssmxidl  33249  r1plmhm  33350  r1pquslmic  33351  ply1degltdimlem  33390  locfinreflem  33511  cmpcref  33521  loop1cycl  34817  fneint  35902  neibastop3  35916  isbasisrelowllem1  36904  isbasisrelowllem2  36905  relowlssretop  36912  finxpreclem6  36945  ralssiun  36956  fin2so  37150  matunitlindflem2  37160  poimirlem26  37189  poimirlem27  37190  heicant  37198  ismblfin  37204  ovoliunnfl  37205  itg2gt0cn  37218  cvrat4  38985  pell14qrexpcl  42352  cantnfresb  42818  liminflimsupxrre  45268  odz2prm2pw  46966  prelrrx2b  47899  opnneilv  48039  intubeu  48107  unilbeu  48108