Theorem simpl1r 1252

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  soisores  6851  tfisi  7338  omopth2  7950  swrdsbslen  13774  swrdspsleq  13775  repswswrd  13936  ramub1lem1  16145  efgsfo  18548  lbspss  19488  maducoeval2  20862  madurid  20866  decpmatmullem  20994  mp2pm2mplem4  21032  llyrest  21708  ptbasin  21800  basqtop  21934  ustuqtop1  22464  mulcxp  24879  elwwlks2ons3im  27351  br8d  30002  isarchi2  30309  archiabllem2c  30319  cvmlift2lem10  31901  5segofs  32710  btwnconn1lem13  32803  2llnjaN  35729  paddasslem12  35994  lhp2lt  36164  lhpexle2lem  36172  lhpmcvr3  36188  lhpat3  36209  trlval3  36350  cdleme17b  36450  cdlemefr27cl  36566  cdlemg11b  36805  tendococl  36935  cdlemj3  36986  cdlemk35s-id  37101  cdlemk39s-id  37103  cdlemk53b  37119  cdlemk35u  37127  cdlemm10N  37281  dihopelvalcpre  37411  dihord6apre  37419  dihord5b  37422  dihglblem5apreN  37454  dihglblem2N  37457  dihmeetlem6  37472  dihmeetlem18N  37487  dvh3dim2  37611  dvh3dim3N  37612  jm2.25lem1  38538  limcleqr  40798  icccncfext  41042  fourierdlem87  41351  sge0seq  41601  smflimsuplem7  41973  itscnhlc0xyqsol  43515  itscnhlinecirc02plem2  43533