Theorem simpl1r 1222

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  soisores  7334  tfisi  7864  omopth2  8605  swrdsbslen  14658  swrdspsleq  14659  repswswrd  14778  ramub1lem1  17014  efgsfo  19723  lbspss  20996  maducoeval2  22603  madurid  22607  decpmatmullem  22734  mp2pm2mplem4  22772  llyrest  23450  ptbasin  23542  basqtop  23676  ustuqtop1  24207  mulcxp  26681  noetalem1  27740  sltmul2  28141  elwwlks2ons3im  29857  br8d  32499  isarchi2  33006  archiabllem2c  33016  cvmlift2lem10  35073  5segofs  35753  btwnconn1lem13  35846  2llnjaN  39189  paddasslem12  39454  lhp2lt  39624  lhpexle2lem  39632  lhpmcvr3  39648  lhpat3  39669  trlval3  39810  cdleme17b  39910  cdlemefr27cl  40026  cdlemg11b  40265  tendococl  40395  cdlemj3  40446  cdlemk35s-id  40561  cdlemk39s-id  40563  cdlemk53b  40579  cdlemk35u  40587  cdlemm10N  40741  dihopelvalcpre  40871  dihord6apre  40879  dihord5b  40882  dihglblem5apreN  40914  dihglblem2N  40917  dihmeetlem6  40932  dihmeetlem18N  40947  dvh3dim2  41071  dvh3dim3N  41072  jm2.25lem1  42566  limcleqr  45175  icccncfext  45418  fourierdlem87  45724  sge0seq  45977  smflimsuplem7  46357  fsupdm  46373  finfdm  46377  itscnhlc0xyqsol  48029  itscnhlinecirc02plem2  48047