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  7273  tfisi  7801  omopth2  8511  swrdsbslen  14588  swrdspsleq  14589  repswswrd  14707  ramub1lem1  16954  efgsfo  19668  lbspss  21034  maducoeval2  22584  madurid  22588  decpmatmullem  22715  mp2pm2mplem4  22753  llyrest  23429  ptbasin  23521  basqtop  23655  ustuqtop1  24185  mulcxp  26650  noetalem1  27709  ltmuls2  28167  elwwlks2ons3im  30027  br8d  32686  isarchi2  33267  archiabllem2c  33277  cvmlift2lem10  35506  5segofs  36200  btwnconn1lem13  36293  2llnjaN  39822  paddasslem12  40087  lhp2lt  40257  lhpexle2lem  40265  lhpmcvr3  40281  lhpat3  40302  trlval3  40443  cdleme17b  40543  cdlemefr27cl  40659  cdlemg11b  40898  tendococl  41028  cdlemj3  41079  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk53b  41212  cdlemk35u  41220  cdlemm10N  41374  dihopelvalcpre  41504  dihord6apre  41512  dihord5b  41515  dihglblem5apreN  41547  dihglblem2N  41550  dihmeetlem6  41565  dihmeetlem18N  41580  dvh3dim2  41704  dvh3dim3N  41705  jm2.25lem1  43236  limcleqr  45884  icccncfext  46127  fourierdlem87  46433  sge0seq  46686  smflimsuplem7  47066  fsupdm  47082  finfdm  47086  itscnhlc0xyqsol  49007  itscnhlinecirc02plem2  49025