Theorem simp1lr 1239

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  lspsolvlem  21101  dmatcrng  22450  scmatcrng  22469  1marepvsma1  22531  mdetunilem7  22566  mat2pmatghm  22678  pmatcollpwscmatlem2  22738  mp2pm2mplem4  22757  ax5seg  28994  measinblem  34358  btwnconn1lem13  36274  athgt  39753  llnle  39815  lplnle  39837  lhpexle1  40305  lhpat3  40343  tendoicl  41093  cdlemk55b  41257  pellex  43113  ssfiunibd  45593  mullimc  45898  mullimcf  45905  icccncfext  46167  etransclem32  46546  uhgrimisgrgriclem  48212