Theorem simp-4l 783

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4l	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simp-4l

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad4antr 732	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  naddssim  8722  marypha1lem  9471  acndom2  10092  ttukeylem6  10552  fpwwe2lem11  10679  swrdccatin1  14760  dfgcd2  16580  ramcl  17063  initoeu2lem1  18068  initoeu2  18070  gsmsymgreqlem2  19464  dfod2  19597  pgpfi  19638  ghmcyg  19929  rhmpreimaidl  21305  psgndif  21638  mhpmulcl  22171  scmatmulcl  22540  cpmatmcllem  22740  neiptoptop  23155  cncnp  23304  subislly  23505  ptcnplem  23645  pthaus  23662  xkohaus  23677  kqreglem1  23765  cnextcn  24091  qustgplem  24145  trust  24254  utoptop  24259  restutopopn  24263  utop3cls  24276  utopreg  24277  isucn2  24304  met1stc  24550  metustsym  24584  metuel2  24594  xrge0tsms  24870  xmetdcn2  24873  nmoleub2lem2  25163  iscfil2  25314  iscfil3  25321  dvmptfsum  26028  dvlip2  26049  aannenlem1  26385  ulm2  26443  ulmuni  26450  mtestbdd  26463  efopn  26715  dchrptlem1  27323  pntpbnd  27647  pntibnd  27652  noetasuplem4  27796  f1otrg  28894  nbupgr  29376  upgriswlk  29674  usgr2pth  29797  clwwlkccatlem  30018  clwlkclwwlklem2a4  30026  cusconngr  30220  xrofsup  32778  ressprs  32939  chnind  32985  gsummpt2d  33035  gsumfs2d  33041  xrge0tsmsd  33048  omndmul2  33072  trsp2cyc  33126  isarchi3  33177  archirngz  33179  lmodslmd  33193  elrgspnlem4  33235  suborng  33325  isarchiofld  33327  idlinsubrg  33439  rhmimaidl  33440  dimkerim  33655  sqsscirc1  33869  lmxrge0  33913  lmdvg  33914  esumrnmpt2  34049  esumfsup  34051  esumcvg  34067  esum2d  34074  ddemeas  34217  omssubadd  34282  satffunlem1lem1  35387  satffunlem2lem1  35389  btwnconn1lem13  36081  matunitlindflem1  37603  matunitlindflem2  37604  poimirlem29  37636  mblfinlem3  37646  mblfinlem4  37647  ftc1anclem7  37686  ftc1anc  37688  prdstotbnd  37781  ltrnid  40118  primrootscoprmpow  42081  posbezout  42082  primrootspoweq0  42088  aks6d1c6lem3  42154  unitscyglem3  42179  rencldnfilem  42808  pellex  42823  pellfundex  42874  dvdsacongtr  42973  naddcnff  43352  naddcnfid1  43357  oaun3lem1  43364  fnchoice  44967  climsuse  45564  addlimc  45604  0ellimcdiv  45605  climxrre  45706  xlimmnfvlem2  45789  xlimpnfvlem2  45793  icccncfext  45843  dvnprodlem3  45904  fourierdlem12  46075  fourierdlem34  46097  fourierdlem50  46112  fourierdlem80  46142  fourierdlem81  46143  fourierdlem87  46149  etransclem35  46225  sge0pr  46350  meaiuninc3v  46440  smfmullem3  46749  fsupdm  46798  finfdm  46802  cfsetsnfsetfo  47010  mogoldbb  47710  uzlidlring  48079  2zlidl  48084