Theorem simpl1l 1222

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 1183	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  soisores  7329  tfisi  7855  funelss  8043  omopth2  8596  swrdsbslen  14632  swrdspsleq  14633  repswswrd  14752  ramub1lem1  16980  cntzsubrng  20486  cntzsubr  20527  lbspss  20949  maducoeval2  22516  cramer  22567  neiptopnei  23010  ptbasin  23455  basqtop  23589  tmdgsum  23973  ustuqtop1  24120  cxplea  26604  cxple2  26605  nosupbnd2lem1  27622  noinfbnd2lem1  27637  sltmul2  28045  ewlkle  29393  uspgr2wlkeq2  29435  clwwlkccat  29774  br8d  32370  isarchi2  32858  archiabllem2c  32868  cvmlift2lem10  34845  5segofs  35525  2llnjaN  38963  lvolnle3at  38979  paddasslem12  39228  paddasslem13  39229  atmod1i1m  39255  lhp2lt  39398  lhpexle2lem  39406  lhpmcvr3  39422  lhpat3  39443  ltrneq2  39545  trlnle  39583  trlval3  39584  trlval4  39585  cdleme0moN  39622  cdleme17b  39684  cdlemefrs29pre00  39792  cdlemefr27cl  39800  cdleme42ke  39882  cdleme42mgN  39885  cdleme46f2g2  39890  cdleme46f2g1  39891  cdleme50eq  39938  cdleme50trn3  39950  trlord  39966  cdlemg6c  40017  cdlemg11b  40039  cdlemg18a  40075  cdlemg42  40126  cdlemg46  40132  trljco  40137  tendococl  40169  cdlemj3  40220  tendotr  40227  cdlemk35s-id  40335  cdlemk39s-id  40337  cdlemk53b  40353  cdlemk53  40354  cdlemk35u  40361  tendoex  40372  cdlemm10N  40515  dihopelvalcpre  40645  dihord6apre  40653  dihord5b  40656  dihglblem5apreN  40688  dihglblem2N  40691  dihmeetlem4preN  40703  dihmeetlem6  40706  dihmeetlem10N  40713  dihmeetlem11N  40714  dihmeetlem16N  40719  dihmeetlem17N  40720  dihmeetlem18N  40721  dihmeetlem19N  40722  dihmeetALTN  40724  dihlspsnat  40730  dvh3dim2  40845  dvh3dim3N  40846  jm2.25lem1  42331  jm2.26  42335  grur1cld  43582  limcperiod  44929  0ellimcdiv  44950  cncfshift  45175  cncfperiod  45180  icccncfext  45188  stoweidlem34  45335  fourierdlem48  45455  fourierdlem87  45494  sge0xaddlem2  45735  smflimsuplem7  46127  domnmsuppn0  47346  itscnhlinecirc02plem2  47769