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  21335  dmatcrng  22730  scmatcrng  22749  1marepvsma1  22811  mdetunilem7  22846  mat2pmatghm  22961  pmatcollpwscmatlem2  23021  mp2pm2mplem4  23040  ax5seg  29403  measinblem  34739  btwnconn1lem13  36687  athgt  40337  llnle  40399  lplnle  40421  lhpexle1  40889  lhpat3  40927  tendoicl  41677  cdlemk55b  41841  pellex  43684  ssfiunibd  46150  mullimc  46454  mullimcf  46461  icccncfext  46723  etransclem32  47102  uhgrimisgrgriclem  48854