Theorem simp1lr 1118

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  lspsolvlem  18963  dmatcrng  20127  scmatcrng  20146  1marepvsma1  20208  mdetunilem7  20243  mat2pmatghm  20354  pmatcollpwscmatlem2  20414  mp2pm2mplem4  20433  ax5seg  25618  measinblem  29610  btwnconn1lem13  31376  athgt  33760  llnle  33822  lplnle  33844  lhpexle1  34312  lhpat3  34350  tendoicl  35102  cdlemk55b  35266  pellex  36417  ssfiunibd  38464  mullimc  38683  mullimcf  38690  icccncfext  38773  etransclem32  39159  clwwnisshclwwsn  41237