Theorem simp1lr 1237

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 1087

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 1089

This theorem is referenced by:  lspsolvlem  21167  dmatcrng  22529  scmatcrng  22548  1marepvsma1  22610  mdetunilem7  22645  mat2pmatghm  22757  pmatcollpwscmatlem2  22817  mp2pm2mplem4  22836  ax5seg  28971  measinblem  34184  btwnconn1lem13  36063  athgt  39413  llnle  39475  lplnle  39497  lhpexle1  39965  lhpat3  40003  tendoicl  40753  cdlemk55b  40917  pellex  42791  ssfiunibd  45224  mullimc  45537  mullimcf  45544  icccncfext  45808  etransclem32  46187  uhgrimisgrgriclem  47782