Theorem simpl1l 1223

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl1l	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l

Step	Hyp	Ref	Expression
1		simpll 764	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1184	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  soisores  7198  tfisi  7705  funelss  7888  omopth2  8415  swrdsbslen  14377  swrdspsleq  14378  repswswrd  14497  ramub1lem1  16727  cntzsubr  20057  lbspss  20344  maducoeval2  21789  cramer  21840  neiptopnei  22283  ptbasin  22728  basqtop  22862  tmdgsum  23246  ustuqtop1  23393  cxplea  25851  cxple2  25852  ewlkle  27972  uspgr2wlkeq2  28014  clwwlkccat  28354  br8d  30950  isarchi2  31439  archiabllem2c  31449  cvmlift2lem10  33274  nosupbnd2lem1  33918  noinfbnd2lem1  33933  5segofs  34308  2llnjaN  37580  lvolnle3at  37596  paddasslem12  37845  paddasslem13  37846  atmod1i1m  37872  lhp2lt  38015  lhpexle2lem  38023  lhpmcvr3  38039  lhpat3  38060  ltrneq2  38162  trlnle  38200  trlval3  38201  trlval4  38202  cdleme0moN  38239  cdleme17b  38301  cdlemefrs29pre00  38409  cdlemefr27cl  38417  cdleme42ke  38499  cdleme42mgN  38502  cdleme46f2g2  38507  cdleme46f2g1  38508  cdleme50eq  38555  cdleme50trn3  38567  trlord  38583  cdlemg6c  38634  cdlemg11b  38656  cdlemg18a  38692  cdlemg42  38743  cdlemg46  38749  trljco  38754  tendococl  38786  cdlemj3  38837  tendotr  38844  cdlemk35s-id  38952  cdlemk39s-id  38954  cdlemk53b  38970  cdlemk53  38971  cdlemk35u  38978  tendoex  38989  cdlemm10N  39132  dihopelvalcpre  39262  dihord6apre  39270  dihord5b  39273  dihglblem5apreN  39305  dihglblem2N  39308  dihmeetlem4preN  39320  dihmeetlem6  39323  dihmeetlem10N  39330  dihmeetlem11N  39331  dihmeetlem16N  39336  dihmeetlem17N  39337  dihmeetlem18N  39338  dihmeetlem19N  39339  dihmeetALTN  39341  dihlspsnat  39347  dvh3dim2  39462  dvh3dim3N  39463  jm2.25lem1  40820  jm2.26  40824  grur1cld  41850  limcperiod  43169  0ellimcdiv  43190  cncfshift  43415  cncfperiod  43420  icccncfext  43428  stoweidlem34  43575  fourierdlem48  43695  fourierdlem87  43734  sge0xaddlem2  43972  smflimsuplem7  44359  isomgrsym  45288  domnmsuppn0  45705  itscnhlinecirc02plem2  46129