Theorem simpl1r 1225

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

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

This theorem is referenced by:  soisores  7230  tfisi  7737  omopth2  8446  swrdsbslen  14422  swrdspsleq  14423  repswswrd  14542  ramub1lem1  16772  efgsfo  19390  lbspss  20389  maducoeval2  21834  madurid  21838  decpmatmullem  21965  mp2pm2mplem4  22003  llyrest  22681  ptbasin  22773  basqtop  22907  ustuqtop1  23438  mulcxp  25885  elwwlks2ons3im  28364  br8d  30995  isarchi2  31484  archiabllem2c  31494  cvmlift2lem10  33319  noetalem1  33989  5segofs  34353  btwnconn1lem13  34446  2llnjaN  37622  paddasslem12  37887  lhp2lt  38057  lhpexle2lem  38065  lhpmcvr3  38081  lhpat3  38102  trlval3  38243  cdleme17b  38343  cdlemefr27cl  38459  cdlemg11b  38698  tendococl  38828  cdlemj3  38879  cdlemk35s-id  38994  cdlemk39s-id  38996  cdlemk53b  39012  cdlemk35u  39020  cdlemm10N  39174  dihopelvalcpre  39304  dihord6apre  39312  dihord5b  39315  dihglblem5apreN  39347  dihglblem2N  39350  dihmeetlem6  39365  dihmeetlem18N  39380  dvh3dim2  39504  dvh3dim3N  39505  jm2.25lem1  40858  limcleqr  43234  icccncfext  43477  fourierdlem87  43783  sge0seq  44034  smflimsuplem7  44413  itscnhlc0xyqsol  46169  itscnhlinecirc02plem2  46187