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  21426  dmatcrng  22823  scmatcrng  22842  1marepvsma1  22904  mdetunilem7  22939  mat2pmatghm  23054  pmatcollpwscmatlem2  23114  mp2pm2mplem4  23133  ax5seg  29522  measinblem  34900  btwnconn1lem13  36957  athgt  40607  llnle  40669  lplnle  40691  lhpexle1  41159  lhpat3  41197  tendoicl  41947  cdlemk55b  42111  pellex  43936  ssfiunibd  46419  mullimc  46722  mullimcf  46729  icccncfext  46991  etransclem32  47370  uhgrimisgrgriclem  49122