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  7319  tfisi  7852  funelss  8044  omopth2  8594  swrdsbslen  14680  swrdspsleq  14681  repswswrd  14800  ramub1lem1  17044  cntzsubrng  20525  cntzsubr  20564  lbspss  21038  maducoeval2  22576  cramer  22627  neiptopnei  23068  ptbasin  23513  basqtop  23647  tmdgsum  24031  ustuqtop1  24178  cxplea  26655  cxple2  26656  nosupbnd2lem1  27677  noinfbnd2lem1  27692  sltmul2  28114  ewlkle  29531  uspgr2wlkeq2  29573  clwwlkccat  29917  br8d  32536  isarchi2  33129  archiabllem2c  33139  cvmlift2lem10  35280  5segofs  35970  2llnjaN  39531  lvolnle3at  39547  paddasslem12  39796  paddasslem13  39797  atmod1i1m  39823  lhp2lt  39966  lhpexle2lem  39974  lhpmcvr3  39990  lhpat3  40011  ltrneq2  40113  trlnle  40151  trlval3  40152  trlval4  40153  cdleme0moN  40190  cdleme17b  40252  cdlemefrs29pre00  40360  cdlemefr27cl  40368  cdleme42ke  40450  cdleme42mgN  40453  cdleme46f2g2  40458  cdleme46f2g1  40459  cdleme50eq  40506  cdleme50trn3  40518  trlord  40534  cdlemg6c  40585  cdlemg11b  40607  cdlemg18a  40643  cdlemg42  40694  cdlemg46  40700  trljco  40705  tendococl  40737  cdlemj3  40788  tendotr  40795  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk53b  40921  cdlemk53  40922  cdlemk35u  40929  tendoex  40940  cdlemm10N  41083  dihopelvalcpre  41213  dihord6apre  41221  dihord5b  41224  dihglblem5apreN  41256  dihglblem2N  41259  dihmeetlem4preN  41271  dihmeetlem6  41274  dihmeetlem10N  41281  dihmeetlem11N  41282  dihmeetlem16N  41287  dihmeetlem17N  41288  dihmeetlem18N  41289  dihmeetlem19N  41290  dihmeetALTN  41292  dihlspsnat  41298  dvh3dim2  41413  dvh3dim3N  41414  jm2.25lem1  42969  jm2.26  42973  grur1cld  44204  limcperiod  45605  0ellimcdiv  45626  cncfshift  45851  cncfperiod  45856  icccncfext  45864  stoweidlem34  46011  fourierdlem48  46131  fourierdlem87  46170  sge0xaddlem2  46411  smflimsuplem7  46803  domnmsuppn0  48292  itscnhlinecirc02plem2  48711