Theorem simpl1r 1227

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soisores  7282  tfisi  7810  omopth2  8519  swrdsbslen  14627  swrdspsleq  14628  repswswrd  14746  ramub1lem1  16997  efgsfo  19714  lbspss  21077  maducoeval2  22605  madurid  22609  decpmatmullem  22736  mp2pm2mplem4  22774  llyrest  23450  ptbasin  23542  basqtop  23676  ustuqtop1  24206  mulcxp  26649  noetalem1  27705  ltmuls2  28163  elwwlks2ons3im  30022  br8d  32681  isarchi2  33246  archiabllem2c  33256  cvmlift2lem10  35494  5segofs  36188  btwnconn1lem13  36281  2llnjaN  40012  paddasslem12  40277  lhp2lt  40447  lhpexle2lem  40455  lhpmcvr3  40471  lhpat3  40492  trlval3  40633  cdleme17b  40733  cdlemefr27cl  40849  cdlemg11b  41088  tendococl  41218  cdlemj3  41269  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53b  41402  cdlemk35u  41410  cdlemm10N  41564  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihglblem5apreN  41737  dihglblem2N  41740  dihmeetlem6  41755  dihmeetlem18N  41770  dvh3dim2  41894  dvh3dim3N  41895  jm2.25lem1  43426  limcleqr  46072  icccncfext  46315  fourierdlem87  46621  sge0seq  46874  smflimsuplem7  47254  fsupdm  47270  finfdm  47274  itscnhlc0xyqsol  49241  itscnhlinecirc02plem2  49259