Theorem simp1lr 1238

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  lspsolvlem  21052  dmatcrng  22389  scmatcrng  22408  1marepvsma1  22470  mdetunilem7  22505  mat2pmatghm  22617  pmatcollpwscmatlem2  22677  mp2pm2mplem4  22696  ax5seg  28865  measinblem  34210  btwnconn1lem13  36087  athgt  39450  llnle  39512  lplnle  39534  lhpexle1  40002  lhpat3  40040  tendoicl  40790  cdlemk55b  40954  pellex  42823  ssfiunibd  45307  mullimc  45614  mullimcf  45621  icccncfext  45885  etransclem32  46264  uhgrimisgrgriclem  47930