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  21089  dmatcrng  22427  scmatcrng  22446  1marepvsma1  22508  mdetunilem7  22543  mat2pmatghm  22655  pmatcollpwscmatlem2  22715  mp2pm2mplem4  22734  ax5seg  28927  measinblem  34244  btwnconn1lem13  36154  athgt  39565  llnle  39627  lplnle  39649  lhpexle1  40117  lhpat3  40155  tendoicl  40905  cdlemk55b  41069  pellex  42942  ssfiunibd  45424  mullimc  45730  mullimcf  45737  icccncfext  45999  etransclem32  46378  uhgrimisgrgriclem  48044