Theorem simp1lr 1235

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  lspsolvlem  20900  dmatcrng  22224  scmatcrng  22243  1marepvsma1  22305  mdetunilem7  22340  mat2pmatghm  22452  pmatcollpwscmatlem2  22512  mp2pm2mplem4  22531  ax5seg  28463  measinblem  33516  btwnconn1lem13  35375  athgt  38630  llnle  38692  lplnle  38714  lhpexle1  39182  lhpat3  39220  tendoicl  39970  cdlemk55b  40134  pellex  41875  ssfiunibd  44317  mullimc  44630  mullimcf  44637  icccncfext  44901  etransclem32  45280