Theorem simpl1l 1224

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 1185	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  7363  tfisi  7896  funelss  8088  omopth2  8640  swrdsbslen  14712  swrdspsleq  14713  repswswrd  14832  ramub1lem1  17073  cntzsubrng  20593  cntzsubr  20634  lbspss  21104  maducoeval2  22667  cramer  22718  neiptopnei  23161  ptbasin  23606  basqtop  23740  tmdgsum  24124  ustuqtop1  24271  cxplea  26756  cxple2  26757  nosupbnd2lem1  27778  noinfbnd2lem1  27793  sltmul2  28215  ewlkle  29641  uspgr2wlkeq2  29683  clwwlkccat  30022  br8d  32632  isarchi2  33165  archiabllem2c  33175  cvmlift2lem10  35280  5segofs  35970  2llnjaN  39523  lvolnle3at  39539  paddasslem12  39788  paddasslem13  39789  atmod1i1m  39815  lhp2lt  39958  lhpexle2lem  39966  lhpmcvr3  39982  lhpat3  40003  ltrneq2  40105  trlnle  40143  trlval3  40144  trlval4  40145  cdleme0moN  40182  cdleme17b  40244  cdlemefrs29pre00  40352  cdlemefr27cl  40360  cdleme42ke  40442  cdleme42mgN  40445  cdleme46f2g2  40450  cdleme46f2g1  40451  cdleme50eq  40498  cdleme50trn3  40510  trlord  40526  cdlemg6c  40577  cdlemg11b  40599  cdlemg18a  40635  cdlemg42  40686  cdlemg46  40692  trljco  40697  tendococl  40729  cdlemj3  40780  tendotr  40787  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53b  40913  cdlemk53  40914  cdlemk35u  40921  tendoex  40932  cdlemm10N  41075  dihopelvalcpre  41205  dihord6apre  41213  dihord5b  41216  dihglblem5apreN  41248  dihglblem2N  41251  dihmeetlem4preN  41263  dihmeetlem6  41266  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem18N  41281  dihmeetlem19N  41282  dihmeetALTN  41284  dihlspsnat  41290  dvh3dim2  41405  dvh3dim3N  41406  jm2.25lem1  42955  jm2.26  42959  grur1cld  44201  limcperiod  45549  0ellimcdiv  45570  cncfshift  45795  cncfperiod  45800  icccncfext  45808  stoweidlem34  45955  fourierdlem48  46075  fourierdlem87  46114  sge0xaddlem2  46355  smflimsuplem7  46747  domnmsuppn0  48094  itscnhlinecirc02plem2  48517