Theorem expl 463

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  reximd2a  3274  rabeqsnd  4633  tfindsg2  7861  tz7.49c  8438  domssl  9007  domssr  9008  ssenen  9152  pssnn  9166  unfi  9168  unwdomg  9559  cff1  10263  cfsmolem  10275  cfpwsdom  10596  wunex2  10750  mulgt0sr  11117  uzwo  12963  shftfval  15145  fsum2dlem  15858  fprod2dlem  16071  prmpwdvds  17000  chnind  18713  ghmqusnsglem2  19409  ghmquskerlem2  19413  quscrng  21487  ring2idlqusb  21514  matunitlindflem2  22903  chfacfscmul0  23084  chfacfpmmul0  23088  tgtop  23199  neitr  23406  bwth  23636  tx1stc  23877  cnextcn  24294  logfac2  27451  2sqmo  27671  oldss  28133  tgsegconeu  28826  tglnpt3  28999  tglnpt4  29000  outpasch  29110  trgcopyeu  29190  prlngmo2  29299  axcontlem12  29418  loop1cycl  30609  spanuni  32011  pjnmopi  32615  superpos  32821  atcvat4i  32864  2ndresdju  33109  fpwrelmap  33191  gsumwun  33503  gsumwrd2dccatlem  33504  wrdpmtrlast  33520  nsgqusf1olem2  33830  ssmxidl  33864  r1plmhm  34006  r1pquslmic  34007  ply1degltdimlem  34119  locfinreflem  34337  cmpcref  34347  fneint  36954  neibastop3  36968  isbasisrelowllem1  38096  isbasisrelowllem2  38097  relowlssretop  38104  finxpreclem6  38137  ralssiun  38148  fin2so  38348  poimirlem26  38382  poimirlem27  38383  heicant  38391  ismblfin  38397  ovoliunnfl  38398  itg2gt0cn  38411  cvrat4  40303  pell14qrexpcl  43695  cantnfresb  44152  liminflimsupxrre  46632  modlt0b  48244  odz2prm2pw  48453  prelrrx2b  49631  opnneilv  49822  intubeu  49897  unilbeu  49898