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  7283  tfisi  7811  omopth2  8521  swrdsbslen  14600  swrdspsleq  14601  repswswrd  14719  ramub1lem1  16966  efgsfo  19680  lbspss  21046  maducoeval2  22596  madurid  22600  decpmatmullem  22727  mp2pm2mplem4  22765  llyrest  23441  ptbasin  23533  basqtop  23667  ustuqtop1  24197  mulcxp  26662  noetalem1  27721  ltmuls2  28179  elwwlks2ons3im  30039  br8d  32697  isarchi2  33278  archiabllem2c  33288  cvmlift2lem10  35525  5segofs  36219  btwnconn1lem13  36312  2llnjaN  39936  paddasslem12  40201  lhp2lt  40371  lhpexle2lem  40379  lhpmcvr3  40395  lhpat3  40416  trlval3  40557  cdleme17b  40657  cdlemefr27cl  40773  cdlemg11b  41012  tendococl  41142  cdlemj3  41193  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk53b  41326  cdlemk35u  41334  cdlemm10N  41488  dihopelvalcpre  41618  dihord6apre  41626  dihord5b  41629  dihglblem5apreN  41661  dihglblem2N  41664  dihmeetlem6  41679  dihmeetlem18N  41694  dvh3dim2  41818  dvh3dim3N  41819  jm2.25lem1  43349  limcleqr  45996  icccncfext  46239  fourierdlem87  46545  sge0seq  46798  smflimsuplem7  47178  fsupdm  47194  finfdm  47198  itscnhlc0xyqsol  49119  itscnhlinecirc02plem2  49137