Theorem simp1lr 1234

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 1130	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

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

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  lspsolvlem  19907  dmatcrng  21107  scmatcrng  21126  1marepvsma1  21188  mdetunilem7  21223  mat2pmatghm  21335  pmatcollpwscmatlem2  21395  mp2pm2mplem4  21414  ax5seg  26732  measinblem  31589  btwnconn1lem13  33673  athgt  36752  llnle  36814  lplnle  36836  lhpexle1  37304  lhpat3  37342  tendoicl  38092  cdlemk55b  38256  pellex  39776  ssfiunibd  41941  mullimc  42258  mullimcf  42265  icccncfext  42529  etransclem32  42908