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  8065  tfrlem1  8295  injresinj  13688  swrdccatin1  14629  reuccatpfxs1  14651  prdsval  17356  catcocl  17588  catass  17589  catpropd  17612  cidpropd  17613  monpropd  17641  subccocl  17749  funcco  17775  funcpropd  17806  fucpropd  17884  initoeu2lem1  17918  xpcpropd  18111  curf2ndf  18150  drsdirfi  18208  chnind  18524  chnub  18525  chnso  18527  mhmmnd  18974  ghmqusnsg  19192  ghmquskerlem3  19196  gsmsymgreqlem2  19341  dfod2  19474  ghmcmn  19741  omndmul2  20043  rhmqusnsg  21220  psgndif  21537  dmatscmcl  22416  smatvscl  22437  cpmatmcllem  22631  pm2mpmhmlem2  22732  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  neitr  23093  1stcrest  23366  dissnref  23441  dissnlocfin  23442  neitx  23520  tgqtop  23625  ptcmplem3  23967  trust  24142  utoptop  24147  restutopopn  24151  ustuqtop2  24155  ustuqtop4  24157  utop3cls  24164  met1stc  24434  prdsxmslem2  24442  metustexhalf  24469  cfilucfil  24472  metucn  24484  aannenlem1  26261  ulmuni  26326  lgamucov  26973  2sqmo  27373  pntpbnd  27524  pntlem3  27545  noetasuplem4  27673  noetainflem4  27677  tgbtwndiff  28482  tgifscgr  28484  iscgrglt  28490  tgbtwnconn1lem3  28550  tgbtwnconn1  28551  legov  28561  legtrd  28565  legtri3  28566  ltgseg  28572  legso  28575  tglinethru  28612  tglnpt2  28617  colline  28625  miriso  28646  midexlem  28668  perpneq  28690  isperp2  28691  footexALT  28694  footex  28697  midex  28713  opphllem3  28725  opphl  28730  hlpasch  28732  lnopp2hpgb  28739  lmieu  28760  trgcopyeu  28782  dfcgra2  28806  f1otrg  28847  axcontlem2  28941  2pthon3v  29919  2ndresdju  32626  fnpreimac  32648  fsumiunle  32807  ressprs  32942  dfmgc2  32972  mgcf1o  32979  mndlrinvb  33001  mndlactf1o  33006  gsumfs2d  33030  gsumwun  33040  gsumwrd2dccatlem  33041  tocyccntz  33108  cyc3genpm  33116  cycpmconjs  33120  cyc3conja  33121  isarchi3  33151  isarchiofld  33163  elrgspnlem4  33207  erler  33227  elrlocbasi  33228  rlocaddval  33230  rlocmulval  33231  rloccring  33232  rlocf1  33235  isdrng4  33256  fracfld  33269  imaslmod  33313  dvdsruasso  33345  nsgqusf1olem1  33373  nsgqusf1olem3  33375  lmhmqusker  33377  intlidl  33380  rhmquskerlem  33385  elrspunidl  33388  elrspunsn  33389  idlinsubrg  33391  rhmimaidl  33392  drngidl  33393  isprmidlc  33407  rhmpreimaprmidl  33411  qsidomlem2  33413  ssdifidllem  33416  ssdifidlprm  33418  mxidlprm  33430  mxidlirredi  33431  ssmxidllem  33433  ssmxidl  33434  opprqusplusg  33449  opprqusmulr  33451  qsdrngi  33455  qsdrng  33457  rsprprmprmidlb  33483  rprmdvdsprod  33494  1arithidom  33497  1arithufdlem2  33505  1arithufdlem3  33506  dfufd2lem  33509  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33634  dimkerim  33635  fedgmul  33639  fldextrspunlsplem  33681  extdgfialg  33702  constrconj  33753  constrfin  33754  constrelextdg2  33755  constrextdg2lem  33756  constrfiss  33759  ist0cld  33841  txomap  33842  qtophaus  33844  zarcls1  33877  zarclsint  33880  zarclssn  33881  pstmxmet  33905  sqsscirc1  33916  lmxrge0  33960  esumcst  34071  esumfsup  34078  esum2dlem  34100  esum2d  34101  esumiun  34102  ldsysgenld  34168  sigapildsys  34170  omssubadd  34308  signstfvneq0  34580  actfunsnf1o  34612  afsval  34679  nn0prpwlem  36355  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  mblfinlem3  37698  itg2addnclem  37710  sstotbnd2  37813  prdstotbnd  37833  lcfl8  41540  fldhmf1  42122  mndmolinv  42127  primrootscoprmpow  42131  primrootspoweq0  42138  aks6d1c2p2  42151  aks6d1c2lem4  42159  aks6d1c2  42162  aks6d1c5  42171  aks6d1c6lem3  42204  unitscyglem3  42229  fiabv  42568  dffltz  42666  flt4lem7  42691  nna4b4nsq  42692  diophren  42845  rencldnfilem  42852  pellex  42867  pell1234qrdich  42893  pell1qrgap  42906  pellfundex  42918  omabs2  43364  iunconnlem2  44966  modelaxrep  45013  suplesup  45377  infleinflem2  45408  xrralrecnnle  45420  rexabslelem  45455  limcrecl  45668  limcleqr  45681  0ellimcdiv  45686  limclner  45688  limsupubuz  45750  limsupvaluz2  45775  supcnvlimsup  45777  climxrre  45787  xlimmnfvlem2  45870  xlimmnfv  45871  xlimpnfvlem2  45874  xlimpnfv  45875  icccncfext  45924  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  fourierdlem50  46193  fourierdlem51  46194  fourierdlem80  46223  fourierdlem87  46230  fourierdlem103  46246  fourierdlem104  46247  meaiuninc3v  46521  omef  46533  smflimlem2  46809  smflimlem4  46811  smfmullem3  46830  fsupdm  46879  finfdm  46883  imaf1co  49186  upfval  49207  fuco21  49367  prcofvalg  49407