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  7332  tfisi  7859  omopth2  8575  swrdsbslen  14738  swrdspsleq  14739  repswswrd  14859  ramub1lem1  17124  efgsfo  19872  lbspss  21272  maducoeval2  22868  madurid  22872  decpmatmullem  23002  mp2pm2mplem4  23040  llyrest  23717  ptbasin  23809  basqtop  23943  ustuqtop1  24473  mulcxp  26930  noetalem1  27985  ltmuls2  28444  elwwlks2ons3im  30430  br8d  33089  isarchi2  33633  archiabllem2c  33643  cvmlift2lem10  35899  5segofs  36594  btwnconn1lem13  36687  2llnjaN  40447  paddasslem12  40712  lhp2lt  40882  lhpexle2lem  40890  lhpmcvr3  40906  lhpat3  40927  trlval3  41068  cdleme17b  41168  cdlemefr27cl  41284  cdlemg11b  41523  tendococl  41653  cdlemj3  41704  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53b  41837  cdlemk35u  41845  cdlemm10N  41999  dihopelvalcpre  42129  dihord6apre  42137  dihord5b  42140  dihglblem5apreN  42172  dihglblem2N  42175  dihmeetlem6  42190  dihmeetlem18N  42205  dvh3dim2  42329  dvh3dim3N  42330  jm2.25lem1  43847  limcleqr  46480  icccncfext  46723  fourierdlem87  47029  sge0seq  47282  smflimsuplem7  47662  fsupdm  47678  finfdm  47682  itscnhlc0xyqsol  49703  itscnhlinecirc02plem2  49721