Theorem simp-4r 795

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 745	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fimaproj  8119  tfrlem1  8350  injresinj  13811  swrdccatin1  14752  reuccatpfxs1  14774  prdsval  17498  catcocl  17731  catass  17732  catpropd  17755  cidpropd  17756  monpropd  17784  subccocl  17892  funcco  17918  funcpropd  17949  fucpropd  18027  initoeu2lem1  18061  xpcpropd  18254  curf2ndf  18293  drsdirfi  18351  chnind  18667  chnub  18668  chnso  18670  mhmmnd  19121  ghmqusnsg  19343  ghmquskerlem3  19347  gsmsymgreqlem2  19492  dfod2  19625  ghmcmn  19892  omndmul2  20194  rhmqusnsg  21387  isprmidlc  21434  rhmpreimaprmidl  21439  qsidomlem2  21441  ssdifidllem  21444  ssdifidlprm  21446  psgndif  21712  dmatscmcl  22621  smatvscl  22642  cpmatmcllem  22836  pm2mpmhmlem2  22937  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  neitr  23298  1stcrest  23571  dissnref  23646  dissnlocfin  23647  neitx  23725  tgqtop  23830  ptcmplem3  24172  trust  24347  utoptop  24352  restutopopn  24356  ustuqtop2  24360  ustuqtop4  24362  utop3cls  24369  met1stc  24639  prdsxmslem2  24647  metustexhalf  24674  cfilucfil  24677  metucn  24689  aannenlem1  26450  ulmuni  26513  lgamucov  27160  2sqmo  27559  pntpbnd  27710  pntlem3  27731  noetasuplem4  27858  noetainflem4  27862  bdayfinbndlem1  28618  tgbtwndiff  28733  tgifscgr  28735  iscgrglt  28741  tgbtwnconn1lem3  28801  tgbtwnconn1  28802  legov  28812  legtrd  28816  legtri3  28817  ltgseg  28823  legso  28826  tglinethru  28863  tglinesseq  28867  colline  28877  tglnpt2  28880  tglnpt4  28882  miriso  28901  midexlem  28923  perpneq  28945  isperp2  28946  footexALT  28949  footex  28952  midex  28968  opphllem3  28980  opphl  28985  hlpasch  28987  lnopp2hpgb  28994  plngcplem  29015  lnssplng  29022  plng3p  29023  lmieu  29036  trgcopyeu  29058  dfcgra2  29082  f1otrg  29129  axcontlem2  29224  2pthon3v  30201  2ndresdju  32906  fnpreimac  32927  fsumiunle  33086  ressprs  33199  dfmgc2  33229  mgcf1o  33236  mndlrinvb  33258  mndlactf1o  33263  gsumfs2d  33294  gsumwun  33309  gsumwrd2dccatlem  33310  tocyccntz  33377  cyc3genpm  33385  cycpmconjs  33389  cyc3conja  33390  isarchi3  33420  isarchiofld  33432  elrgspnlem4  33478  erler  33498  elrlocbasi  33500  rlocaddval  33502  rlocmulval  33503  rloccring  33504  rlocf1  33507  rlocisunit  33509  ricdomn1  33522  isdrng4  33531  fracfld  33544  imaslmod  33588  dvdsruasso  33614  nsgqusf1olem1  33638  nsgqusf1olem3  33640  lmhmqusker  33642  intlidl  33644  rhmquskerlem  33649  elrspunidl  33652  elrspunsn  33653  idlinsubrg  33655  rhmimaidl  33656  drngidl  33657  mxidlprm  33670  mxidlirredi  33671  ssmxidllem  33673  ssmxidl  33674  opprqusplusg  33688  opprqusmulr  33690  qsdrngi  33694  qsdrng  33696  drnglring  33699  dflring2  33700  dflringlem3  33703  dflring4  33705  rsprprmprmidlb  33730  rprmdvdsprod  33741  1arithidom  33744  1arithufdlem2  33752  1arithufdlem3  33753  dfufd2lem  33756  r1plmhm  33816  r1pquslmic  33817  mplidomlem  33834  lbsdiflsp0  33933  dimkerim  33934  fedgmul  33938  fldextrspunlsplem  33980  extdgfialg  34001  constrconj  34052  constrfin  34053  constrelextdg2  34054  constrextdg2lem  34055  constrfiss  34058  ist0cld  34140  txomap  34141  qtophaus  34143  zarcls1  34176  zarclsint  34179  zarclssn  34180  pstmxmet  34204  sqsscirc1  34215  lmxrge0  34259  esumcst  34370  esumfsup  34377  esum2dlem  34399  esum2d  34400  esumiun  34401  ldsysgenld  34467  sigapildsys  34469  omssubadd  34607  signstfvneq0  34876  actfunsnf1o  34908  afsval  34978  nn0prpwlem  36695  lindsenlbs  38126  matunitlindflem1  38127  matunitlindflem2  38128  mblfinlem3  38170  itg2addnclem  38182  sstotbnd2  38285  prdstotbnd  38305  lcfl8  42138  fldhmf1  42719  mndmolinv  42724  primrootscoprmpow  42728  primrootspoweq0  42735  aks6d1c2p2  42748  aks6d1c2lem4  42756  aks6d1c2  42759  aks6d1c5  42768  aks6d1c6lem3  42801  unitscyglem3  42826  fiabv  43166  dffltz  43228  flt4lem7  43253  nna4b4nsq  43254  diophren  43402  rencldnfilem  43409  pellex  43424  pell1234qrdich  43450  pell1qrgap  43463  pellfundex  43475  omabs2  43921  iunconnlem2  45508  modelaxrep  45555  suplesup  45913  infleinflem2  45944  xrralrecnnle  45956  rexabslelem  45990  limcrecl  46203  limcleqr  46216  0ellimcdiv  46221  limclner  46223  limsupubuz  46285  limsupvaluz2  46310  supcnvlimsup  46312  climxrre  46322  xlimmnfvlem2  46405  xlimmnfv  46406  xlimpnfvlem2  46409  xlimpnfv  46410  icccncfext  46459  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  fourierdlem50  46728  fourierdlem51  46729  fourierdlem80  46758  fourierdlem87  46765  fourierdlem103  46781  fourierdlem104  46782  meaiuninc3v  47056  omef  47068  smflimlem2  47344  smflimlem4  47346  smfmullem3  47365  fsupdm  47414  finfdm  47418  chnerlem1  47456  imaf1co  49784  upfval  49805  fuco21  49965  prcofvalg  50005