Theorem simp1lr 1233

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  lspsolvlem  19916  dmatcrng  21113  scmatcrng  21132  1marepvsma1  21194  mdetunilem7  21229  mat2pmatghm  21340  pmatcollpwscmatlem2  21400  mp2pm2mplem4  21419  ax5seg  26726  measinblem  31481  btwnconn1lem13  33562  athgt  36594  llnle  36656  lplnle  36678  lhpexle1  37146  lhpat3  37184  tendoicl  37934  cdlemk55b  38098  pellex  39439  ssfiunibd  41583  mullimc  41904  mullimcf  41911  icccncfext  42177  etransclem32  42558