Theorem simp1lr 1275

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  lspsolvlem  19538  dmatcrng  20713  scmatcrng  20732  1marepvsma1  20794  mdetunilem7  20829  mat2pmatghm  20942  pmatcollpwscmatlem2  21002  mp2pm2mplem4  21021  ax5seg  26287  measinblem  30881  btwnconn1lem13  32795  athgt  35612  llnle  35674  lplnle  35696  lhpexle1  36164  lhpat3  36202  tendoicl  36952  cdlemk55b  37116  pellex  38363  ssfiunibd  40436  mullimc  40760  mullimcf  40767  icccncfext  41032  etransclem32  41414