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  7267  tfisi  7795  omopth2  8505  swrdsbslen  14574  swrdspsleq  14575  repswswrd  14693  ramub1lem1  16940  efgsfo  19653  lbspss  21018  maducoeval2  22556  madurid  22560  decpmatmullem  22687  mp2pm2mplem4  22725  llyrest  23401  ptbasin  23493  basqtop  23627  ustuqtop1  24157  mulcxp  26622  noetalem1  27681  sltmul2  28111  elwwlks2ons3im  29934  br8d  32593  isarchi2  33161  archiabllem2c  33171  cvmlift2lem10  35377  5segofs  36071  btwnconn1lem13  36164  2llnjaN  39685  paddasslem12  39950  lhp2lt  40120  lhpexle2lem  40128  lhpmcvr3  40144  lhpat3  40165  trlval3  40306  cdleme17b  40406  cdlemefr27cl  40522  cdlemg11b  40761  tendococl  40891  cdlemj3  40942  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk53b  41075  cdlemk35u  41083  cdlemm10N  41237  dihopelvalcpre  41367  dihord6apre  41375  dihord5b  41378  dihglblem5apreN  41410  dihglblem2N  41413  dihmeetlem6  41428  dihmeetlem18N  41443  dvh3dim2  41567  dvh3dim3N  41568  jm2.25lem1  43115  limcleqr  45766  icccncfext  46009  fourierdlem87  46315  sge0seq  46568  smflimsuplem7  46948  fsupdm  46964  finfdm  46968  itscnhlc0xyqsol  48890  itscnhlinecirc02plem2  48908