Theorem simp-4r 781

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 730	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 206  df-an 396

This theorem is referenced by:  fimaproj  8126  tfrlem1  8382  injresinj  13760  swrdccatin1  14682  reuccatpfxs1  14704  prdsval  17408  catcocl  17636  catass  17637  catpropd  17660  cidpropd  17661  monpropd  17691  subccocl  17802  funcco  17828  funcpropd  17860  fucpropd  17940  initoeu2lem1  17974  xpcpropd  18171  curf2ndf  18210  drsdirfi  18268  mhmmnd  18990  gsmsymgreqlem2  19347  dfod2  19480  ghmcmn  19747  psgndif  21465  mhpmulcl  22001  dmatscmcl  22325  smatvscl  22346  cpmatmcllem  22540  pm2mpmhmlem2  22641  chfacfscmulgsum  22682  chfacfpmmulgsum  22686  neitr  23004  1stcrest  23277  dissnref  23352  dissnlocfin  23353  neitx  23431  tgqtop  23536  ptcmplem3  23878  trust  24054  utoptop  24059  restutopopn  24063  ustuqtop2  24067  ustuqtop4  24069  utop3cls  24076  met1stc  24350  prdsxmslem2  24358  metustexhalf  24385  cfilucfil  24388  metucn  24400  aannenlem1  26180  ulmuni  26243  lgamucov  26884  2sqmo  27284  pntpbnd  27435  pntlem3  27456  noetasuplem4  27583  noetainflem4  27587  tgbtwndiff  28191  tgifscgr  28193  iscgrglt  28199  tgbtwnconn1lem3  28259  tgbtwnconn1  28260  legov  28270  legtrd  28274  legtri3  28275  ltgseg  28281  legso  28284  tglinethru  28321  tglnpt2  28326  colline  28334  miriso  28355  midexlem  28377  perpneq  28399  isperp2  28400  footexALT  28403  footex  28406  midex  28422  opphllem3  28434  opphl  28439  hlpasch  28441  lnopp2hpgb  28448  lmieu  28469  trgcopyeu  28491  dfcgra2  28515  f1otrg  28556  axcontlem2  28657  2pthon3v  29631  2ndresdju  32308  fnpreimac  32330  fsumiunle  32469  ressprs  32567  dfmgc2  32600  mgcf1o  32607  omndmul2  32667  tocyccntz  32740  cyc3genpm  32748  cycpmconjs  32752  cyc3conja  32753  isarchi3  32770  isdrng4  32832  isarchiofld  32872  imaslmod  32905  dvdsruasso  32931  nsgqusf1olem1  32965  nsgqusf1olem3  32967  ghmquskerlem3  32972  lmhmqusker  32975  intlidl  32977  rhmquskerlem  32984  elrspunidl  32987  elrspunsn  32988  idlinsubrg  32990  rhmimaidl  32991  drngidl  32992  isprmidlc  33007  rhmpreimaprmidl  33011  qsidomlem2  33013  mxidlprm  33027  mxidlirredi  33028  ssmxidllem  33030  ssmxidl  33031  opprqusplusg  33044  opprqusmulr  33046  qsdrngi  33050  qsdrng  33052  r1plmhm  33122  r1pquslmic  33123  lbsdiflsp0  33166  dimkerim  33167  fedgmul  33171  ist0cld  33278  txomap  33279  qtophaus  33281  zarcls1  33314  zarclsint  33317  zarclssn  33318  pstmxmet  33342  sqsscirc1  33353  lmxrge0  33397  esumcst  33526  esumfsup  33533  esum2dlem  33555  esum2d  33556  esumiun  33557  ldsysgenld  33623  sigapildsys  33625  omssubadd  33764  signstfvneq0  34048  actfunsnf1o  34081  afsval  34148  nn0prpwlem  35673  lindsenlbs  36949  matunitlindflem1  36950  matunitlindflem2  36951  mblfinlem3  36993  itg2addnclem  37005  sstotbnd2  37108  prdstotbnd  37128  lcfl8  40839  fldhmf1  41424  aks6d1c2p2  41426  dffltz  41841  flt4lem7  41866  nna4b4nsq  41867  diophren  42016  rencldnfilem  42023  pellex  42038  pell1234qrdich  42064  pell1qrgap  42077  pellfundex  42089  omabs2  42547  iunconnlem2  44161  suplesup  44510  infleinflem2  44542  xrralrecnnle  44554  rexabslelem  44589  limcrecl  44806  limcleqr  44821  0ellimcdiv  44826  limclner  44828  limsupubuz  44890  limsupvaluz2  44915  supcnvlimsup  44917  climxrre  44927  xlimmnfvlem2  45010  xlimmnfv  45011  xlimpnfvlem2  45014  xlimpnfv  45015  icccncfext  45064  ioodvbdlimc1lem2  45109  ioodvbdlimc2lem  45111  fourierdlem50  45333  fourierdlem51  45334  fourierdlem80  45363  fourierdlem87  45370  fourierdlem103  45386  fourierdlem104  45387  meaiuninc3v  45661  omef  45673  smflimlem2  45949  smflimlem4  45951  smfmullem3  45970  fsupdm  46019  finfdm  46023