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

This theorem is referenced by:  lspsolvlem  20319  dmatcrng  21559  scmatcrng  21578  1marepvsma1  21640  mdetunilem7  21675  mat2pmatghm  21787  pmatcollpwscmatlem2  21847  mp2pm2mplem4  21866  ax5seg  27209  measinblem  32088  btwnconn1lem13  34328  athgt  37397  llnle  37459  lplnle  37481  lhpexle1  37949  lhpat3  37987  tendoicl  38737  cdlemk55b  38901  pellex  40573  ssfiunibd  42738  mullimc  43047  mullimcf  43054  icccncfext  43318  etransclem32  43697