Theorem simp-4r 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-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 733	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  8117  tfrlem1  8347  injresinj  13756  swrdccatin1  14697  reuccatpfxs1  14719  prdsval  17425  catcocl  17653  catass  17654  catpropd  17677  cidpropd  17678  monpropd  17706  subccocl  17814  funcco  17840  funcpropd  17871  fucpropd  17949  initoeu2lem1  17983  xpcpropd  18176  curf2ndf  18215  drsdirfi  18273  mhmmnd  19003  ghmqusnsg  19221  ghmquskerlem3  19225  gsmsymgreqlem2  19368  dfod2  19501  ghmcmn  19768  rhmqusnsg  21202  psgndif  21518  dmatscmcl  22397  smatvscl  22418  cpmatmcllem  22612  pm2mpmhmlem2  22713  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  neitr  23074  1stcrest  23347  dissnref  23422  dissnlocfin  23423  neitx  23501  tgqtop  23606  ptcmplem3  23948  trust  24124  utoptop  24129  restutopopn  24133  ustuqtop2  24137  ustuqtop4  24139  utop3cls  24146  met1stc  24416  prdsxmslem2  24424  metustexhalf  24451  cfilucfil  24454  metucn  24466  aannenlem1  26243  ulmuni  26308  lgamucov  26955  2sqmo  27355  pntpbnd  27506  pntlem3  27527  noetasuplem4  27655  noetainflem4  27659  tgbtwndiff  28440  tgifscgr  28442  iscgrglt  28448  tgbtwnconn1lem3  28508  tgbtwnconn1  28509  legov  28519  legtrd  28523  legtri3  28524  ltgseg  28530  legso  28533  tglinethru  28570  tglnpt2  28575  colline  28583  miriso  28604  midexlem  28626  perpneq  28648  isperp2  28649  footexALT  28652  footex  28655  midex  28671  opphllem3  28683  opphl  28688  hlpasch  28690  lnopp2hpgb  28697  lmieu  28718  trgcopyeu  28740  dfcgra2  28764  f1otrg  28805  axcontlem2  28899  2pthon3v  29880  2ndresdju  32580  fnpreimac  32602  fsumiunle  32761  ressprs  32897  dfmgc2  32929  mgcf1o  32936  chnind  32944  chnub  32945  chnso  32947  mndlrinvb  32973  mndlactf1o  32978  gsumfs2d  33002  gsumwun  33012  gsumwrd2dccatlem  33013  omndmul2  33033  tocyccntz  33108  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  isarchi3  33148  elrgspnlem4  33203  erler  33223  elrlocbasi  33224  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rlocf1  33231  isdrng4  33252  fracfld  33265  isarchiofld  33302  imaslmod  33331  dvdsruasso  33363  nsgqusf1olem1  33391  nsgqusf1olem3  33393  lmhmqusker  33395  intlidl  33398  rhmquskerlem  33403  elrspunidl  33406  elrspunsn  33407  idlinsubrg  33409  rhmimaidl  33410  drngidl  33411  isprmidlc  33425  rhmpreimaprmidl  33429  qsidomlem2  33431  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  ssmxidllem  33451  ssmxidl  33452  opprqusplusg  33467  opprqusmulr  33469  qsdrngi  33473  qsdrng  33475  rsprprmprmidlb  33501  rprmdvdsprod  33512  1arithidom  33515  1arithufdlem2  33523  1arithufdlem3  33524  dfufd2lem  33527  r1plmhm  33582  r1pquslmic  33583  lbsdiflsp0  33629  dimkerim  33630  fedgmul  33634  fldextrspunlsplem  33675  constrconj  33742  constrfin  33743  constrelextdg2  33744  constrextdg2lem  33745  constrfiss  33748  ist0cld  33830  txomap  33831  qtophaus  33833  zarcls1  33866  zarclsint  33869  zarclssn  33870  pstmxmet  33894  sqsscirc1  33905  lmxrge0  33949  esumcst  34060  esumfsup  34067  esum2dlem  34089  esum2d  34090  esumiun  34091  ldsysgenld  34157  sigapildsys  34159  omssubadd  34298  signstfvneq0  34570  actfunsnf1o  34602  afsval  34669  nn0prpwlem  36317  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  mblfinlem3  37660  itg2addnclem  37672  sstotbnd2  37775  prdstotbnd  37795  lcfl8  41503  fldhmf1  42085  mndmolinv  42090  primrootscoprmpow  42094  primrootspoweq0  42101  aks6d1c2p2  42114  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5  42134  aks6d1c6lem3  42167  unitscyglem3  42192  fiabv  42531  dffltz  42629  flt4lem7  42654  nna4b4nsq  42655  diophren  42808  rencldnfilem  42815  pellex  42830  pell1234qrdich  42856  pell1qrgap  42869  pellfundex  42881  omabs2  43328  iunconnlem2  44931  modelaxrep  44978  suplesup  45342  infleinflem2  45374  xrralrecnnle  45386  rexabslelem  45421  limcrecl  45634  limcleqr  45649  0ellimcdiv  45654  limclner  45656  limsupubuz  45718  limsupvaluz2  45743  supcnvlimsup  45745  climxrre  45755  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  icccncfext  45892  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  fourierdlem50  46161  fourierdlem51  46162  fourierdlem80  46191  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  meaiuninc3v  46489  omef  46501  smflimlem2  46777  smflimlem4  46779  smfmullem3  46798  fsupdm  46847  finfdm  46851  imaf1co  49148  upfval  49169  fuco21  49329  prcofvalg  49369