Theorem simpll1 1213

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 726	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:  f1prex  7230  poxp3  8092  naddsuc2  8629  ordiso2  9420  hartogslem1  9447  wemapso2lem  9457  acndom  9961  fin1a2lem12  10321  fin1a2lem13  10322  prlem934  10944  ifle  13112  lcmfunsnlem2lem1  16565  divgcdcoprm0  16592  rpexp  16649  qexpz  16829  ramval  16936  0ram  16948  ramz2  16952  initoeu2lem2  17939  mrelatglb  18483  dfgrp3lem  18968  odbezout  19487  rhmdvdsr  20441  lsmcl  21035  lbsextlem3  21115  rnglidlmcl  21171  frlmsslsp  21751  islindf4  21793  psropprmul  22178  coe1mul2  22211  coe1fzgsumdlem  22247  evl1gsumdlem  22300  scmate  22454  mdetunilem7  22562  mdetmul  22567  cramerlem2  22632  m2pmfzgsumcl  22692  decpmatmul  22716  pmatcollpw3lem  22727  chpdmatlem2  22783  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  chcoeffeqlem  22829  cnconst2  23227  ordthauslem  23327  clsconn  23374  restnlly  23426  comppfsc  23476  ptpjopn  23556  trfg  23835  rnelfmlem  23896  isfcf  23978  fcfnei  23979  cnpfcf  23985  utop2nei  24194  neipcfilu  24239  blssps  24368  blss  24369  metcnp  24485  xrsxmet  24754  metdsge  24794  metdseq0  24799  addcnlem  24809  xrhmeo  24900  nmhmcn  25076  caucfil  25239  limcfval  25829  fta1b  26133  lgsmod  27290  lgsdir  27299  lgsne0  27302  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd2  27684  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd2  27699  cutsun12  27786  ltslpss  27904  leadds1  27985  axpasch  29014  axcontlem2  29038  clwwlknonex2  30184  frgr3v  30350  pjhthmo  31377  difioo  32862  xrge0adddir  33100  archiabl  33280  ssmxidl  33555  dimvalfi  33758  probun  34576  satfv1lem  35556  trisegint  36222  btwnconn1lem13  36293  brsegle2  36303  linethru  36347  lindsadd  37810  hlrelat  39658  intnatN  39663  lnnat  39683  3dim0  39713  3dim1  39723  3dim2  39724  atcvrlln  39776  llnexatN  39777  2at0mat0  39781  llncvrlpln  39814  lplnexllnN  39820  lplncvrlvol  39872  lncvrelatN  40037  lncmp  40039  elpaddn0  40056  paddasslem5  40080  pmapjoin  40108  pmapjat1  40109  pclclN  40147  osumclN  40223  lhprelat3N  40296  trlval4  40444  cdlemd5  40458  cdleme32fvcl  40696  cdleme42keg  40742  cdlemg1a  40826  cdlemg1cN  40843  cdlemg39  40972  ltrncom  40994  cdlemk34  41166  dihord2pre  41481  dihopelvalcpre  41504  dihmeetALTN  41583  dihlspsnssN  41588  dihlspsnat  41589  aks6d1c6isolem1  42424  diophrw  42997  lzunuz  43006  qirropth  43146  jm2.19  43231  jm2.27  43246  lmhmfgsplit  43324  hbtlem5  43366  nadd2rabtr  43622  fzunt  43692  iunrelexpuztr  43956  rfcnnnub  45277  3adantll2  45282  3adantll3  45283  ioondisj2  45735  ioondisj1  45736  iccintsng  45765  icccncfext  46127  stoweidlem20  46260  stoweidlem61  46301  smflimlem2  47012  isuspgrim0lem  48135  isuspgrim0  48136  rmsupp0  48610  rmsuppss  48612  ply1mulgsum  48632  rrxlinesc  48977