Theorem simpl1r 1280

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  soisores  6720  tfisi  7205  omopth2  7818  swrdsbslen  13657  swrdspsleq  13658  repswswrd  13740  ramub1lem1  15937  efgsfo  18359  lbspss  19295  maducoeval2  20664  madurid  20668  decpmatmullem  20796  mp2pm2mplem4  20834  llyrest  21509  ptbasin  21601  basqtop  21735  ustuqtop1  22265  mulcxp  24652  elwwlks2ons3im  27101  br8d  29760  isarchi2  30079  archiabllem2c  30089  cvmlift2lem10  31632  5segofs  32450  btwnconn1lem13  32543  2llnjaN  35374  paddasslem12  35639  lhp2lt  35809  lhpexle2lem  35817  lhpmcvr3  35833  lhpat3  35854  trlval3  35996  cdleme17b  36096  cdlemefr27cl  36212  cdlemg11b  36451  tendococl  36581  cdlemj3  36632  cdlemk35s-id  36747  cdlemk39s-id  36749  cdlemk53b  36765  cdlemk35u  36773  cdlemm10N  36928  dihopelvalcpre  37058  dihord6apre  37066  dihord5b  37069  dihglblem5apreN  37101  dihglblem2N  37104  dihmeetlem6  37119  dihmeetlem18N  37134  dvh3dim2  37258  dvh3dim3N  37259  jm2.25lem1  38091  limcleqr  40394  icccncfext  40618  fourierdlem87  40927  sge0seq  41180  smflimsuplem7  41552