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  8140  tfrlem1  8371  injresinj  13839  swrdccatin1  14786  reuccatpfxs1  14808  prdsval  17533  catcocl  17766  catass  17767  catpropd  17790  cidpropd  17791  monpropd  17819  subccocl  17927  funcco  17953  funcpropd  17984  fucpropd  18062  initoeu2lem1  18096  xpcpropd  18289  curf2ndf  18328  drsdirfi  18386  chnind  18702  chnub  18703  chnso  18705  mhmmnd  19161  ghmqusnsg  19383  ghmquskerlem3  19387  gsmsymgreqlem2  19532  dfod2  19665  ghmcmn  19932  omndmul2  20234  isdrng4  20876  drngidl  21422  rhmqusnsg  21462  isprmidlc  21509  rhmpreimaprmidl  21516  qsidomlem2  21518  ssdifidllem  21521  ssdifidlprm  21523  psgndif  21789  dmatscmcl  22697  smatvscl  22718  cpmatmcllem  22912  pm2mpmhmlem2  23013  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  neitr  23374  1stcrest  23647  dissnref  23722  dissnlocfin  23723  neitx  23801  tgqtop  23906  ptcmplem3  24248  trust  24423  utoptop  24428  restutopopn  24432  ustuqtop2  24436  ustuqtop4  24438  utop3cls  24445  met1stc  24715  prdsxmslem2  24723  metustexhalf  24750  cfilucfil  24753  metucn  24765  aannenlem1  26528  ulmuni  26592  lgamucov  27239  2sqmo  27638  pntpbnd  27789  pntlem3  27810  noetasuplem4  27937  noetainflem4  27941  bdayfinbndlem1  28697  tgbtwndiff  28812  tgifscgr  28814  iscgrglt  28820  tgbtwnconn1lem3  28880  tgbtwnconn1  28881  legov  28891  legtrd  28895  legtri3  28896  ltgseg  28902  legso  28905  tglinethru  28946  tglinesseq  28950  colline  28960  tglnpt2  28963  tglnpt4  28965  miriso  28984  midexlem  29006  perpneq  29031  isperp2  29032  footexALT  29035  footex  29038  midex  29055  opphllem3  29067  opphl  29072  hlpasch  29075  lnopp2hpgb  29082  plngcplem  29104  lnssplng  29111  plng3p  29116  lmieu  29130  trgcopyeu  29154  dfcgra2  29178  ragcgra  29183  cgrarag  29184  ragsupplcgra  29185  prlnghpg  29233  dfprlng2  29234  dfprlng3  29235  perpprlng  29237  prlngex  29238  prlngmolem1  29239  prlngmolem2  29240  quadcgrprlng  29253  f1otrg  29257  axcontlem2  29352  2pthon3v  30329  2ndresdju  33031  fnpreimac  33052  fsumiunle  33210  ressprs  33317  dfmgc2  33347  mgcf1o  33354  mndlrinvb  33376  mndlactf1o  33381  gsumfs2d  33412  gsumwun  33427  gsumwrd2dccatlem  33428  tocyccntz  33495  cyc3genpm  33503  cycpmconjs  33507  cyc3conja  33508  isarchi3  33538  isarchiofld  33550  elrgspnlem4  33596  erler  33616  elrlocbasi  33618  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rlocf1  33625  rlocisunit  33627  ricdomn1  33640  fracfld  33660  imaslmod  33704  dvdsruasso  33729  nsgqusf1olem1  33753  nsgqusf1olem3  33755  lmhmqusker  33757  intlidl  33759  rhmquskerlem  33764  elrspunidl  33767  elrspunsn  33768  idlinsubrg  33770  rhmimaidl  33771  mxidlprm  33784  mxidlirredi  33785  ssmxidllem  33787  ssmxidl  33788  opprqusplusg  33802  opprqusmulr  33804  qsdrngi  33808  qsdrng  33810  drnglring  33813  dflring2  33814  dflringlem3  33817  dflring4  33819  rsprprmprmidlb  33844  rprmdvdsprod  33855  1arithidom  33858  1arithufdlem2  33866  1arithufdlem3  33867  dfufd2lem  33870  r1plmhm  33930  r1pquslmic  33931  mplidomlem  33948  lbsdiflsp0  34047  dimkerim  34048  fedgmul  34052  fldextrspunlsplem  34094  extdgfialg  34115  constrconj  34166  constrfin  34167  constrelextdg2  34168  constrextdg2lem  34169  constrfiss  34172  ist0cld  34254  txomap  34255  qtophaus  34257  zarcls1  34290  zarclsint  34293  zarclssn  34294  pstmxmet  34318  sqsscirc1  34329  lmxrge0  34373  esumcst  34484  esumfsup  34491  esum2dlem  34513  esum2d  34514  esumiun  34515  ldsysgenld  34582  sigapildsys  34584  omssubadd  34722  signstfvneq0  34991  actfunsnf1o  35023  afsval  35093  nn0prpwlem  36874  lindsenlbs  38307  matunitlindflem1  38308  matunitlindflem2  38309  mblfinlem3  38351  itg2addnclem  38363  sstotbnd2  38466  prdstotbnd  38486  lcfl8  42317  fldhmf1  42898  mndmolinv  42903  primrootscoprmpow  42907  primrootspoweq0  42914  aks6d1c2p2  42927  aks6d1c2lem4  42935  aks6d1c2  42938  aks6d1c5  42947  aks6d1c6lem3  42980  unitscyglem3  43005  fiabv  43345  dffltz  43407  flt4lem7  43432  nna4b4nsq  43433  diophren  43581  rencldnfilem  43588  pellex  43603  pell1234qrdich  43629  pell1qrgap  43642  pellfundex  43654  omabs2  44100  iunconnlem2  45684  modelaxrep  45731  suplesup  46096  infleinflem2  46127  xrralrecnnle  46139  rexabslelem  46173  limcrecl  46386  limcleqr  46399  0ellimcdiv  46404  limclner  46406  limsupubuz  46468  limsupvaluz2  46493  supcnvlimsup  46495  climxrre  46505  xlimmnfvlem2  46588  xlimmnfv  46589  xlimpnfvlem2  46592  xlimpnfv  46593  icccncfext  46642  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  fourierdlem50  46911  fourierdlem51  46912  fourierdlem80  46941  fourierdlem87  46948  fourierdlem103  46964  fourierdlem104  46965  meaiuninc3v  47239  omef  47251  smflimlem2  47527  smflimlem4  47529  smfmullem3  47548  fsupdm  47597  finfdm  47601  chnerlem1  47639  imaf1co  49974  upfval  49995  fuco21  50155  prcofvalg  50195