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  21103  dmatcrng  22440  scmatcrng  22459  1marepvsma1  22521  mdetunilem7  22556  mat2pmatghm  22668  pmatcollpwscmatlem2  22728  mp2pm2mplem4  22747  ax5seg  28917  measinblem  34251  btwnconn1lem13  36117  athgt  39475  llnle  39537  lplnle  39559  lhpexle1  40027  lhpat3  40065  tendoicl  40815  cdlemk55b  40979  pellex  42858  ssfiunibd  45338  mullimc  45645  mullimcf  45652  icccncfext  45916  etransclem32  46295  uhgrimisgrgriclem  47943