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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  soisores  7254  tfisi  7773  omopth2  8486  swrdsbslen  14475  swrdspsleq  14476  repswswrd  14595  ramub1lem1  16824  efgsfo  19440  lbspss  20450  maducoeval2  21895  madurid  21899  decpmatmullem  22026  mp2pm2mplem4  22064  llyrest  22742  ptbasin  22834  basqtop  22968  ustuqtop1  23499  mulcxp  25946  noetalem1  26995  elwwlks2ons3im  28607  br8d  31237  isarchi2  31726  archiabllem2c  31736  cvmlift2lem10  33573  5segofs  34404  btwnconn1lem13  34497  2llnjaN  37842  paddasslem12  38107  lhp2lt  38277  lhpexle2lem  38285  lhpmcvr3  38301  lhpat3  38322  trlval3  38463  cdleme17b  38563  cdlemefr27cl  38679  cdlemg11b  38918  tendococl  39048  cdlemj3  39099  cdlemk35s-id  39214  cdlemk39s-id  39216  cdlemk53b  39232  cdlemk35u  39240  cdlemm10N  39394  dihopelvalcpre  39524  dihord6apre  39532  dihord5b  39535  dihglblem5apreN  39567  dihglblem2N  39570  dihmeetlem6  39585  dihmeetlem18N  39600  dvh3dim2  39724  dvh3dim3N  39725  jm2.25lem1  41091  limcleqr  43530  icccncfext  43773  fourierdlem87  44079  sge0seq  44330  smflimsuplem7  44710  itscnhlc0xyqsol  46471  itscnhlinecirc02plem2  46489