Theorem simpl1r 1242

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simpl1r

Step	Hyp	Ref	Expression
1		simplr 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl1 1202	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  soisores  7315  tfisi  7843  omopth2  8557  swrdsbslen  14692  swrdspsleq  14693  repswswrd  14811  ramub1lem1  17076  efgsfo  19800  lbspss  21172  maducoeval2  22758  madurid  22762  decpmatmullem  22889  mp2pm2mplem4  22927  llyrest  23603  ptbasin  23695  basqtop  23829  ustuqtop1  24359  mulcxp  26808  noetalem1  27863  ltmuls2  28322  elwwlks2ons3im  30212  br8d  32865  isarchi2  33418  archiabllem2c  33428  cvmlift2lem10  35675  5segofs  36369  btwnconn1lem13  36462  2llnjaN  40202  paddasslem12  40467  lhp2lt  40637  lhpexle2lem  40645  lhpmcvr3  40661  lhpat3  40682  trlval3  40823  cdleme17b  40923  cdlemefr27cl  41039  cdlemg11b  41278  tendococl  41408  cdlemj3  41459  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53b  41592  cdlemk35u  41600  cdlemm10N  41754  dihopelvalcpre  41884  dihord6apre  41892  dihord5b  41895  dihglblem5apreN  41927  dihglblem2N  41930  dihmeetlem6  41945  dihmeetlem18N  41960  dvh3dim2  42084  dvh3dim3N  42085  jm2.25lem1  43587  limcleqr  46216  icccncfext  46459  fourierdlem87  46765  sge0seq  47018  smflimsuplem7  47398  fsupdm  47414  finfdm  47418  itscnhlc0xyqsol  49396  itscnhlinecirc02plem2  49414