Theorem simpl1r 1244

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7327  tfisi  7859  omopth2  8576  swrdsbslen  14794  swrdspsleq  14795  repswswrd  14915  ramub1lem1  17184  efgsfo  19933  lbspss  21337  maducoeval2  22935  madurid  22939  decpmatmullem  23069  mp2pm2mplem4  23107  llyrest  23784  ptbasin  23876  basqtop  24010  ustuqtop1  24540  mulcxp  26995  noetalem1  28080  ltmuls2  28539  elwwlks2ons3im  30525  br8d  33184  isarchi2  33728  archiabllem2c  33738  cvmlift2lem10  36046  5segofs  36741  btwnconn1lem13  36834  2llnjaN  40591  paddasslem12  40856  lhp2lt  41026  lhpexle2lem  41034  lhpmcvr3  41050  lhpat3  41071  trlval3  41212  cdleme17b  41312  cdlemefr27cl  41428  cdlemg11b  41667  tendococl  41797  cdlemj3  41848  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk53b  41981  cdlemk35u  41989  cdlemm10N  42143  dihopelvalcpre  42273  dihord6apre  42281  dihord5b  42284  dihglblem5apreN  42316  dihglblem2N  42319  dihmeetlem6  42334  dihmeetlem18N  42349  dvh3dim2  42473  dvh3dim3N  42474  jm2.25lem1  43958  limcleqr  46598  icccncfext  46841  fourierdlem87  47147  sge0seq  47400  smflimsuplem7  47780  fsupdm  47796  finfdm  47800  itscnhlc0xyqsol  49821  itscnhlinecirc02plem2  49839