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 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1134	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  21144  dmatcrng  22508  scmatcrng  22527  1marepvsma1  22589  mdetunilem7  22624  mat2pmatghm  22736  pmatcollpwscmatlem2  22796  mp2pm2mplem4  22815  ax5seg  28953  measinblem  34221  btwnconn1lem13  36100  athgt  39458  llnle  39520  lplnle  39542  lhpexle1  40010  lhpat3  40048  tendoicl  40798  cdlemk55b  40962  pellex  42846  ssfiunibd  45321  mullimc  45631  mullimcf  45638  icccncfext  45902  etransclem32  46281  uhgrimisgrgriclem  47898