Theorem simpl1r 1221

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 1181	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7083  tfisi  7576  omopth2  8213  swrdsbslen  14029  swrdspsleq  14030  repswswrd  14149  ramub1lem1  16365  efgsfo  18868  lbspss  19857  maducoeval2  21252  madurid  21256  decpmatmullem  21382  mp2pm2mplem4  21420  llyrest  22096  ptbasin  22188  basqtop  22322  ustuqtop1  22853  mulcxp  25271  elwwlks2ons3im  27736  br8d  30364  isarchi2  30818  archiabllem2c  30828  cvmlift2lem10  32563  5segofs  33471  btwnconn1lem13  33564  2llnjaN  36706  paddasslem12  36971  lhp2lt  37141  lhpexle2lem  37149  lhpmcvr3  37165  lhpat3  37186  trlval3  37327  cdleme17b  37427  cdlemefr27cl  37543  cdlemg11b  37782  tendococl  37912  cdlemj3  37963  cdlemk35s-id  38078  cdlemk39s-id  38080  cdlemk53b  38096  cdlemk35u  38104  cdlemm10N  38258  dihopelvalcpre  38388  dihord6apre  38396  dihord5b  38399  dihglblem5apreN  38431  dihglblem2N  38434  dihmeetlem6  38449  dihmeetlem18N  38464  dvh3dim2  38588  dvh3dim3N  38589  jm2.25lem1  39601  limcleqr  41931  icccncfext  42176  fourierdlem87  42485  sge0seq  42735  smflimsuplem7  43107  itscnhlc0xyqsol  44759  itscnhlinecirc02plem2  44777