Theorem simp-4r 796

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fimaproj  8137  tfrlem1  8368  injresinj  13851  swrdccatin1  14798  reuccatpfxs1  14820  prdsval  17546  catcocl  17779  catass  17780  catpropd  17803  cidpropd  17804  monpropd  17832  subccocl  17940  funcco  17966  funcpropd  17997  fucpropd  18075  initoeu2lem1  18109  xpcpropd  18302  curf2ndf  18341  drsdirfi  18399  chnind  18715  chnub  18716  chnso  18718  mhmmnd  19193  ghmqusnsg  19415  ghmquskerlem3  19419  gsmsymgreqlem2  19564  dfod2  19697  ghmcmn  19964  omndmul2  20266  isdrng4  20908  drngidl  21454  rhmqusnsg  21494  isprmidlc  21541  rhmpreimaprmidl  21548  qsidomlem2  21550  ssdifidllem  21553  ssdifidlprm  21555  psgndif  21821  lindsenlbs  22070  dmatscmcl  22731  smatvscl  22752  matunitlindflem1  22907  matunitlindflem2  22908  cpmatmcllem  22949  pm2mpmhmlem2  23050  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  neitr  23411  1stcrest  23684  dissnref  23760  dissnlocfin  23761  neitx  23839  tgqtop  23944  ptcmplem3  24286  trust  24461  utoptop  24466  restutopopn  24470  ustuqtop2  24474  ustuqtop4  24476  utop3cls  24483  met1stc  24753  prdsxmslem2  24761  metustexhalf  24788  cfilucfil  24791  metucn  24803  aannenlem1  26571  ulmuni  26635  lgamucov  27282  2sqmo  27681  pntpbnd  27832  pntlem3  27853  noetasuplem4  27980  noetainflem4  27984  bdayfinbndlem1  28740  tgsegconeu  28836  tgbtwndiff  28856  tgifscgr  28858  iscgrglt  28864  tgbtwnconn1lem3  28924  tgbtwnconn1  28925  legov  28935  legtrd  28939  legtri3  28940  ltgseg  28946  legso  28949  tglinethru  28991  tglinesseq  28995  colline  29005  tglnpt2  29008  tglnpt4  29010  miriso  29029  midexlem  29051  perpneq  29076  isperp2  29077  footexALT  29080  footex  29083  midex  29100  opphllem3  29112  opphl  29117  hlpasch  29121  lnopp2hpgb  29128  plngcplem  29150  lnssplng  29157  plng3p  29162  lmieu  29176  trgcopyeu  29200  zerocgra  29218  dfcgra2  29225  ragcgra  29230  cgrarag  29231  ragsupplcgra  29232  tgaaddcpbllem1  29236  cgraer  29264  cgrabasimass  29265  angmgmaddeu1  29266  angmgmaddeu2  29267  angmgmaddeu3  29268  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  prlnghpg  29311  dfprlng2  29312  dfprlng3  29313  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  quadcgrprlng  29331  f1otrg  29335  axcontlem2  29430  2pthon3v  30419  2ndresdju  33130  fnpreimac  33151  fsumiunle  33307  ressprs  33414  dfmgc2  33444  mgcf1o  33451  mndlrinvb  33473  mndlactf1o  33478  gsumfs2d  33509  gsumwun  33524  gsumwrd2dccatlem  33525  tocyccntz  33592  cyc3genpm  33600  cycpmconjs  33604  cyc3conja  33605  isarchi3  33635  isarchiofld  33647  elrgspnlem4  33693  erler  33713  elrlocbasi  33715  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rlocf1  33722  rlocisunit  33724  ricdomn1  33737  fracfld  33757  imaslmod  33801  dvdsruasso  33826  nsgqusf1olem1  33850  nsgqusf1olem3  33852  lmhmqusker  33854  intlidl  33856  rhmquskerlem  33861  elrspunidl  33864  elrspunsn  33865  idlinsubrg  33867  rhmimaidl  33868  mxidlprm  33881  mxidlirredi  33882  ssmxidllem  33884  ssmxidl  33885  opprqusplusg  33899  opprqusmulr  33901  qsdrngi  33905  qsdrng  33907  drnglring  33910  dflring2  33911  dflringlem3  33914  dflring4  33916  rsprprmprmidlb  33941  rprmdvdsprod  33952  1arithidom  33955  1arithufdlem2  33963  1arithufdlem3  33964  dfufd2lem  33967  r1plmhm  34027  r1pquslmic  34028  mplidomlem  34045  lbsdiflsp0  34144  dimkerim  34145  fedgmul  34149  fldextrspunlsplem  34191  extdgfialg  34212  constrconj  34263  constrfin  34264  constrelextdg2  34265  constrextdg2lem  34266  constrfiss  34269  ist0cld  34351  txomap  34352  qtophaus  34354  zarcls1  34387  zarclsint  34390  zarclssn  34391  pstmxmet  34415  sqsscirc1  34426  lmxrge0  34470  esumcst  34581  esumfsup  34588  esum2dlem  34610  esum2d  34611  esumiun  34612  ldsysgenld  34679  sigapildsys  34681  omssubadd  34819  signstfvneq0  35088  actfunsnf1o  35120  afsval  35190  nn0prpwlem  36949  mblfinlem3  38416  itg2addnclem  38428  sstotbnd2  38532  prdstotbnd  38552  lcfl8  42383  fldhmf1  42964  mndmolinv  42969  primrootscoprmpow  42973  primrootspoweq0  42980  aks6d1c2p2  42993  aks6d1c2lem4  43001  aks6d1c2  43004  aks6d1c5  43013  aks6d1c6lem3  43046  unitscyglem3  43071  fiabv  43426  dffltz  43488  flt4lem7  43513  nna4b4nsq  43514  diophren  43662  rencldnfilem  43669  pellex  43684  pell1234qrdich  43710  pell1qrgap  43723  pellfundex  43735  omabs2  44181  iunconnlem2  45765  modelaxrep  45812  suplesup  46177  infleinflem2  46208  xrralrecnnle  46220  rexabslelem  46254  limcrecl  46467  limcleqr  46480  0ellimcdiv  46485  limclner  46487  limsupubuz  46549  limsupvaluz2  46574  supcnvlimsup  46576  climxrre  46586  xlimmnfvlem2  46669  xlimmnfv  46670  xlimpnfvlem2  46673  xlimpnfv  46674  icccncfext  46723  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  fourierdlem50  46992  fourierdlem51  46993  fourierdlem80  47022  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  meaiuninc3v  47320  omef  47332  smflimlem2  47608  smflimlem4  47610  smfmullem3  47629  fsupdm  47678  finfdm  47682  chnerlem1  47718  imaf1co  50089  upfval  50110  fuco21  50270  prcofvalg  50310