Theorem simpl1r 1244

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7336  tfisi  7864  omopth2  8578  swrdsbslen  14726  swrdspsleq  14727  repswswrd  14847  ramub1lem1  17111  efgsfo  19840  lbspss  21240  maducoeval2  22834  madurid  22838  decpmatmullem  22965  mp2pm2mplem4  23003  llyrest  23679  ptbasin  23771  basqtop  23905  ustuqtop1  24435  mulcxp  26887  noetalem1  27942  ltmuls2  28401  elwwlks2ons3im  30340  br8d  32990  isarchi2  33536  archiabllem2c  33546  cvmlift2lem10  35825  5segofs  36519  btwnconn1lem13  36612  2llnjaN  40381  paddasslem12  40646  lhp2lt  40816  lhpexle2lem  40824  lhpmcvr3  40840  lhpat3  40861  trlval3  41002  cdleme17b  41102  cdlemefr27cl  41218  cdlemg11b  41457  tendococl  41587  cdlemj3  41638  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk53b  41771  cdlemk35u  41779  cdlemm10N  41933  dihopelvalcpre  42063  dihord6apre  42071  dihord5b  42074  dihglblem5apreN  42106  dihglblem2N  42109  dihmeetlem6  42124  dihmeetlem18N  42139  dvh3dim2  42263  dvh3dim3N  42264  jm2.25lem1  43766  limcleqr  46399  icccncfext  46642  fourierdlem87  46948  sge0seq  47201  smflimsuplem7  47581  fsupdm  47597  finfdm  47601  itscnhlc0xyqsol  49586  itscnhlinecirc02plem2  49604