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 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1151	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  lspsolvlem  21247  dmatcrng  22640  scmatcrng  22659  1marepvsma1  22721  mdetunilem7  22756  mat2pmatghm  22868  pmatcollpwscmatlem2  22928  mp2pm2mplem4  22947  ax5seg  29266  measinblem  34588  btwnconn1lem13  36569  athgt  40208  llnle  40270  lplnle  40292  lhpexle1  40760  lhpat3  40798  tendoicl  41548  cdlemk55b  41712  pellex  43542  ssfiunibd  46008  mullimc  46312  mullimcf  46319  icccncfext  46581  etransclem32  46960  uhgrimisgrgriclem  48672