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  7305  tfisi  7838  funelss  8029  omopth2  8551  swrdsbslen  14636  swrdspsleq  14637  repswswrd  14756  ramub1lem1  17004  cntzsubrng  20483  cntzsubr  20522  lbspss  20996  maducoeval2  22534  cramer  22585  neiptopnei  23026  ptbasin  23471  basqtop  23605  tmdgsum  23989  ustuqtop1  24136  cxplea  26612  cxple2  26613  nosupbnd2lem1  27634  noinfbnd2lem1  27649  sltmul2  28081  ewlkle  29540  uspgr2wlkeq2  29582  clwwlkccat  29926  br8d  32545  isarchi2  33146  archiabllem2c  33156  cvmlift2lem10  35306  5segofs  36001  2llnjaN  39567  lvolnle3at  39583  paddasslem12  39832  paddasslem13  39833  atmod1i1m  39859  lhp2lt  40002  lhpexle2lem  40010  lhpmcvr3  40026  lhpat3  40047  ltrneq2  40149  trlnle  40187  trlval3  40188  trlval4  40189  cdleme0moN  40226  cdleme17b  40288  cdlemefrs29pre00  40396  cdlemefr27cl  40404  cdleme42ke  40486  cdleme42mgN  40489  cdleme46f2g2  40494  cdleme46f2g1  40495  cdleme50eq  40542  cdleme50trn3  40554  trlord  40570  cdlemg6c  40621  cdlemg11b  40643  cdlemg18a  40679  cdlemg42  40730  cdlemg46  40736  trljco  40741  tendococl  40773  cdlemj3  40824  tendotr  40831  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53b  40957  cdlemk53  40958  cdlemk35u  40965  tendoex  40976  cdlemm10N  41119  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihglblem5apreN  41292  dihglblem2N  41295  dihmeetlem4preN  41307  dihmeetlem6  41310  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem18N  41325  dihmeetlem19N  41326  dihmeetALTN  41328  dihlspsnat  41334  dvh3dim2  41449  dvh3dim3N  41450  jm2.25lem1  42994  jm2.26  42998  grur1cld  44228  limcperiod  45633  0ellimcdiv  45654  cncfshift  45879  cncfperiod  45884  icccncfext  45892  stoweidlem34  46039  fourierdlem48  46159  fourierdlem87  46198  sge0xaddlem2  46439  smflimsuplem7  46831  domnmsuppn0  48361  itscnhlinecirc02plem2  48776