Theorem simpl1l 1226

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 767	. 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  7275  tfisi  7803  funelss  7993  omopth2  8512  swrdsbslen  14618  swrdspsleq  14619  repswswrd  14737  ramub1lem1  16988  cntzsubrng  20535  cntzsubr  20574  lbspss  21069  maducoeval2  22615  cramer  22666  neiptopnei  23107  ptbasin  23552  basqtop  23686  tmdgsum  24070  ustuqtop1  24216  cxplea  26673  cxple2  26674  nosupbnd2lem1  27693  noinfbnd2lem1  27708  ltmuls2  28177  ewlkle  29689  uspgr2wlkeq2  29730  clwwlkccat  30075  br8d  32696  isarchi2  33261  archiabllem2c  33271  cvmlift2lem10  35510  5segofs  36204  2llnjaN  40026  lvolnle3at  40042  paddasslem12  40291  paddasslem13  40292  atmod1i1m  40318  lhp2lt  40461  lhpexle2lem  40469  lhpmcvr3  40485  lhpat3  40506  ltrneq2  40608  trlnle  40646  trlval3  40647  trlval4  40648  cdleme0moN  40685  cdleme17b  40747  cdlemefrs29pre00  40855  cdlemefr27cl  40863  cdleme42ke  40945  cdleme42mgN  40948  cdleme46f2g2  40953  cdleme46f2g1  40954  cdleme50eq  41001  cdleme50trn3  41013  trlord  41029  cdlemg6c  41080  cdlemg11b  41102  cdlemg18a  41138  cdlemg42  41189  cdlemg46  41195  trljco  41200  tendococl  41232  cdlemj3  41283  tendotr  41290  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk53b  41416  cdlemk53  41417  cdlemk35u  41424  tendoex  41435  cdlemm10N  41578  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihglblem5apreN  41751  dihglblem2N  41754  dihmeetlem4preN  41766  dihmeetlem6  41769  dihmeetlem10N  41776  dihmeetlem11N  41777  dihmeetlem16N  41782  dihmeetlem17N  41783  dihmeetlem18N  41784  dihmeetlem19N  41785  dihmeetALTN  41787  dihlspsnat  41793  dvh3dim2  41908  dvh3dim3N  41909  jm2.25lem1  43444  jm2.26  43448  grur1cld  44677  limcperiod  46076  0ellimcdiv  46095  cncfshift  46320  cncfperiod  46325  icccncfext  46333  stoweidlem34  46480  fourierdlem48  46600  fourierdlem87  46639  sge0xaddlem2  46880  smflimsuplem7  47272  domnmsuppn0  48857  itscnhlinecirc02plem2  49271