Theorem simp-4r 782

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 731	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 206  df-an 397

This theorem is referenced by:  fimaproj  8123  tfrlem1  8378  injresinj  13757  swrdccatin1  14679  reuccatpfxs1  14701  prdsval  17405  catcocl  17633  catass  17634  catpropd  17657  cidpropd  17658  monpropd  17688  subccocl  17799  funcco  17825  funcpropd  17855  fucpropd  17934  initoeu2lem1  17968  xpcpropd  18165  curf2ndf  18204  drsdirfi  18262  mhmmnd  18983  gsmsymgreqlem2  19340  dfod2  19473  ghmcmn  19740  psgndif  21374  mhpmulcl  21911  dmatscmcl  22225  smatvscl  22246  cpmatmcllem  22440  pm2mpmhmlem2  22541  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  neitr  22904  1stcrest  23177  dissnref  23252  dissnlocfin  23253  neitx  23331  tgqtop  23436  ptcmplem3  23778  trust  23954  utoptop  23959  restutopopn  23963  ustuqtop2  23967  ustuqtop4  23969  utop3cls  23976  met1stc  24250  prdsxmslem2  24258  metustexhalf  24285  cfilucfil  24288  metucn  24300  aannenlem1  26065  ulmuni  26128  lgamucov  26766  2sqmo  27164  pntpbnd  27315  pntlem3  27336  noetasuplem4  27463  noetainflem4  27467  tgbtwndiff  28012  tgifscgr  28014  iscgrglt  28020  tgbtwnconn1lem3  28080  tgbtwnconn1  28081  legov  28091  legtrd  28095  legtri3  28096  ltgseg  28102  legso  28105  tglinethru  28142  tglnpt2  28147  colline  28155  miriso  28176  midexlem  28198  perpneq  28220  isperp2  28221  footexALT  28224  footex  28227  midex  28243  opphllem3  28255  opphl  28260  hlpasch  28262  lnopp2hpgb  28269  lmieu  28290  trgcopyeu  28312  dfcgra2  28336  f1otrg  28377  axcontlem2  28478  2pthon3v  29452  2ndresdju  32129  fnpreimac  32151  fsumiunle  32290  ressprs  32388  dfmgc2  32421  mgcf1o  32428  omndmul2  32488  tocyccntz  32561  cyc3genpm  32569  cycpmconjs  32573  cyc3conja  32574  isarchi3  32591  isdrng4  32653  isarchiofld  32693  imaslmod  32726  dvdsruasso  32752  nsgqusf1olem1  32786  nsgqusf1olem3  32788  ghmquskerlem3  32793  lmhmqusker  32796  intlidl  32798  rhmquskerlem  32805  elrspunidl  32808  elrspunsn  32809  idlinsubrg  32811  rhmimaidl  32812  drngidl  32813  isprmidlc  32828  rhmpreimaprmidl  32832  qsidomlem2  32834  mxidlprm  32848  mxidlirredi  32849  ssmxidllem  32851  ssmxidl  32852  opprqusplusg  32865  opprqusmulr  32867  qsdrngi  32871  qsdrng  32873  r1plmhm  32943  r1pquslmic  32944  lbsdiflsp0  32987  dimkerim  32988  fedgmul  32992  ist0cld  33099  txomap  33100  qtophaus  33102  zarcls1  33135  zarclsint  33138  zarclssn  33139  pstmxmet  33163  sqsscirc1  33174  lmxrge0  33218  esumcst  33347  esumfsup  33354  esum2dlem  33376  esum2d  33377  esumiun  33378  ldsysgenld  33444  sigapildsys  33446  omssubadd  33585  signstfvneq0  33869  actfunsnf1o  33902  afsval  33969  nn0prpwlem  35510  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  mblfinlem3  36830  itg2addnclem  36842  sstotbnd2  36945  prdstotbnd  36965  lcfl8  40676  fldhmf1  41261  aks6d1c2p2  41263  dffltz  41678  flt4lem7  41703  nna4b4nsq  41704  diophren  41853  rencldnfilem  41860  pellex  41875  pell1234qrdich  41901  pell1qrgap  41914  pellfundex  41926  omabs2  42384  iunconnlem2  43998  suplesup  44348  infleinflem2  44380  xrralrecnnle  44392  rexabslelem  44427  limcrecl  44644  limcleqr  44659  0ellimcdiv  44664  limclner  44666  limsupubuz  44728  limsupvaluz2  44753  supcnvlimsup  44755  climxrre  44765  xlimmnfvlem2  44848  xlimmnfv  44849  xlimpnfvlem2  44852  xlimpnfv  44853  icccncfext  44902  ioodvbdlimc1lem2  44947  ioodvbdlimc2lem  44949  fourierdlem50  45171  fourierdlem51  45172  fourierdlem80  45201  fourierdlem87  45208  fourierdlem103  45224  fourierdlem104  45225  meaiuninc3v  45499  omef  45511  smflimlem2  45787  smflimlem4  45789  smfmullem3  45808  fsupdm  45857  finfdm  45861