Theorem simpl1r 1225

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

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

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  soisores  7320  tfisi  7844  omopth2  8580  swrdsbslen  14610  swrdspsleq  14611  repswswrd  14730  ramub1lem1  16955  efgsfo  19601  lbspss  20685  maducoeval2  22133  madurid  22137  decpmatmullem  22264  mp2pm2mplem4  22302  llyrest  22980  ptbasin  23072  basqtop  23206  ustuqtop1  23737  mulcxp  26184  noetalem1  27233  sltmul2  27612  elwwlks2ons3im  29197  br8d  31826  isarchi2  32318  archiabllem2c  32328  cvmlift2lem10  34291  5segofs  34966  btwnconn1lem13  35059  2llnjaN  38425  paddasslem12  38690  lhp2lt  38860  lhpexle2lem  38868  lhpmcvr3  38884  lhpat3  38905  trlval3  39046  cdleme17b  39146  cdlemefr27cl  39262  cdlemg11b  39501  tendococl  39631  cdlemj3  39682  cdlemk35s-id  39797  cdlemk39s-id  39799  cdlemk53b  39815  cdlemk35u  39823  cdlemm10N  39977  dihopelvalcpre  40107  dihord6apre  40115  dihord5b  40118  dihglblem5apreN  40150  dihglblem2N  40153  dihmeetlem6  40168  dihmeetlem18N  40183  dvh3dim2  40307  dvh3dim3N  40308  jm2.25lem1  41722  limcleqr  44346  icccncfext  44589  fourierdlem87  44895  sge0seq  45148  smflimsuplem7  45528  fsupdm  45544  finfdm  45548  itscnhlc0xyqsol  47404  itscnhlinecirc02plem2  47422