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  21400  dmatcrng  22797  scmatcrng  22816  1marepvsma1  22878  mdetunilem7  22913  mat2pmatghm  23028  pmatcollpwscmatlem2  23088  mp2pm2mplem4  23107  ax5seg  29498  measinblem  34835  btwnconn1lem13  36834  athgt  40481  llnle  40543  lplnle  40565  lhpexle1  41033  lhpat3  41071  tendoicl  41821  cdlemk55b  41985  pellex  43795  ssfiunibd  46268  mullimc  46572  mullimcf  46579  icccncfext  46841  etransclem32  47220  uhgrimisgrgriclem  48972