Theorem simpl1l 1237

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soisores  7307  tfisi  7835  funelss  8024  omopth2  8548  swrdsbslen  14675  swrdspsleq  14676  repswswrd  14794  ramub1lem1  17045  cntzsubrng  20596  cntzsubr  20635  lbspss  21129  maducoeval2  22680  cramer  22731  neiptopnei  23172  ptbasin  23617  basqtop  23751  tmdgsum  24135  ustuqtop1  24281  cxplea  26738  cxple2  26739  nosupbnd2lem1  27756  noinfbnd2lem1  27771  ltmuls2  28241  ewlkle  29752  uspgr2wlkeq2  29793  clwwlkccat  30138  br8d  32760  isarchi2  33326  archiabllem2c  33336  cvmlift2lem10  35626  5segofs  36320  2llnjaN  40154  lvolnle3at  40170  paddasslem12  40419  paddasslem13  40420  atmod1i1m  40446  lhp2lt  40589  lhpexle2lem  40597  lhpmcvr3  40613  lhpat3  40634  ltrneq2  40736  trlnle  40774  trlval3  40775  trlval4  40776  cdleme0moN  40813  cdleme17b  40875  cdlemefrs29pre00  40983  cdlemefr27cl  40991  cdleme42ke  41073  cdleme42mgN  41076  cdleme46f2g2  41081  cdleme46f2g1  41082  cdleme50eq  41129  cdleme50trn3  41141  trlord  41157  cdlemg6c  41208  cdlemg11b  41230  cdlemg18a  41266  cdlemg42  41317  cdlemg46  41323  trljco  41328  tendococl  41360  cdlemj3  41411  tendotr  41418  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk53b  41544  cdlemk53  41545  cdlemk35u  41552  tendoex  41563  cdlemm10N  41706  dihopelvalcpre  41836  dihord6apre  41844  dihord5b  41847  dihglblem5apreN  41879  dihglblem2N  41882  dihmeetlem4preN  41894  dihmeetlem6  41897  dihmeetlem10N  41904  dihmeetlem11N  41905  dihmeetlem16N  41910  dihmeetlem17N  41911  dihmeetlem18N  41912  dihmeetlem19N  41913  dihmeetALTN  41915  dihlspsnat  41921  dvh3dim2  42036  dvh3dim3N  42037  jm2.25lem1  43539  jm2.26  43543  grur1cld  44772  limcperiod  46168  0ellimcdiv  46187  cncfshift  46412  cncfperiod  46417  icccncfext  46425  stoweidlem34  46572  fourierdlem48  46692  fourierdlem87  46731  sge0xaddlem2  46972  smflimsuplem7  47364  domnmsuppn0  48955  itscnhlinecirc02plem2  49369