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  21067  dmatcrng  22405  scmatcrng  22424  1marepvsma1  22486  mdetunilem7  22521  mat2pmatghm  22633  pmatcollpwscmatlem2  22693  mp2pm2mplem4  22712  ax5seg  28901  measinblem  34186  btwnconn1lem13  36072  athgt  39435  llnle  39497  lplnle  39519  lhpexle1  39987  lhpat3  40025  tendoicl  40775  cdlemk55b  40939  pellex  42808  ssfiunibd  45291  mullimc  45598  mullimcf  45605  icccncfext  45869  etransclem32  46248  uhgrimisgrgriclem  47914