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  21109  dmatcrng  22458  scmatcrng  22477  1marepvsma1  22539  mdetunilem7  22574  mat2pmatghm  22686  pmatcollpwscmatlem2  22746  mp2pm2mplem4  22765  ax5seg  29023  measinblem  34397  btwnconn1lem13  36312  athgt  39821  llnle  39883  lplnle  39905  lhpexle1  40373  lhpat3  40411  tendoicl  41161  cdlemk55b  41325  pellex  43181  ssfiunibd  45660  mullimc  45965  mullimcf  45972  icccncfext  46234  etransclem32  46613  uhgrimisgrgriclem  48279