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  21140  dmatcrng  22467  scmatcrng  22486  1marepvsma1  22548  mdetunilem7  22583  mat2pmatghm  22695  pmatcollpwscmatlem2  22755  mp2pm2mplem4  22774  ax5seg  29007  measinblem  34364  btwnconn1lem13  36281  athgt  39902  llnle  39964  lplnle  39986  lhpexle1  40454  lhpat3  40492  tendoicl  41242  cdlemk55b  41406  pellex  43263  ssfiunibd  45742  mullimc  46046  mullimcf  46053  icccncfext  46315  etransclem32  46694  uhgrimisgrgriclem  48406