Theorem simpl1l 1225

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7267  tfisi  7795  funelss  7985  omopth2  8505  swrdsbslen  14574  swrdspsleq  14575  repswswrd  14693  ramub1lem1  16940  cntzsubrng  20484  cntzsubr  20523  lbspss  21018  maducoeval2  22556  cramer  22607  neiptopnei  23048  ptbasin  23493  basqtop  23627  tmdgsum  24011  ustuqtop1  24157  cxplea  26633  cxple2  26634  nosupbnd2lem1  27655  noinfbnd2lem1  27670  sltmul2  28111  ewlkle  29586  uspgr2wlkeq2  29627  clwwlkccat  29972  br8d  32593  isarchi2  33161  archiabllem2c  33171  cvmlift2lem10  35377  5segofs  36071  2llnjaN  39685  lvolnle3at  39701  paddasslem12  39950  paddasslem13  39951  atmod1i1m  39977  lhp2lt  40120  lhpexle2lem  40128  lhpmcvr3  40144  lhpat3  40165  ltrneq2  40267  trlnle  40305  trlval3  40306  trlval4  40307  cdleme0moN  40344  cdleme17b  40406  cdlemefrs29pre00  40514  cdlemefr27cl  40522  cdleme42ke  40604  cdleme42mgN  40607  cdleme46f2g2  40612  cdleme46f2g1  40613  cdleme50eq  40660  cdleme50trn3  40672  trlord  40688  cdlemg6c  40739  cdlemg11b  40761  cdlemg18a  40797  cdlemg42  40848  cdlemg46  40854  trljco  40859  tendococl  40891  cdlemj3  40942  tendotr  40949  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk53b  41075  cdlemk53  41076  cdlemk35u  41083  tendoex  41094  cdlemm10N  41237  dihopelvalcpre  41367  dihord6apre  41375  dihord5b  41378  dihglblem5apreN  41410  dihglblem2N  41413  dihmeetlem4preN  41425  dihmeetlem6  41428  dihmeetlem10N  41435  dihmeetlem11N  41436  dihmeetlem16N  41441  dihmeetlem17N  41442  dihmeetlem18N  41443  dihmeetlem19N  41444  dihmeetALTN  41446  dihlspsnat  41452  dvh3dim2  41567  dvh3dim3N  41568  jm2.25lem1  43115  jm2.26  43119  grur1cld  44349  limcperiod  45752  0ellimcdiv  45771  cncfshift  45996  cncfperiod  46001  icccncfext  46009  stoweidlem34  46156  fourierdlem48  46276  fourierdlem87  46315  sge0xaddlem2  46556  smflimsuplem7  46948  domnmsuppn0  48493  itscnhlinecirc02plem2  48908