Theorem simpl1l 1222

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  soisores  7178  tfisi  7680  funelss  7861  omopth2  8377  swrdsbslen  14305  swrdspsleq  14306  repswswrd  14425  ramub1lem1  16655  cntzsubr  19972  lbspss  20259  maducoeval2  21697  cramer  21748  neiptopnei  22191  ptbasin  22636  basqtop  22770  tmdgsum  23154  ustuqtop1  23301  cxplea  25756  cxple2  25757  ewlkle  27875  uspgr2wlkeq2  27916  clwwlkccat  28255  br8d  30851  isarchi2  31341  archiabllem2c  31351  cvmlift2lem10  33174  nosupbnd2lem1  33845  noinfbnd2lem1  33860  5segofs  34235  2llnjaN  37507  lvolnle3at  37523  paddasslem12  37772  paddasslem13  37773  atmod1i1m  37799  lhp2lt  37942  lhpexle2lem  37950  lhpmcvr3  37966  lhpat3  37987  ltrneq2  38089  trlnle  38127  trlval3  38128  trlval4  38129  cdleme0moN  38166  cdleme17b  38228  cdlemefrs29pre00  38336  cdlemefr27cl  38344  cdleme42ke  38426  cdleme42mgN  38429  cdleme46f2g2  38434  cdleme46f2g1  38435  cdleme50eq  38482  cdleme50trn3  38494  trlord  38510  cdlemg6c  38561  cdlemg11b  38583  cdlemg18a  38619  cdlemg42  38670  cdlemg46  38676  trljco  38681  tendococl  38713  cdlemj3  38764  tendotr  38771  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk53b  38897  cdlemk53  38898  cdlemk35u  38905  tendoex  38916  cdlemm10N  39059  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihglblem5apreN  39232  dihglblem2N  39235  dihmeetlem4preN  39247  dihmeetlem6  39250  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem16N  39263  dihmeetlem17N  39264  dihmeetlem18N  39265  dihmeetlem19N  39266  dihmeetALTN  39268  dihlspsnat  39274  dvh3dim2  39389  dvh3dim3N  39390  jm2.25lem1  40736  jm2.26  40740  grur1cld  41739  limcperiod  43059  0ellimcdiv  43080  cncfshift  43305  cncfperiod  43310  icccncfext  43318  stoweidlem34  43465  fourierdlem48  43585  fourierdlem87  43624  sge0xaddlem2  43862  smflimsuplem7  44246  isomgrsym  45176  domnmsuppn0  45593  itscnhlinecirc02plem2  46017