Theorem simpl1r 1224

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 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl1 1184	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  7346  tfisi  7879  omopth2  8620  swrdsbslen  14698  swrdspsleq  14699  repswswrd  14818  ramub1lem1  17059  efgsfo  19771  lbspss  21098  maducoeval2  22661  madurid  22665  decpmatmullem  22792  mp2pm2mplem4  22830  llyrest  23508  ptbasin  23600  basqtop  23734  ustuqtop1  24265  mulcxp  26741  noetalem1  27800  sltmul2  28211  elwwlks2ons3im  29983  br8d  32629  isarchi2  33174  archiabllem2c  33184  cvmlift2lem10  35296  5segofs  35987  btwnconn1lem13  36080  2llnjaN  39548  paddasslem12  39813  lhp2lt  39983  lhpexle2lem  39991  lhpmcvr3  40007  lhpat3  40028  trlval3  40169  cdleme17b  40269  cdlemefr27cl  40385  cdlemg11b  40624  tendococl  40754  cdlemj3  40805  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53b  40938  cdlemk35u  40946  cdlemm10N  41100  dihopelvalcpre  41230  dihord6apre  41238  dihord5b  41241  dihglblem5apreN  41273  dihglblem2N  41276  dihmeetlem6  41291  dihmeetlem18N  41306  dvh3dim2  41430  dvh3dim3N  41431  jm2.25lem1  42986  limcleqr  45599  icccncfext  45842  fourierdlem87  46148  sge0seq  46401  smflimsuplem7  46781  fsupdm  46797  finfdm  46801  itscnhlc0xyqsol  48614  itscnhlinecirc02plem2  48632