Theorem simpl1r 1226

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 1186	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  7347  tfisi  7880  omopth2  8622  swrdsbslen  14702  swrdspsleq  14703  repswswrd  14822  ramub1lem1  17064  efgsfo  19757  lbspss  21081  maducoeval2  22646  madurid  22650  decpmatmullem  22777  mp2pm2mplem4  22815  llyrest  23493  ptbasin  23585  basqtop  23719  ustuqtop1  24250  mulcxp  26727  noetalem1  27786  sltmul2  28197  elwwlks2ons3im  29974  br8d  32622  isarchi2  33192  archiabllem2c  33202  cvmlift2lem10  35317  5segofs  36007  btwnconn1lem13  36100  2llnjaN  39568  paddasslem12  39833  lhp2lt  40003  lhpexle2lem  40011  lhpmcvr3  40027  lhpat3  40048  trlval3  40189  cdleme17b  40289  cdlemefr27cl  40405  cdlemg11b  40644  tendococl  40774  cdlemj3  40825  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53b  40958  cdlemk35u  40966  cdlemm10N  41120  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihglblem5apreN  41293  dihglblem2N  41296  dihmeetlem6  41311  dihmeetlem18N  41326  dvh3dim2  41450  dvh3dim3N  41451  jm2.25lem1  43010  limcleqr  45659  icccncfext  45902  fourierdlem87  46208  sge0seq  46461  smflimsuplem7  46841  fsupdm  46857  finfdm  46861  itscnhlc0xyqsol  48686  itscnhlinecirc02plem2  48704