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  7268  tfisi  7799  funelss  7989  omopth2  8509  swrdsbslen  14589  swrdspsleq  14590  repswswrd  14708  ramub1lem1  16956  cntzsubrng  20470  cntzsubr  20509  lbspss  21004  maducoeval2  22543  cramer  22594  neiptopnei  23035  ptbasin  23480  basqtop  23614  tmdgsum  23998  ustuqtop1  24145  cxplea  26621  cxple2  26622  nosupbnd2lem1  27643  noinfbnd2lem1  27658  sltmul2  28097  ewlkle  29569  uspgr2wlkeq2  29610  clwwlkccat  29952  br8d  32571  isarchi2  33137  archiabllem2c  33147  cvmlift2lem10  35284  5segofs  35979  2llnjaN  39545  lvolnle3at  39561  paddasslem12  39810  paddasslem13  39811  atmod1i1m  39837  lhp2lt  39980  lhpexle2lem  39988  lhpmcvr3  40004  lhpat3  40025  ltrneq2  40127  trlnle  40165  trlval3  40166  trlval4  40167  cdleme0moN  40204  cdleme17b  40266  cdlemefrs29pre00  40374  cdlemefr27cl  40382  cdleme42ke  40464  cdleme42mgN  40467  cdleme46f2g2  40472  cdleme46f2g1  40473  cdleme50eq  40520  cdleme50trn3  40532  trlord  40548  cdlemg6c  40599  cdlemg11b  40621  cdlemg18a  40657  cdlemg42  40708  cdlemg46  40714  trljco  40719  tendococl  40751  cdlemj3  40802  tendotr  40809  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53b  40935  cdlemk53  40936  cdlemk35u  40943  tendoex  40954  cdlemm10N  41097  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihglblem5apreN  41270  dihglblem2N  41273  dihmeetlem4preN  41285  dihmeetlem6  41288  dihmeetlem10N  41295  dihmeetlem11N  41296  dihmeetlem16N  41301  dihmeetlem17N  41302  dihmeetlem18N  41303  dihmeetlem19N  41304  dihmeetALTN  41306  dihlspsnat  41312  dvh3dim2  41427  dvh3dim3N  41428  jm2.25lem1  42971  jm2.26  42975  grur1cld  44205  limcperiod  45610  0ellimcdiv  45631  cncfshift  45856  cncfperiod  45861  icccncfext  45869  stoweidlem34  46016  fourierdlem48  46136  fourierdlem87  46175  sge0xaddlem2  46416  smflimsuplem7  46808  domnmsuppn0  48354  itscnhlinecirc02plem2  48769