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  7320  tfisi  7854  omopth2  8596  swrdsbslen  14682  swrdspsleq  14683  repswswrd  14802  ramub1lem1  17046  efgsfo  19720  lbspss  21040  maducoeval2  22578  madurid  22582  decpmatmullem  22709  mp2pm2mplem4  22747  llyrest  23423  ptbasin  23515  basqtop  23649  ustuqtop1  24180  mulcxp  26646  noetalem1  27705  sltmul2  28126  elwwlks2ons3im  29936  br8d  32590  isarchi2  33183  archiabllem2c  33193  cvmlift2lem10  35334  5segofs  36024  btwnconn1lem13  36117  2llnjaN  39585  paddasslem12  39850  lhp2lt  40020  lhpexle2lem  40028  lhpmcvr3  40044  lhpat3  40065  trlval3  40206  cdleme17b  40306  cdlemefr27cl  40422  cdlemg11b  40661  tendococl  40791  cdlemj3  40842  cdlemk35s-id  40957  cdlemk39s-id  40959  cdlemk53b  40975  cdlemk35u  40983  cdlemm10N  41137  dihopelvalcpre  41267  dihord6apre  41275  dihord5b  41278  dihglblem5apreN  41310  dihglblem2N  41313  dihmeetlem6  41328  dihmeetlem18N  41343  dvh3dim2  41467  dvh3dim3N  41468  jm2.25lem1  43022  limcleqr  45673  icccncfext  45916  fourierdlem87  46222  sge0seq  46475  smflimsuplem7  46855  fsupdm  46871  finfdm  46875  itscnhlc0xyqsol  48745  itscnhlinecirc02plem2  48763