Theorem simpl1l 1243

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7336  tfisi  7864  funelss  8053  omopth2  8578  swrdsbslen  14726  swrdspsleq  14727  repswswrd  14847  ramub1lem1  17111  cntzsubrng  20703  cntzsubr  20742  lbspss  21240  maducoeval2  22834  cramer  22885  neiptopnei  23326  ptbasin  23771  basqtop  23905  tmdgsum  24289  ustuqtop1  24435  cxplea  26898  cxple2  26899  nosupbnd2lem1  27916  noinfbnd2lem1  27931  ltmuls2  28401  ewlkle  29992  uspgr2wlkeq2  30033  clwwlkccat  30378  br8d  32990  isarchi2  33536  archiabllem2c  33546  cvmlift2lem10  35825  5segofs  36519  2llnjaN  40381  lvolnle3at  40397  paddasslem12  40646  paddasslem13  40647  atmod1i1m  40673  lhp2lt  40816  lhpexle2lem  40824  lhpmcvr3  40840  lhpat3  40861  ltrneq2  40963  trlnle  41001  trlval3  41002  trlval4  41003  cdleme0moN  41040  cdleme17b  41102  cdlemefrs29pre00  41210  cdlemefr27cl  41218  cdleme42ke  41300  cdleme42mgN  41303  cdleme46f2g2  41308  cdleme46f2g1  41309  cdleme50eq  41356  cdleme50trn3  41368  trlord  41384  cdlemg6c  41435  cdlemg11b  41457  cdlemg18a  41493  cdlemg42  41544  cdlemg46  41550  trljco  41555  tendococl  41587  cdlemj3  41638  tendotr  41645  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk53b  41771  cdlemk53  41772  cdlemk35u  41779  tendoex  41790  cdlemm10N  41933  dihopelvalcpre  42063  dihord6apre  42071  dihord5b  42074  dihglblem5apreN  42106  dihglblem2N  42109  dihmeetlem4preN  42121  dihmeetlem6  42124  dihmeetlem10N  42131  dihmeetlem11N  42132  dihmeetlem16N  42137  dihmeetlem17N  42138  dihmeetlem18N  42139  dihmeetlem19N  42140  dihmeetALTN  42142  dihlspsnat  42148  dvh3dim2  42263  dvh3dim3N  42264  jm2.25lem1  43766  jm2.26  43770  grur1cld  44997  limcperiod  46385  0ellimcdiv  46404  cncfshift  46629  cncfperiod  46634  icccncfext  46642  stoweidlem34  46789  fourierdlem48  46909  fourierdlem87  46948  sge0xaddlem2  47189  smflimsuplem7  47581  domnmsuppn0  49190  itscnhlinecirc02plem2  49604