Theorem simp-4r 789

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fimaproj  8082  tfrlem1  8312  injresinj  13744  swrdccatin1  14685  reuccatpfxs1  14707  prdsval  17416  catcocl  17649  catass  17650  catpropd  17673  cidpropd  17674  monpropd  17702  subccocl  17810  funcco  17836  funcpropd  17867  fucpropd  17945  initoeu2lem1  17979  xpcpropd  18172  curf2ndf  18211  drsdirfi  18269  chnind  18585  chnub  18586  chnso  18588  mhmmnd  19038  ghmqusnsg  19255  ghmquskerlem3  19259  gsmsymgreqlem2  19404  dfod2  19537  ghmcmn  19804  omndmul2  20106  rhmqusnsg  21285  psgndif  21584  dmatscmcl  22493  smatvscl  22514  cpmatmcllem  22708  pm2mpmhmlem2  22809  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  neitr  23170  1stcrest  23443  dissnref  23518  dissnlocfin  23519  neitx  23597  tgqtop  23702  ptcmplem3  24044  trust  24219  utoptop  24224  restutopopn  24228  ustuqtop2  24232  ustuqtop4  24234  utop3cls  24241  met1stc  24511  prdsxmslem2  24519  metustexhalf  24546  cfilucfil  24549  metucn  24561  aannenlem1  26319  ulmuni  26382  lgamucov  27026  2sqmo  27425  pntpbnd  27576  pntlem3  27597  noetasuplem4  27725  noetainflem4  27729  bdayfinbndlem1  28484  tgbtwndiff  28599  tgifscgr  28601  iscgrglt  28607  tgbtwnconn1lem3  28667  tgbtwnconn1  28668  legov  28678  legtrd  28682  legtri3  28683  ltgseg  28689  legso  28692  tglinethru  28729  tglnpt2  28734  colline  28742  miriso  28763  midexlem  28785  perpneq  28807  isperp2  28808  footexALT  28811  footex  28814  midex  28830  opphllem3  28842  opphl  28847  hlpasch  28849  lnopp2hpgb  28856  lmieu  28877  trgcopyeu  28899  dfcgra2  28923  f1otrg  28964  axcontlem2  29059  2pthon3v  30036  2ndresdju  32748  fnpreimac  32769  fsumiunle  32928  ressprs  33052  dfmgc2  33082  mgcf1o  33089  mndlrinvb  33111  mndlactf1o  33116  gsumfs2d  33149  gsumwun  33164  gsumwrd2dccatlem  33165  tocyccntz  33232  cyc3genpm  33240  cycpmconjs  33244  cyc3conja  33245  isarchi3  33275  isarchiofld  33287  elrgspnlem4  33333  erler  33353  elrlocbasi  33354  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rlocf1  33361  ricdomn1  33377  isdrng4  33386  fracfld  33399  imaslmod  33443  dvdsruasso  33475  nsgqusf1olem1  33503  nsgqusf1olem3  33505  lmhmqusker  33507  intlidl  33510  rhmquskerlem  33515  elrspunidl  33518  elrspunsn  33519  idlinsubrg  33521  rhmimaidl  33522  drngidl  33523  isprmidlc  33537  rhmpreimaprmidl  33541  qsidomlem2  33543  ssdifidllem  33546  ssdifidlprm  33548  mxidlprm  33560  mxidlirredi  33561  ssmxidllem  33563  ssmxidl  33564  opprqusplusg  33579  opprqusmulr  33581  qsdrngi  33585  qsdrng  33587  rsprprmprmidlb  33613  rprmdvdsprod  33624  1arithidom  33627  1arithufdlem2  33635  1arithufdlem3  33636  dfufd2lem  33639  r1plmhm  33700  r1pquslmic  33701  mplidomlem  33718  lbsdiflsp0  33817  dimkerim  33818  fedgmul  33822  fldextrspunlsplem  33864  extdgfialg  33885  constrconj  33936  constrfin  33937  constrelextdg2  33938  constrextdg2lem  33939  constrfiss  33942  ist0cld  34024  txomap  34025  qtophaus  34027  zarcls1  34060  zarclsint  34063  zarclssn  34064  pstmxmet  34088  sqsscirc1  34099  lmxrge0  34143  esumcst  34254  esumfsup  34261  esum2dlem  34283  esum2d  34284  esumiun  34285  ldsysgenld  34351  sigapildsys  34353  omssubadd  34491  signstfvneq0  34763  actfunsnf1o  34795  afsval  34862  nn0prpwlem  36557  lindsenlbs  37989  matunitlindflem1  37990  matunitlindflem2  37991  mblfinlem3  38033  itg2addnclem  38045  sstotbnd2  38148  prdstotbnd  38168  lcfl8  42001  fldhmf1  42582  mndmolinv  42587  primrootscoprmpow  42591  primrootspoweq0  42598  aks6d1c2p2  42611  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c5  42631  aks6d1c6lem3  42664  unitscyglem3  42689  fiabv  43029  dffltz  43091  flt4lem7  43116  nna4b4nsq  43117  diophren  43265  rencldnfilem  43272  pellex  43287  pell1234qrdich  43313  pell1qrgap  43326  pellfundex  43338  omabs2  43784  iunconnlem2  45385  modelaxrep  45432  suplesup  45791  infleinflem2  45822  xrralrecnnle  45834  rexabslelem  45868  limcrecl  46081  limcleqr  46094  0ellimcdiv  46099  limclner  46101  limsupubuz  46163  limsupvaluz2  46188  supcnvlimsup  46190  climxrre  46200  xlimmnfvlem2  46283  xlimmnfv  46284  xlimpnfvlem2  46287  xlimpnfv  46288  icccncfext  46337  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  fourierdlem50  46606  fourierdlem51  46607  fourierdlem80  46636  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  meaiuninc3v  46934  omef  46946  smflimlem2  47222  smflimlem4  47224  smfmullem3  47243  fsupdm  47292  finfdm  47296  chnerlem1  47334  imaf1co  49652  upfval  49673  fuco21  49833  prcofvalg  49873