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  7261  tfisi  7789  omopth2  8499  swrdsbslen  14569  swrdspsleq  14570  repswswrd  14688  ramub1lem1  16935  efgsfo  19649  lbspss  21014  maducoeval2  22553  madurid  22557  decpmatmullem  22684  mp2pm2mplem4  22722  llyrest  23398  ptbasin  23490  basqtop  23624  ustuqtop1  24154  mulcxp  26619  noetalem1  27678  sltmul2  28108  elwwlks2ons3im  29930  br8d  32586  isarchi2  33149  archiabllem2c  33159  cvmlift2lem10  35344  5segofs  36039  btwnconn1lem13  36132  2llnjaN  39604  paddasslem12  39869  lhp2lt  40039  lhpexle2lem  40047  lhpmcvr3  40063  lhpat3  40084  trlval3  40225  cdleme17b  40325  cdlemefr27cl  40441  cdlemg11b  40680  tendococl  40810  cdlemj3  40861  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk53b  40994  cdlemk35u  41002  cdlemm10N  41156  dihopelvalcpre  41286  dihord6apre  41294  dihord5b  41297  dihglblem5apreN  41329  dihglblem2N  41332  dihmeetlem6  41347  dihmeetlem18N  41362  dvh3dim2  41486  dvh3dim3N  41487  jm2.25lem1  43030  limcleqr  45681  icccncfext  45924  fourierdlem87  46230  sge0seq  46483  smflimsuplem7  46863  fsupdm  46879  finfdm  46883  itscnhlc0xyqsol  48796  itscnhlinecirc02plem2  48814