Theorem simpl1r 1221

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 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl1 1181	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7074  tfisi  7567  omopth2  8204  swrdsbslen  14020  swrdspsleq  14021  repswswrd  14140  ramub1lem1  16356  efgsfo  18859  lbspss  19848  maducoeval2  21243  madurid  21247  decpmatmullem  21373  mp2pm2mplem4  21411  llyrest  22087  ptbasin  22179  basqtop  22313  ustuqtop1  22844  mulcxp  25262  elwwlks2ons3im  27727  br8d  30355  isarchi2  30809  archiabllem2c  30819  cvmlift2lem10  32554  5segofs  33462  btwnconn1lem13  33555  2llnjaN  36696  paddasslem12  36961  lhp2lt  37131  lhpexle2lem  37139  lhpmcvr3  37155  lhpat3  37176  trlval3  37317  cdleme17b  37417  cdlemefr27cl  37533  cdlemg11b  37772  tendococl  37902  cdlemj3  37953  cdlemk35s-id  38068  cdlemk39s-id  38070  cdlemk53b  38086  cdlemk35u  38094  cdlemm10N  38248  dihopelvalcpre  38378  dihord6apre  38386  dihord5b  38389  dihglblem5apreN  38421  dihglblem2N  38424  dihmeetlem6  38439  dihmeetlem18N  38454  dvh3dim2  38578  dvh3dim3N  38579  jm2.25lem1  39588  limcleqr  41917  icccncfext  42162  fourierdlem87  42471  sge0seq  42721  smflimsuplem7  43093  itscnhlc0xyqsol  44745  itscnhlinecirc02plem2  44763