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  7256  tfisi  7784  omopth2  8494  swrdsbslen  14564  swrdspsleq  14565  repswswrd  14683  ramub1lem1  16930  efgsfo  19644  lbspss  21009  maducoeval2  22548  madurid  22552  decpmatmullem  22679  mp2pm2mplem4  22717  llyrest  23393  ptbasin  23485  basqtop  23619  ustuqtop1  24149  mulcxp  26614  noetalem1  27673  sltmul2  28103  elwwlks2ons3im  29925  br8d  32581  isarchi2  33144  archiabllem2c  33154  cvmlift2lem10  35324  5segofs  36019  btwnconn1lem13  36112  2llnjaN  39584  paddasslem12  39849  lhp2lt  40019  lhpexle2lem  40027  lhpmcvr3  40043  lhpat3  40064  trlval3  40205  cdleme17b  40305  cdlemefr27cl  40421  cdlemg11b  40660  tendococl  40790  cdlemj3  40841  cdlemk35s-id  40956  cdlemk39s-id  40958  cdlemk53b  40974  cdlemk35u  40982  cdlemm10N  41136  dihopelvalcpre  41266  dihord6apre  41274  dihord5b  41277  dihglblem5apreN  41309  dihglblem2N  41312  dihmeetlem6  41327  dihmeetlem18N  41342  dvh3dim2  41466  dvh3dim3N  41467  jm2.25lem1  43010  limcleqr  45661  icccncfext  45904  fourierdlem87  46210  sge0seq  46463  smflimsuplem7  46843  fsupdm  46859  finfdm  46863  itscnhlc0xyqsol  48776  itscnhlinecirc02plem2  48794