Theorem simpl1r 1244

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7358  tfisi  7894  omopth2  8620  swrdsbslen  14842  swrdspsleq  14843  repswswrd  14963  ramub1lem1  17233  efgsfo  19983  lbspss  21387  maducoeval2  22985  madurid  22989  decpmatmullem  23119  mp2pm2mplem4  23157  llyrest  23834  ptbasin  23926  basqtop  24060  ustuqtop1  24590  mulcxp  27043  noetalem1  28128  ltmuls2  28587  elwwlks2ons3im  30573  br8d  33274  isarchi2  33816  archiabllem2c  33826  cvmlift2lem10  36244  5segofs  36949  btwnconn1lem13  37042  2llnjaN  40815  paddasslem12  41080  lhp2lt  41250  lhpexle2lem  41258  lhpmcvr3  41274  lhpat3  41295  trlval3  41436  cdleme17b  41536  cdlemefr27cl  41652  cdlemg11b  41891  tendococl  42021  cdlemj3  42072  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk53b  42205  cdlemk35u  42213  cdlemm10N  42367  dihopelvalcpre  42497  dihord6apre  42505  dihord5b  42508  dihglblem5apreN  42540  dihglblem2N  42543  dihmeetlem6  42558  dihmeetlem18N  42573  dvh3dim2  42697  dvh3dim3N  42698  jm2.25lem1  44198  limcleqr  46859  icccncfext  47102  fourierdlem87  47408  sge0seq  47661  smflimsuplem7  48041  fsupdm  48057  finfdm  48061  itscnhlc0xyqsol  50082  itscnhlinecirc02plem2  50100