Theorem simp1lr 1256

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1lr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Proof of Theorem simp1lr

Step	Hyp	Ref	Expression
1		simplr 781	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1151	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

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

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  df-3an 1105

This theorem is used by:  lspsolvlem  21453  dmatcrng  22850  scmatcrng  22869  1marepvsma1  22931  mdetunilem7  22966  mat2pmatghm  23081  pmatcollpwscmatlem2  23141  mp2pm2mplem4  23160  ax5seg  29549  measinblem  34936  btwnconn1lem13  37055  athgt  40716  llnle  40778  lplnle  40800  lhpexle1  41268  lhpat3  41306  tendoicl  42056  cdlemk55b  42220  pellex  44046  ssfiunibd  46540  mullimc  46843  mullimcf  46850  icccncfext  47112  etransclem32  47491  uhgrimisgrgriclem  49243