Theorem simpll1 1229

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpll1	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simp1 1152	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 738	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  f1prex  7272  poxp3  8134  naddsuc2  8676  ordiso2  9465  hartogslem1  9492  wemapso2lem  9502  acndom  10023  fin1a2lem12  10383  fin1a2lem13  10384  prlem934  11006  ifle  13214  lcmfunsnlem2lem1  16686  divgcdcoprm0  16713  rpexp  16771  qexpz  16951  ramval  17058  0ram  17070  ramz2  17074  initoeu2lem2  18062  mrelatglb  18606  dfgrp3lem  19095  odbezout  19619  rhmdvdsr  20582  lsmcl  21173  lbsextlem3  21253  rnglidlmcl  21310  frlmsslsp  21906  islindf4  21948  psropprmul  22357  coe1mul2  22390  coe1fzgsumdlem  22424  evl1gsumdlem  22477  scmate  22628  mdetunilem7  22736  mdetmul  22741  cramerlem2  22806  m2pmfzgsumcl  22866  decpmatmul  22890  pmatcollpw3lem  22901  chpdmatlem2  22957  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  chcoeffeqlem  23003  cnconst2  23401  ordthauslem  23501  clsconn  23548  restnlly  23600  comppfsc  23650  ptpjopn  23730  trfg  24009  rnelfmlem  24070  isfcf  24152  fcfnei  24153  cnpfcf  24159  utop2nei  24368  neipcfilu  24413  blssps  24542  blss  24543  metcnp  24659  xrsxmet  24928  metdsge  24968  metdseq0  24973  addcnlem  24983  xrhmeo  25066  nmhmcn  25240  caucfil  25403  limcfval  25992  fta1b  26290  lgsmod  27445  lgsdir  27454  lgsne0  27457  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd2  27838  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  noinfbnd2  27853  cutsun12  27941  ltslpss  28059  leadds1  28140  axpasch  29200  axcontlem2  29224  clwwlknonex2  30369  frgr3v  30535  pjhthmo  31563  difioo  33039  xrge0adddir  33251  archiabl  33431  ssmxidl  33674  dimvalfi  33909  probun  34726  satfv1lem  35725  trisegint  36391  btwnconn1lem13  36462  brsegle2  36472  linethru  36516  lindsadd  38124  hlrelat  40038  intnatN  40043  lnnat  40063  3dim0  40093  3dim1  40103  3dim2  40104  atcvrlln  40156  llnexatN  40157  2at0mat0  40161  llncvrlpln  40194  lplnexllnN  40200  lplncvrlvol  40252  lncvrelatN  40417  lncmp  40419  elpaddn0  40436  paddasslem5  40460  pmapjoin  40488  pmapjat1  40489  pclclN  40527  osumclN  40603  lhprelat3N  40676  trlval4  40824  cdlemd5  40838  cdleme32fvcl  41076  cdleme42keg  41122  cdlemg1a  41206  cdlemg1cN  41223  cdlemg39  41352  ltrncom  41374  cdlemk34  41546  dihord2pre  41861  dihopelvalcpre  41884  dihmeetALTN  41963  dihlspsnssN  41968  dihlspsnat  41969  aks6d1c6isolem1  42803  diophrw  43352  lzunuz  43361  qirropth  43497  jm2.19  43582  jm2.27  43597  lmhmfgsplit  43675  hbtlem5  43717  nadd2rabtr  43973  fzunt  44043  iunrelexpuztr  44307  rfcnnnub  45614  3adantll2  45619  3adantll3  45620  ioondisj2  46067  ioondisj1  46068  iccintsng  46097  icccncfext  46459  stoweidlem20  46592  stoweidlem61  46633  smflimlem2  47344  isuspgrim0lem  48513  isuspgrim0  48514  rmsupp0  48999  rmsuppss  49001  ply1mulgsum  49021  rrxlinesc  49366