Theorem simp1lr 1256

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

Assertion

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

Proof of Theorem simp1lr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  lspsolvlem  21303  dmatcrng  22696  scmatcrng  22715  1marepvsma1  22777  mdetunilem7  22812  mat2pmatghm  22924  pmatcollpwscmatlem2  22984  mp2pm2mplem4  23003  ax5seg  29325  measinblem  34642  btwnconn1lem13  36612  athgt  40271  llnle  40333  lplnle  40355  lhpexle1  40823  lhpat3  40861  tendoicl  41611  cdlemk55b  41775  pellex  43603  ssfiunibd  46069  mullimc  46373  mullimcf  46380  icccncfext  46642  etransclem32  47021  uhgrimisgrgriclem  48736