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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  soisores  7268  tfisi  7799  omopth2  8509  swrdsbslen  14589  swrdspsleq  14590  repswswrd  14708  ramub1lem1  16956  efgsfo  19636  lbspss  21004  maducoeval2  22543  madurid  22547  decpmatmullem  22674  mp2pm2mplem4  22712  llyrest  23388  ptbasin  23480  basqtop  23614  ustuqtop1  24145  mulcxp  26610  noetalem1  27669  sltmul2  28097  elwwlks2ons3im  29917  br8d  32571  isarchi2  33137  archiabllem2c  33147  cvmlift2lem10  35284  5segofs  35979  btwnconn1lem13  36072  2llnjaN  39545  paddasslem12  39810  lhp2lt  39980  lhpexle2lem  39988  lhpmcvr3  40004  lhpat3  40025  trlval3  40166  cdleme17b  40266  cdlemefr27cl  40382  cdlemg11b  40621  tendococl  40751  cdlemj3  40802  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53b  40935  cdlemk35u  40943  cdlemm10N  41097  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihglblem5apreN  41270  dihglblem2N  41273  dihmeetlem6  41288  dihmeetlem18N  41303  dvh3dim2  41427  dvh3dim3N  41428  jm2.25lem1  42971  limcleqr  45626  icccncfext  45869  fourierdlem87  46175  sge0seq  46428  smflimsuplem7  46808  fsupdm  46824  finfdm  46828  itscnhlc0xyqsol  48751  itscnhlinecirc02plem2  48769