Theorem simpl1r 1223

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  soisores  7191  tfisi  7693  omopth2  8391  swrdsbslen  14358  swrdspsleq  14359  repswswrd  14478  ramub1lem1  16708  efgsfo  19326  lbspss  20325  maducoeval2  21770  madurid  21774  decpmatmullem  21901  mp2pm2mplem4  21939  llyrest  22617  ptbasin  22709  basqtop  22843  ustuqtop1  23374  mulcxp  25821  elwwlks2ons3im  28298  br8d  30929  isarchi2  31418  archiabllem2c  31428  cvmlift2lem10  33253  noetalem1  33923  5segofs  34287  btwnconn1lem13  34380  2llnjaN  37559  paddasslem12  37824  lhp2lt  37994  lhpexle2lem  38002  lhpmcvr3  38018  lhpat3  38039  trlval3  38180  cdleme17b  38280  cdlemefr27cl  38396  cdlemg11b  38635  tendococl  38765  cdlemj3  38816  cdlemk35s-id  38931  cdlemk39s-id  38933  cdlemk53b  38949  cdlemk35u  38957  cdlemm10N  39111  dihopelvalcpre  39241  dihord6apre  39249  dihord5b  39252  dihglblem5apreN  39284  dihglblem2N  39287  dihmeetlem6  39302  dihmeetlem18N  39317  dvh3dim2  39441  dvh3dim3N  39442  jm2.25lem1  40800  limcleqr  43139  icccncfext  43382  fourierdlem87  43688  sge0seq  43938  smflimsuplem7  44310  itscnhlc0xyqsol  46063  itscnhlinecirc02plem2  46081