Theorem simp1lr 1254

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 1149	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

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

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 1103

This theorem is referenced by:  lspsolvlem  21235  dmatcrng  22620  scmatcrng  22639  1marepvsma1  22701  mdetunilem7  22736  mat2pmatghm  22848  pmatcollpwscmatlem2  22908  mp2pm2mplem4  22927  ax5seg  29197  measinblem  34527  btwnconn1lem13  36462  athgt  40092  llnle  40154  lplnle  40176  lhpexle1  40644  lhpat3  40682  tendoicl  41432  cdlemk55b  41596  pellex  43424  ssfiunibd  45886  mullimc  46190  mullimcf  46197  icccncfext  46459  etransclem32  46838  uhgrimisgrgriclem  48550