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  7273  tfisi  7801  funelss  7991  omopth2  8511  swrdsbslen  14588  swrdspsleq  14589  repswswrd  14707  ramub1lem1  16954  cntzsubrng  20500  cntzsubr  20539  lbspss  21034  maducoeval2  22584  cramer  22635  neiptopnei  23076  ptbasin  23521  basqtop  23655  tmdgsum  24039  ustuqtop1  24185  cxplea  26661  cxple2  26662  nosupbnd2lem1  27683  noinfbnd2lem1  27698  ltmuls2  28167  ewlkle  29679  uspgr2wlkeq2  29720  clwwlkccat  30065  br8d  32686  isarchi2  33267  archiabllem2c  33277  cvmlift2lem10  35506  5segofs  36200  2llnjaN  39822  lvolnle3at  39838  paddasslem12  40087  paddasslem13  40088  atmod1i1m  40114  lhp2lt  40257  lhpexle2lem  40265  lhpmcvr3  40281  lhpat3  40302  ltrneq2  40404  trlnle  40442  trlval3  40443  trlval4  40444  cdleme0moN  40481  cdleme17b  40543  cdlemefrs29pre00  40651  cdlemefr27cl  40659  cdleme42ke  40741  cdleme42mgN  40744  cdleme46f2g2  40749  cdleme46f2g1  40750  cdleme50eq  40797  cdleme50trn3  40809  trlord  40825  cdlemg6c  40876  cdlemg11b  40898  cdlemg18a  40934  cdlemg42  40985  cdlemg46  40991  trljco  40996  tendococl  41028  cdlemj3  41079  tendotr  41086  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk53b  41212  cdlemk53  41213  cdlemk35u  41220  tendoex  41231  cdlemm10N  41374  dihopelvalcpre  41504  dihord6apre  41512  dihord5b  41515  dihglblem5apreN  41547  dihglblem2N  41550  dihmeetlem4preN  41562  dihmeetlem6  41565  dihmeetlem10N  41572  dihmeetlem11N  41573  dihmeetlem16N  41578  dihmeetlem17N  41579  dihmeetlem18N  41580  dihmeetlem19N  41581  dihmeetALTN  41583  dihlspsnat  41589  dvh3dim2  41704  dvh3dim3N  41705  jm2.25lem1  43236  jm2.26  43240  grur1cld  44469  limcperiod  45870  0ellimcdiv  45889  cncfshift  46114  cncfperiod  46119  icccncfext  46127  stoweidlem34  46274  fourierdlem48  46394  fourierdlem87  46433  sge0xaddlem2  46674  smflimsuplem7  47066  domnmsuppn0  48611  itscnhlinecirc02plem2  49025