Theorem simp-4r 784

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

Assertion

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

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 734	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:  fimaproj  8078  tfrlem1  8308  injresinj  13737  swrdccatin1  14678  reuccatpfxs1  14700  prdsval  17409  catcocl  17642  catass  17643  catpropd  17666  cidpropd  17667  monpropd  17695  subccocl  17803  funcco  17829  funcpropd  17860  fucpropd  17938  initoeu2lem1  17972  xpcpropd  18165  curf2ndf  18204  drsdirfi  18262  chnind  18578  chnub  18579  chnso  18581  mhmmnd  19031  ghmqusnsg  19248  ghmquskerlem3  19252  gsmsymgreqlem2  19397  dfod2  19530  ghmcmn  19797  omndmul2  20099  rhmqusnsg  21275  psgndif  21592  dmatscmcl  22478  smatvscl  22499  cpmatmcllem  22693  pm2mpmhmlem2  22794  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  neitr  23155  1stcrest  23428  dissnref  23503  dissnlocfin  23504  neitx  23582  tgqtop  23687  ptcmplem3  24029  trust  24204  utoptop  24209  restutopopn  24213  ustuqtop2  24217  ustuqtop4  24219  utop3cls  24226  met1stc  24496  prdsxmslem2  24504  metustexhalf  24531  cfilucfil  24534  metucn  24546  aannenlem1  26305  ulmuni  26370  lgamucov  27015  2sqmo  27414  pntpbnd  27565  pntlem3  27586  noetasuplem4  27714  noetainflem4  27718  bdayfinbndlem1  28473  tgbtwndiff  28588  tgifscgr  28590  iscgrglt  28596  tgbtwnconn1lem3  28656  tgbtwnconn1  28657  legov  28667  legtrd  28671  legtri3  28672  ltgseg  28678  legso  28681  tglinethru  28718  tglnpt2  28723  colline  28731  miriso  28752  midexlem  28774  perpneq  28796  isperp2  28797  footexALT  28800  footex  28803  midex  28819  opphllem3  28831  opphl  28836  hlpasch  28838  lnopp2hpgb  28845  lmieu  28866  trgcopyeu  28888  dfcgra2  28912  f1otrg  28953  axcontlem2  29048  2pthon3v  30026  2ndresdju  32737  fnpreimac  32758  fsumiunle  32917  ressprs  33041  dfmgc2  33071  mgcf1o  33078  mndlrinvb  33100  mndlactf1o  33105  gsumfs2d  33137  gsumwun  33152  gsumwrd2dccatlem  33153  tocyccntz  33220  cyc3genpm  33228  cycpmconjs  33232  cyc3conja  33233  isarchi3  33263  isarchiofld  33275  elrgspnlem4  33321  erler  33341  elrlocbasi  33342  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rlocf1  33349  isdrng4  33371  fracfld  33384  imaslmod  33428  dvdsruasso  33460  nsgqusf1olem1  33488  nsgqusf1olem3  33490  lmhmqusker  33492  intlidl  33495  rhmquskerlem  33500  elrspunidl  33503  elrspunsn  33504  idlinsubrg  33506  rhmimaidl  33507  drngidl  33508  isprmidlc  33522  rhmpreimaprmidl  33526  qsidomlem2  33528  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  ssmxidllem  33548  ssmxidl  33549  opprqusplusg  33564  opprqusmulr  33566  qsdrngi  33570  qsdrng  33572  rsprprmprmidlb  33598  rprmdvdsprod  33609  1arithidom  33612  1arithufdlem2  33620  1arithufdlem3  33621  dfufd2lem  33624  r1plmhm  33685  r1pquslmic  33686  lbsdiflsp0  33786  dimkerim  33787  fedgmul  33791  fldextrspunlsplem  33833  extdgfialg  33854  constrconj  33905  constrfin  33906  constrelextdg2  33907  constrextdg2lem  33908  constrfiss  33911  ist0cld  33993  txomap  33994  qtophaus  33996  zarcls1  34029  zarclsint  34032  zarclssn  34033  pstmxmet  34057  sqsscirc1  34068  lmxrge0  34112  esumcst  34223  esumfsup  34230  esum2dlem  34252  esum2d  34253  esumiun  34254  ldsysgenld  34320  sigapildsys  34322  omssubadd  34460  signstfvneq0  34732  actfunsnf1o  34764  afsval  34831  nn0prpwlem  36520  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  mblfinlem3  37994  itg2addnclem  38006  sstotbnd2  38109  prdstotbnd  38129  lcfl8  41962  fldhmf1  42543  mndmolinv  42548  primrootscoprmpow  42552  primrootspoweq0  42559  aks6d1c2p2  42572  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5  42592  aks6d1c6lem3  42625  unitscyglem3  42650  fiabv  42995  dffltz  43081  flt4lem7  43106  nna4b4nsq  43107  diophren  43259  rencldnfilem  43266  pellex  43281  pell1234qrdich  43307  pell1qrgap  43320  pellfundex  43332  omabs2  43778  iunconnlem2  45379  modelaxrep  45426  suplesup  45787  infleinflem2  45818  xrralrecnnle  45830  rexabslelem  45864  limcrecl  46077  limcleqr  46090  0ellimcdiv  46095  limclner  46097  limsupubuz  46159  limsupvaluz2  46184  supcnvlimsup  46186  climxrre  46196  xlimmnfvlem2  46279  xlimmnfv  46280  xlimpnfvlem2  46283  xlimpnfv  46284  icccncfext  46333  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  fourierdlem50  46602  fourierdlem51  46603  fourierdlem80  46632  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  meaiuninc3v  46930  omef  46942  smflimlem2  47218  smflimlem4  47220  smfmullem3  47239  fsupdm  47288  finfdm  47292  chnerlem1  47328  imaf1co  49642  upfval  49663  fuco21  49823  prcofvalg  49863