Theorem simpl1r 1133

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

Assertion

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

Proof of Theorem simpl1r

Step	Hyp	Ref	Expression
1		simp1r 1106	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	adantr 480	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  soisores  6617  tfisi  7100  omopth2  7709  swrdsbslen  13494  swrdspsleq  13495  repswswrd  13577  ramub1lem1  15777  efgsfo  18198  lbspss  19130  maducoeval2  20494  madurid  20498  decpmatmullem  20624  mp2pm2mplem4  20662  llyrest  21336  ptbasin  21428  basqtop  21562  ustuqtop1  22092  mulcxp  24476  elwwlks2ons3im  26919  br8d  29548  isarchi2  29867  archiabllem2c  29877  cvmlift2lem10  31420  5segofs  32238  btwnconn1lem13  32331  2llnjaN  35170  paddasslem12  35435  lhp2lt  35605  lhpexle2lem  35613  lhpmcvr3  35629  lhpat3  35650  trlval3  35792  cdleme17b  35892  cdlemefr27cl  36008  cdlemg11b  36247  tendococl  36377  cdlemj3  36428  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk53b  36561  cdlemk35u  36569  cdlemm10N  36724  dihopelvalcpre  36854  dihord6apre  36862  dihord5b  36865  dihglblem5apreN  36897  dihglblem2N  36900  dihmeetlem6  36915  dihmeetlem18N  36930  dvh3dim2  37054  dvh3dim3N  37055  jm2.25lem1  37882  limcleqr  40194  icccncfext  40418  fourierdlem87  40728  sge0seq  40981  smflimsuplem7  41353