Theorem simpl1r 1238

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  soisores  7307  tfisi  7835  omopth2  8548  swrdsbslen  14675  swrdspsleq  14676  repswswrd  14794  ramub1lem1  17045  efgsfo  19762  lbspss  21129  maducoeval2  22680  madurid  22684  decpmatmullem  22811  mp2pm2mplem4  22849  llyrest  23525  ptbasin  23617  basqtop  23751  ustuqtop1  24281  mulcxp  26727  noetalem1  27782  ltmuls2  28241  elwwlks2ons3im  30100  br8d  32760  isarchi2  33326  archiabllem2c  33336  cvmlift2lem10  35626  5segofs  36320  btwnconn1lem13  36413  2llnjaN  40154  paddasslem12  40419  lhp2lt  40589  lhpexle2lem  40597  lhpmcvr3  40613  lhpat3  40634  trlval3  40775  cdleme17b  40875  cdlemefr27cl  40991  cdlemg11b  41230  tendococl  41360  cdlemj3  41411  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk53b  41544  cdlemk35u  41552  cdlemm10N  41706  dihopelvalcpre  41836  dihord6apre  41844  dihord5b  41847  dihglblem5apreN  41879  dihglblem2N  41882  dihmeetlem6  41897  dihmeetlem18N  41912  dvh3dim2  42036  dvh3dim3N  42037  jm2.25lem1  43539  limcleqr  46182  icccncfext  46425  fourierdlem87  46731  sge0seq  46984  smflimsuplem7  47364  fsupdm  47380  finfdm  47384  itscnhlc0xyqsol  49351  itscnhlinecirc02plem2  49369