Theorem simpl1r 1227

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 1187	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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 1089

This theorem is referenced by:  soisores  7275  tfisi  7803  omopth2  8512  swrdsbslen  14618  swrdspsleq  14619  repswswrd  14737  ramub1lem1  16988  efgsfo  19705  lbspss  21069  maducoeval2  22615  madurid  22619  decpmatmullem  22746  mp2pm2mplem4  22784  llyrest  23460  ptbasin  23552  basqtop  23686  ustuqtop1  24216  mulcxp  26662  noetalem1  27719  ltmuls2  28177  elwwlks2ons3im  30037  br8d  32696  isarchi2  33261  archiabllem2c  33271  cvmlift2lem10  35510  5segofs  36204  btwnconn1lem13  36297  2llnjaN  40026  paddasslem12  40291  lhp2lt  40461  lhpexle2lem  40469  lhpmcvr3  40485  lhpat3  40506  trlval3  40647  cdleme17b  40747  cdlemefr27cl  40863  cdlemg11b  41102  tendococl  41232  cdlemj3  41283  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk53b  41416  cdlemk35u  41424  cdlemm10N  41578  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihglblem5apreN  41751  dihglblem2N  41754  dihmeetlem6  41769  dihmeetlem18N  41784  dvh3dim2  41908  dvh3dim3N  41909  jm2.25lem1  43444  limcleqr  46090  icccncfext  46333  fourierdlem87  46639  sge0seq  46892  smflimsuplem7  47272  fsupdm  47288  finfdm  47292  itscnhlc0xyqsol  49253  itscnhlinecirc02plem2  49271