Theorem simp-4l 781

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  naddssim  8704  marypha1lem  9456  acndom2  10077  ttukeylem6  10537  fpwwe2lem11  10664  swrdccatin1  14707  dfgcd2  16521  ramcl  16997  initoeu2lem1  18002  initoeu2  18004  gsmsymgreqlem2  19390  dfod2  19523  pgpfi  19564  ghmcyg  19855  psgndif  21538  mhpmulcl  22081  scmatmulcl  22450  cpmatmcllem  22650  neiptoptop  23065  cncnp  23214  subislly  23415  ptcnplem  23555  pthaus  23572  xkohaus  23587  kqreglem1  23675  cnextcn  24001  qustgplem  24055  trust  24164  utoptop  24169  restutopopn  24173  utop3cls  24186  utopreg  24187  isucn2  24214  met1stc  24460  metustsym  24494  metuel2  24504  xrge0tsms  24780  xmetdcn2  24783  nmoleub2lem2  25073  iscfil2  25224  iscfil3  25231  dvmptfsum  25937  dvlip2  25958  aannenlem1  26293  ulm2  26351  ulmuni  26358  mtestbdd  26371  efopn  26622  dchrptlem1  27227  pntpbnd  27551  pntibnd  27556  noetasuplem4  27699  f1otrg  28731  nbupgr  29213  upgriswlk  29511  usgr2pth  29634  clwwlkccatlem  29855  clwlkclwwlklem2a4  29863  cusconngr  30057  xrofsup  32594  ressprs  32747  gsummpt2d  32820  xrge0tsmsd  32828  omndmul2  32849  trsp2cyc  32901  isarchi3  32952  archirngz  32954  lmodslmd  32968  suborng  33090  isarchiofld  33092  rhmpreimaidl  33195  idlinsubrg  33209  rhmimaidl  33210  dimkerim  33395  sqsscirc1  33579  lmxrge0  33623  lmdvg  33624  esumrnmpt2  33757  esumfsup  33759  esumcvg  33775  esum2d  33782  ddemeas  33925  omssubadd  33990  satffunlem1lem1  35082  satffunlem2lem1  35084  btwnconn1lem13  35765  matunitlindflem1  37159  matunitlindflem2  37160  poimirlem29  37192  mblfinlem3  37202  mblfinlem4  37203  ftc1anclem7  37242  ftc1anc  37244  prdstotbnd  37337  ltrnid  39677  primrootscoprmpow  41639  posbezout  41640  primrootspoweq0  41646  aks6d1c6lem3  41713  rencldnfilem  42305  pellex  42320  pellfundex  42371  dvdsacongtr  42470  naddcnff  42856  naddcnfid1  42861  oaun3lem1  42868  fnchoice  44456  climsuse  45059  addlimc  45099  0ellimcdiv  45100  climxrre  45201  xlimmnfvlem2  45284  xlimpnfvlem2  45288  icccncfext  45338  dvnprodlem3  45399  fourierdlem12  45570  fourierdlem34  45592  fourierdlem50  45607  fourierdlem80  45637  fourierdlem81  45638  fourierdlem87  45644  etransclem35  45720  sge0pr  45845  meaiuninc3v  45935  smfmullem3  46244  fsupdm  46293  finfdm  46297  cfsetsnfsetfo  46505  mogoldbb  47188  uzlidlring  47409  2zlidl  47414