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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soisores  7327  tfisi  7856  omopth2  8570  swrdsbslen  14704  swrdspsleq  14705  repswswrd  14823  ramub1lem1  17087  efgsfo  19810  lbspss  21184  maducoeval2  22778  madurid  22782  decpmatmullem  22909  mp2pm2mplem4  22947  llyrest  23623  ptbasin  23715  basqtop  23849  ustuqtop1  24379  mulcxp  26828  noetalem1  27883  ltmuls2  28342  elwwlks2ons3im  30281  br8d  32931  isarchi2  33483  archiabllem2c  33493  cvmlift2lem10  35782  5segofs  36476  btwnconn1lem13  36569  2llnjaN  40318  paddasslem12  40583  lhp2lt  40753  lhpexle2lem  40761  lhpmcvr3  40777  lhpat3  40798  trlval3  40939  cdleme17b  41039  cdlemefr27cl  41155  cdlemg11b  41394  tendococl  41524  cdlemj3  41575  cdlemk35s-id  41690  cdlemk39s-id  41692  cdlemk53b  41708  cdlemk35u  41716  cdlemm10N  41870  dihopelvalcpre  42000  dihord6apre  42008  dihord5b  42011  dihglblem5apreN  42043  dihglblem2N  42046  dihmeetlem6  42061  dihmeetlem18N  42076  dvh3dim2  42200  dvh3dim3N  42201  jm2.25lem1  43705  limcleqr  46338  icccncfext  46581  fourierdlem87  46887  sge0seq  47140  smflimsuplem7  47520  fsupdm  47536  finfdm  47540  itscnhlc0xyqsol  49522  itscnhlinecirc02plem2  49540