Theorem simp-4r 780

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 729	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  7947  tfrlem1  8178  injresinj  13436  swrdccatin1  14366  reuccatpfxs1  14388  prdsval  17083  catcocl  17311  catass  17312  catpropd  17335  cidpropd  17336  monpropd  17366  subccocl  17476  funcco  17502  funcpropd  17532  fucpropd  17611  initoeu2lem1  17645  xpcpropd  17842  curf2ndf  17881  drsdirfi  17938  mhmmnd  18612  gsmsymgreqlem2  18954  dfod2  19086  ghmcmn  19348  psgndif  20719  mhpmulcl  21249  dmatscmcl  21560  smatvscl  21581  cpmatmcllem  21775  pm2mpmhmlem2  21876  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  neitr  22239  1stcrest  22512  dissnref  22587  dissnlocfin  22588  neitx  22666  tgqtop  22771  ptcmplem3  23113  trust  23289  utoptop  23294  restutopopn  23298  ustuqtop2  23302  ustuqtop4  23304  utop3cls  23311  met1stc  23583  prdsxmslem2  23591  metustexhalf  23618  cfilucfil  23621  metucn  23633  aannenlem1  25393  ulmuni  25456  lgamucov  26092  2sqmo  26490  pntpbnd  26641  pntlem3  26662  istrkgb  26720  tgbtwndiff  26771  tgifscgr  26773  iscgrglt  26779  tgbtwnconn1lem3  26839  tgbtwnconn1  26840  legov  26850  legtrd  26854  legtri3  26855  ltgseg  26861  legso  26864  tglinethru  26901  tglnpt2  26906  colline  26914  miriso  26935  midexlem  26957  perpneq  26979  isperp2  26980  footexALT  26983  footex  26986  midex  27002  opphllem3  27014  opphl  27019  hlpasch  27021  lnopp2hpgb  27028  lmieu  27049  trgcopyeu  27071  dfcgra2  27095  f1otrg  27136  axcontlem2  27236  2pthon3v  28209  2ndresdju  30887  fnpreimac  30910  fsumiunle  31045  ressprs  31143  dfmgc2  31176  mgcf1o  31183  omndmul2  31240  tocyccntz  31313  cyc3genpm  31321  cycpmconjs  31325  cyc3conja  31326  isarchi3  31343  isarchiofld  31418  imaslmod  31455  nsgqusf1olem1  31500  nsgqusf1olem3  31502  intlidl  31504  elrspunidl  31508  idlinsubrg  31510  rhmimaidl  31511  isprmidlc  31525  rhmpreimaprmidl  31529  qsidomlem2  31531  mxidlprm  31542  ssmxidllem  31543  ssmxidl  31544  lbsdiflsp0  31609  dimkerim  31610  fedgmul  31614  ist0cld  31685  txomap  31686  qtophaus  31688  zarcls1  31721  zarclsint  31724  zarclssn  31725  pstmxmet  31749  sqsscirc1  31760  lmxrge0  31804  esumcst  31931  esumfsup  31938  esum2dlem  31960  esum2d  31961  esumiun  31962  ldsysgenld  32028  sigapildsys  32030  omssubadd  32167  signstfvneq0  32451  actfunsnf1o  32484  afsval  32551  noetasuplem4  33866  noetainflem4  33870  nn0prpwlem  34438  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  mblfinlem3  35743  itg2addnclem  35755  sstotbnd2  35859  prdstotbnd  35879  lcfl8  39443  dffltz  40387  flt4lem7  40412  nna4b4nsq  40413  diophren  40551  rencldnfilem  40558  pellex  40573  pell1234qrdich  40599  pell1qrgap  40612  pellfundex  40624  iunconnlem2  42444  suplesup  42768  infleinflem2  42800  xrralrecnnle  42812  rexabslelem  42848  limcrecl  43060  limcleqr  43075  0ellimcdiv  43080  limclner  43082  limsupubuz  43144  limsupvaluz2  43169  supcnvlimsup  43171  climxrre  43181  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  icccncfext  43318  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  fourierdlem50  43587  fourierdlem51  43588  fourierdlem80  43617  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  meaiuninc3v  43912  omef  43924  smflimlem2  44194  smflimlem4  44196  smfmullem3  44214