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 768	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl1 1185	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  7363  tfisi  7896  omopth2  8640  swrdsbslen  14712  swrdspsleq  14713  repswswrd  14832  ramub1lem1  17073  efgsfo  19781  lbspss  21104  maducoeval2  22667  madurid  22671  decpmatmullem  22798  mp2pm2mplem4  22836  llyrest  23514  ptbasin  23606  basqtop  23740  ustuqtop1  24271  mulcxp  26745  noetalem1  27804  sltmul2  28215  elwwlks2ons3im  29987  br8d  32632  isarchi2  33165  archiabllem2c  33175  cvmlift2lem10  35280  5segofs  35970  btwnconn1lem13  36063  2llnjaN  39523  paddasslem12  39788  lhp2lt  39958  lhpexle2lem  39966  lhpmcvr3  39982  lhpat3  40003  trlval3  40144  cdleme17b  40244  cdlemefr27cl  40360  cdlemg11b  40599  tendococl  40729  cdlemj3  40780  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53b  40913  cdlemk35u  40921  cdlemm10N  41075  dihopelvalcpre  41205  dihord6apre  41213  dihord5b  41216  dihglblem5apreN  41248  dihglblem2N  41251  dihmeetlem6  41266  dihmeetlem18N  41281  dvh3dim2  41405  dvh3dim3N  41406  jm2.25lem1  42955  limcleqr  45565  icccncfext  45808  fourierdlem87  46114  sge0seq  46367  smflimsuplem7  46747  fsupdm  46763  finfdm  46767  itscnhlc0xyqsol  48499  itscnhlinecirc02plem2  48517