Theorem simpl1r 1232

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soisores  7278  tfisi  7806  omopth2  8516  swrdsbslen  14625  swrdspsleq  14626  repswswrd  14744  ramub1lem1  16995  efgsfo  19712  lbspss  21079  maducoeval2  22630  madurid  22634  decpmatmullem  22761  mp2pm2mplem4  22799  llyrest  23475  ptbasin  23567  basqtop  23701  ustuqtop1  24231  mulcxp  26674  noetalem1  27730  ltmuls2  28188  elwwlks2ons3im  30047  br8d  32707  isarchi2  33273  archiabllem2c  33283  cvmlift2lem10  35547  5segofs  36241  btwnconn1lem13  36334  2llnjaN  40065  paddasslem12  40330  lhp2lt  40500  lhpexle2lem  40508  lhpmcvr3  40524  lhpat3  40545  trlval3  40686  cdleme17b  40786  cdlemefr27cl  40902  cdlemg11b  41141  tendococl  41271  cdlemj3  41322  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk53b  41455  cdlemk35u  41463  cdlemm10N  41617  dihopelvalcpre  41747  dihord6apre  41755  dihord5b  41758  dihglblem5apreN  41790  dihglblem2N  41793  dihmeetlem6  41808  dihmeetlem18N  41823  dvh3dim2  41947  dvh3dim3N  41948  jm2.25lem1  43450  limcleqr  46094  icccncfext  46337  fourierdlem87  46643  sge0seq  46896  smflimsuplem7  47276  fsupdm  47292  finfdm  47296  itscnhlc0xyqsol  49263  itscnhlinecirc02plem2  49281