Theorem simp-4l 782

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  8610  marypha1lem  9342  acndom2  9967  ttukeylem6  10427  fpwwe2lem11  10554  swrdccatin1  14649  dfgcd2  16475  ramcl  16959  initoeu2lem1  17939  initoeu2  17941  gsmsymgreqlem2  19328  dfod2  19461  pgpfi  19502  ghmcyg  19793  omndmul2  20030  suborng  20779  rhmpreimaidl  21202  psgndif  21527  mhpmulcl  22052  scmatmulcl  22421  cpmatmcllem  22621  neiptoptop  23034  cncnp  23183  subislly  23384  ptcnplem  23524  pthaus  23541  xkohaus  23556  kqreglem1  23644  cnextcn  23970  qustgplem  24024  trust  24133  utoptop  24138  restutopopn  24142  utop3cls  24155  utopreg  24156  isucn2  24182  met1stc  24425  metustsym  24459  metuel2  24469  xrge0tsms  24739  xmetdcn2  24742  nmoleub2lem2  25032  iscfil2  25182  iscfil3  25189  dvmptfsum  25895  dvlip2  25916  aannenlem1  26252  ulm2  26310  ulmuni  26317  mtestbdd  26330  efopn  26583  dchrptlem1  27191  pntpbnd  27515  pntibnd  27520  noetasuplem4  27664  f1otrg  28834  nbupgr  29307  upgriswlk  29604  usgr2pth  29727  clwwlkccatlem  29951  clwlkclwwlklem2a4  29959  cusconngr  30153  xrofsup  32723  ressprs  32921  chnind  32966  gsummpt2d  33015  gsumfs2d  33021  xrge0tsmsd  33028  trsp2cyc  33078  isarchi3  33139  archirngz  33141  isarchiofld  33151  lmodslmd  33156  elrgspnlem4  33195  idlinsubrg  33378  rhmimaidl  33379  dimkerim  33599  sqsscirc1  33874  lmxrge0  33918  lmdvg  33919  esumrnmpt2  34034  esumfsup  34036  esumcvg  34052  esum2d  34059  ddemeas  34202  omssubadd  34267  satffunlem1lem1  35374  satffunlem2lem1  35376  btwnconn1lem13  36072  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem29  37628  mblfinlem3  37638  mblfinlem4  37639  ftc1anclem7  37678  ftc1anc  37680  prdstotbnd  37773  ltrnid  40114  primrootscoprmpow  42072  posbezout  42073  primrootspoweq0  42079  aks6d1c6lem3  42145  unitscyglem3  42170  rencldnfilem  42793  pellex  42808  pellfundex  42859  dvdsacongtr  42957  naddcnff  43335  naddcnfid1  43340  oaun3lem1  43347  fnchoice  45007  climsuse  45590  addlimc  45630  0ellimcdiv  45631  climxrre  45732  xlimmnfvlem2  45815  xlimpnfvlem2  45819  icccncfext  45869  dvnprodlem3  45930  fourierdlem12  46101  fourierdlem34  46123  fourierdlem50  46138  fourierdlem80  46168  fourierdlem81  46169  fourierdlem87  46175  etransclem35  46251  sge0pr  46376  meaiuninc3v  46466  smfmullem3  46775  fsupdm  46824  finfdm  46828  cfsetsnfsetfo  47045  mogoldbb  47770  uzlidlring  48207  2zlidl  48212