Theorem simp1lr 1236

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

Assertion

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

Proof of Theorem simp1lr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  lspsolvlem  20484  dmatcrng  21731  scmatcrng  21750  1marepvsma1  21812  mdetunilem7  21847  mat2pmatghm  21959  pmatcollpwscmatlem2  22019  mp2pm2mplem4  22038  ax5seg  27439  measinblem  32324  btwnconn1lem13  34471  athgt  37696  llnle  37758  lplnle  37780  lhpexle1  38248  lhpat3  38286  tendoicl  39036  cdlemk55b  39200  pellex  40878  ssfiunibd  43102  mullimc  43412  mullimcf  43419  icccncfext  43683  etransclem32  44062