Theorem expl 460

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reximd2a  3312  tfindsg2  7570  tz7.49c  8076  ssenen  8685  pssnn  8730  unwdomg  9042  cff1  9674  cfsmolem  9686  cfpwsdom  10000  wunex2  10154  mulgt0sr  10521  uzwo  12305  shftfval  14423  fsum2dlem  15119  fprod2dlem  15328  prmpwdvds  16234  quscrng  20007  chfacfscmul0  21460  chfacfpmmul0  21464  tgtop  21575  neitr  21782  bwth  22012  tx1stc  22252  cnextcn  22669  logfac2  25787  2sqmo  26007  outpasch  26535  trgcopyeu  26586  axcontlem12  26755  spanuni  29315  pjnmopi  29919  superpos  30125  atcvat4i  30168  rabeqsnd  30258  fpwrelmap  30463  ssmxidl  30974  locfinreflem  31099  cmpcref  31109  loop1cycl  32379  fneint  33691  neibastop3  33705  isbasisrelowllem1  34630  isbasisrelowllem2  34631  relowlssretop  34638  finxpreclem6  34671  ralssiun  34682  fin2so  34873  matunitlindflem2  34883  poimirlem26  34912  poimirlem27  34913  heicant  34921  ismblfin  34927  ovoliunnfl  34928  itg2gt0cn  34941  cvrat4  36573  pell14qrexpcl  39457  liminflimsupxrre  42091  odz2prm2pw  43719  prelrrx2b  44695