Theorem simp-4r 793

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fimaproj  8110  tfrlem1  8341  injresinj  13794  swrdccatin1  14735  reuccatpfxs1  14757  prdsval  17467  catcocl  17700  catass  17701  catpropd  17724  cidpropd  17725  monpropd  17753  subccocl  17861  funcco  17887  funcpropd  17918  fucpropd  17996  initoeu2lem1  18030  xpcpropd  18223  curf2ndf  18262  drsdirfi  18320  chnind  18636  chnub  18637  chnso  18639  mhmmnd  19089  ghmqusnsg  19305  ghmquskerlem3  19309  gsmsymgreqlem2  19454  dfod2  19587  ghmcmn  19854  omndmul2  20156  rhmqusnsg  21335  psgndif  21634  dmatscmcl  22543  smatvscl  22564  cpmatmcllem  22758  pm2mpmhmlem2  22859  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  neitr  23220  1stcrest  23493  dissnref  23568  dissnlocfin  23569  neitx  23647  tgqtop  23752  ptcmplem3  24094  trust  24269  utoptop  24274  restutopopn  24278  ustuqtop2  24282  ustuqtop4  24284  utop3cls  24291  met1stc  24561  prdsxmslem2  24569  metustexhalf  24596  cfilucfil  24599  metucn  24611  aannenlem1  26369  ulmuni  26432  lgamucov  27079  2sqmo  27478  pntpbnd  27629  pntlem3  27650  noetasuplem4  27777  noetainflem4  27781  bdayfinbndlem1  28537  tgbtwndiff  28652  tgifscgr  28654  iscgrglt  28660  tgbtwnconn1lem3  28720  tgbtwnconn1  28721  legov  28731  legtrd  28735  legtri3  28736  ltgseg  28742  legso  28745  tglinethru  28782  tglnpt2  28787  colline  28795  miriso  28816  midexlem  28838  perpneq  28860  isperp2  28861  footexALT  28864  footex  28867  midex  28883  opphllem3  28895  opphl  28900  hlpasch  28902  lnopp2hpgb  28909  lmieu  28930  trgcopyeu  28952  dfcgra2  28976  f1otrg  29017  axcontlem2  29112  2pthon3v  30089  2ndresdju  32801  fnpreimac  32822  fsumiunle  32981  ressprs  33105  dfmgc2  33135  mgcf1o  33142  mndlrinvb  33164  mndlactf1o  33169  gsumfs2d  33202  gsumwun  33217  gsumwrd2dccatlem  33218  tocyccntz  33285  cyc3genpm  33293  cycpmconjs  33297  cyc3conja  33298  isarchi3  33328  isarchiofld  33340  elrgspnlem4  33387  erler  33407  elrlocbasi  33409  rlocaddval  33411  rlocmulval  33412  rloccring  33413  rlocf1  33416  rlocisunit  33418  ricdomn1  33434  isdrng4  33443  fracfld  33456  imaslmod  33500  dvdsruasso  33532  nsgqusf1olem1  33560  nsgqusf1olem3  33562  lmhmqusker  33564  intlidl  33567  rhmquskerlem  33572  elrspunidl  33575  elrspunsn  33576  idlinsubrg  33578  rhmimaidl  33579  drngidl  33580  isprmidlc  33594  rhmpreimaprmidl  33599  qsidomlem2  33601  ssdifidllem  33604  ssdifidlprm  33606  mxidlprm  33619  mxidlirredi  33620  ssmxidllem  33622  ssmxidl  33623  opprqusplusg  33638  opprqusmulr  33640  qsdrngi  33644  qsdrng  33646  drnglring  33649  dflring2  33650  dflringlem3  33653  dflring4  33655  rsprprmprmidlb  33680  rprmdvdsprod  33691  1arithidom  33694  1arithufdlem2  33702  1arithufdlem3  33703  dfufd2lem  33706  r1plmhm  33767  r1pquslmic  33768  mplidomlem  33785  lbsdiflsp0  33884  dimkerim  33885  fedgmul  33889  fldextrspunlsplem  33931  extdgfialg  33952  constrconj  34003  constrfin  34004  constrelextdg2  34005  constrextdg2lem  34006  constrfiss  34009  ist0cld  34091  txomap  34092  qtophaus  34094  zarcls1  34127  zarclsint  34130  zarclssn  34131  pstmxmet  34155  sqsscirc1  34166  lmxrge0  34210  esumcst  34321  esumfsup  34328  esum2dlem  34350  esum2d  34351  esumiun  34352  ldsysgenld  34418  sigapildsys  34420  omssubadd  34558  signstfvneq0  34830  actfunsnf1o  34862  afsval  34932  nn0prpwlem  36646  lindsenlbs  38078  matunitlindflem1  38079  matunitlindflem2  38080  mblfinlem3  38122  itg2addnclem  38134  sstotbnd2  38237  prdstotbnd  38257  lcfl8  42090  fldhmf1  42671  mndmolinv  42676  primrootscoprmpow  42680  primrootspoweq0  42687  aks6d1c2p2  42700  aks6d1c2lem4  42708  aks6d1c2  42711  aks6d1c5  42720  aks6d1c6lem3  42753  unitscyglem3  42778  fiabv  43118  dffltz  43180  flt4lem7  43205  nna4b4nsq  43206  diophren  43354  rencldnfilem  43361  pellex  43376  pell1234qrdich  43402  pell1qrgap  43415  pellfundex  43427  omabs2  43873  iunconnlem2  45474  modelaxrep  45521  suplesup  45879  infleinflem2  45910  xrralrecnnle  45922  rexabslelem  45956  limcrecl  46169  limcleqr  46182  0ellimcdiv  46187  limclner  46189  limsupubuz  46251  limsupvaluz2  46276  supcnvlimsup  46278  climxrre  46288  xlimmnfvlem2  46371  xlimmnfv  46372  xlimpnfvlem2  46375  xlimpnfv  46376  icccncfext  46425  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  fourierdlem50  46694  fourierdlem51  46695  fourierdlem80  46724  fourierdlem87  46731  fourierdlem103  46747  fourierdlem104  46748  meaiuninc3v  47022  omef  47034  smflimlem2  47310  smflimlem4  47312  smfmullem3  47331  fsupdm  47380  finfdm  47384  chnerlem1  47422  imaf1co  49740  upfval  49761  fuco21  49921  prcofvalg  49961