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  7305  tfisi  7838  omopth2  8551  swrdsbslen  14636  swrdspsleq  14637  repswswrd  14756  ramub1lem1  17004  efgsfo  19676  lbspss  20996  maducoeval2  22534  madurid  22538  decpmatmullem  22665  mp2pm2mplem4  22703  llyrest  23379  ptbasin  23471  basqtop  23605  ustuqtop1  24136  mulcxp  26601  noetalem1  27660  sltmul2  28081  elwwlks2ons3im  29891  br8d  32545  isarchi2  33146  archiabllem2c  33156  cvmlift2lem10  35306  5segofs  36001  btwnconn1lem13  36094  2llnjaN  39567  paddasslem12  39832  lhp2lt  40002  lhpexle2lem  40010  lhpmcvr3  40026  lhpat3  40047  trlval3  40188  cdleme17b  40288  cdlemefr27cl  40404  cdlemg11b  40643  tendococl  40773  cdlemj3  40824  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53b  40957  cdlemk35u  40965  cdlemm10N  41119  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihglblem5apreN  41292  dihglblem2N  41295  dihmeetlem6  41310  dihmeetlem18N  41325  dvh3dim2  41449  dvh3dim3N  41450  jm2.25lem1  42994  limcleqr  45649  icccncfext  45892  fourierdlem87  46198  sge0seq  46451  smflimsuplem7  46831  fsupdm  46847  finfdm  46851  itscnhlc0xyqsol  48758  itscnhlinecirc02plem2  48776