Theorem simpl1r 1226

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

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

This theorem is referenced by:  soisores  7302  tfisi  7835  omopth2  8548  swrdsbslen  14629  swrdspsleq  14630  repswswrd  14749  ramub1lem1  16997  efgsfo  19669  lbspss  20989  maducoeval2  22527  madurid  22531  decpmatmullem  22658  mp2pm2mplem4  22696  llyrest  23372  ptbasin  23464  basqtop  23598  ustuqtop1  24129  mulcxp  26594  noetalem1  27653  sltmul2  28074  elwwlks2ons3im  29884  br8d  32538  isarchi2  33139  archiabllem2c  33149  cvmlift2lem10  35299  5segofs  35994  btwnconn1lem13  36087  2llnjaN  39560  paddasslem12  39825  lhp2lt  39995  lhpexle2lem  40003  lhpmcvr3  40019  lhpat3  40040  trlval3  40181  cdleme17b  40281  cdlemefr27cl  40397  cdlemg11b  40636  tendococl  40766  cdlemj3  40817  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53b  40950  cdlemk35u  40958  cdlemm10N  41112  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihglblem5apreN  41285  dihglblem2N  41288  dihmeetlem6  41303  dihmeetlem18N  41318  dvh3dim2  41442  dvh3dim3N  41443  jm2.25lem1  42987  limcleqr  45642  icccncfext  45885  fourierdlem87  46191  sge0seq  46444  smflimsuplem7  46824  fsupdm  46840  finfdm  46844  itscnhlc0xyqsol  48754  itscnhlinecirc02plem2  48772