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  7261  tfisi  7789  funelss  7979  omopth2  8499  swrdsbslen  14569  swrdspsleq  14570  repswswrd  14688  ramub1lem1  16935  cntzsubrng  20480  cntzsubr  20519  lbspss  21014  maducoeval2  22553  cramer  22604  neiptopnei  23045  ptbasin  23490  basqtop  23624  tmdgsum  24008  ustuqtop1  24154  cxplea  26630  cxple2  26631  nosupbnd2lem1  27652  noinfbnd2lem1  27667  sltmul2  28108  ewlkle  29582  uspgr2wlkeq2  29623  clwwlkccat  29965  br8d  32586  isarchi2  33149  archiabllem2c  33159  cvmlift2lem10  35344  5segofs  36039  2llnjaN  39604  lvolnle3at  39620  paddasslem12  39869  paddasslem13  39870  atmod1i1m  39896  lhp2lt  40039  lhpexle2lem  40047  lhpmcvr3  40063  lhpat3  40084  ltrneq2  40186  trlnle  40224  trlval3  40225  trlval4  40226  cdleme0moN  40263  cdleme17b  40325  cdlemefrs29pre00  40433  cdlemefr27cl  40441  cdleme42ke  40523  cdleme42mgN  40526  cdleme46f2g2  40531  cdleme46f2g1  40532  cdleme50eq  40579  cdleme50trn3  40591  trlord  40607  cdlemg6c  40658  cdlemg11b  40680  cdlemg18a  40716  cdlemg42  40767  cdlemg46  40773  trljco  40778  tendococl  40810  cdlemj3  40861  tendotr  40868  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk53b  40994  cdlemk53  40995  cdlemk35u  41002  tendoex  41013  cdlemm10N  41156  dihopelvalcpre  41286  dihord6apre  41294  dihord5b  41297  dihglblem5apreN  41329  dihglblem2N  41332  dihmeetlem4preN  41344  dihmeetlem6  41347  dihmeetlem10N  41354  dihmeetlem11N  41355  dihmeetlem16N  41360  dihmeetlem17N  41361  dihmeetlem18N  41362  dihmeetlem19N  41363  dihmeetALTN  41365  dihlspsnat  41371  dvh3dim2  41486  dvh3dim3N  41487  jm2.25lem1  43030  jm2.26  43034  grur1cld  44264  limcperiod  45667  0ellimcdiv  45686  cncfshift  45911  cncfperiod  45916  icccncfext  45924  stoweidlem34  46071  fourierdlem48  46191  fourierdlem87  46230  sge0xaddlem2  46471  smflimsuplem7  46863  domnmsuppn0  48399  itscnhlinecirc02plem2  48814