Theorem simpl1l 1231

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  soisores  7278  tfisi  7806  funelss  7996  omopth2  8516  swrdsbslen  14625  swrdspsleq  14626  repswswrd  14744  ramub1lem1  16995  cntzsubrng  20546  cntzsubr  20585  lbspss  21079  maducoeval2  22630  cramer  22681  neiptopnei  23122  ptbasin  23567  basqtop  23701  tmdgsum  24085  ustuqtop1  24231  cxplea  26685  cxple2  26686  nosupbnd2lem1  27704  noinfbnd2lem1  27719  ltmuls2  28188  ewlkle  29699  uspgr2wlkeq2  29740  clwwlkccat  30085  br8d  32707  isarchi2  33273  archiabllem2c  33283  cvmlift2lem10  35547  5segofs  36241  2llnjaN  40065  lvolnle3at  40081  paddasslem12  40330  paddasslem13  40331  atmod1i1m  40357  lhp2lt  40500  lhpexle2lem  40508  lhpmcvr3  40524  lhpat3  40545  ltrneq2  40647  trlnle  40685  trlval3  40686  trlval4  40687  cdleme0moN  40724  cdleme17b  40786  cdlemefrs29pre00  40894  cdlemefr27cl  40902  cdleme42ke  40984  cdleme42mgN  40987  cdleme46f2g2  40992  cdleme46f2g1  40993  cdleme50eq  41040  cdleme50trn3  41052  trlord  41068  cdlemg6c  41119  cdlemg11b  41141  cdlemg18a  41177  cdlemg42  41228  cdlemg46  41234  trljco  41239  tendococl  41271  cdlemj3  41322  tendotr  41329  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk53b  41455  cdlemk53  41456  cdlemk35u  41463  tendoex  41474  cdlemm10N  41617  dihopelvalcpre  41747  dihord6apre  41755  dihord5b  41758  dihglblem5apreN  41790  dihglblem2N  41793  dihmeetlem4preN  41805  dihmeetlem6  41808  dihmeetlem10N  41815  dihmeetlem11N  41816  dihmeetlem16N  41821  dihmeetlem17N  41822  dihmeetlem18N  41823  dihmeetlem19N  41824  dihmeetALTN  41826  dihlspsnat  41832  dvh3dim2  41947  dvh3dim3N  41948  jm2.25lem1  43450  jm2.26  43454  grur1cld  44683  limcperiod  46080  0ellimcdiv  46099  cncfshift  46324  cncfperiod  46329  icccncfext  46337  stoweidlem34  46484  fourierdlem48  46604  fourierdlem87  46643  sge0xaddlem2  46884  smflimsuplem7  47276  domnmsuppn0  48867  itscnhlinecirc02plem2  49281