Theorem simp1lr 1250

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  lspsolvlem  21192  dmatcrng  22542  scmatcrng  22561  1marepvsma1  22623  mdetunilem7  22658  mat2pmatghm  22770  pmatcollpwscmatlem2  22830  mp2pm2mplem4  22849  ax5seg  29085  measinblem  34478  btwnconn1lem13  36413  athgt  40044  llnle  40106  lplnle  40128  lhpexle1  40596  lhpat3  40634  tendoicl  41384  cdlemk55b  41548  pellex  43376  ssfiunibd  45852  mullimc  46156  mullimcf  46163  icccncfext  46425  etransclem32  46804  uhgrimisgrgriclem  48516