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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ 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 401  df-3an 1105

This theorem is used by:  soisores  7325  tfisi  7851  omopth2  8565  swrdsbslen  14707  swrdspsleq  14708  repswswrd  14826  ramub1lem1  17090  efgsfo  19813  lbspss  21212  maducoeval2  22806  madurid  22810  decpmatmullem  22937  mp2pm2mplem4  22975  llyrest  23651  ptbasin  23743  basqtop  23877  ustuqtop1  24407  mulcxp  26859  noetalem1  27914  ltmuls2  28373  elwwlks2ons3im  30312  br8d  32962  isarchi2  33514  archiabllem2c  33524  cvmlift2lem10  35812  5segofs  36506  btwnconn1lem13  36599  2llnjaN  40368  paddasslem12  40633  lhp2lt  40803  lhpexle2lem  40811  lhpmcvr3  40827  lhpat3  40848  trlval3  40989  cdleme17b  41089  cdlemefr27cl  41205  cdlemg11b  41444  tendococl  41574  cdlemj3  41625  cdlemk35s-id  41740  cdlemk39s-id  41742  cdlemk53b  41758  cdlemk35u  41766  cdlemm10N  41920  dihopelvalcpre  42050  dihord6apre  42058  dihord5b  42061  dihglblem5apreN  42093  dihglblem2N  42096  dihmeetlem6  42111  dihmeetlem18N  42126  dvh3dim2  42250  dvh3dim3N  42251  jm2.25lem1  43753  limcleqr  46386  icccncfext  46629  fourierdlem87  46935  sge0seq  47188  smflimsuplem7  47568  fsupdm  47584  finfdm  47588  itscnhlc0xyqsol  49573  itscnhlinecirc02plem2  49591