Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-4r Structured version   Visualization version   GIF version

Theorem simp-4r 783
 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
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad4antlr 732 1 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
 Colors of variables: wff setvar class 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 210  df-an 400 This theorem is referenced by:  fimaproj  7814  tfrlem1  7997  injresinj  13155  swrdccatin1  14080  reuccatpfxs1  14102  prdsval  16722  catcocl  16950  catass  16951  catpropd  16973  cidpropd  16974  monpropd  17001  subccocl  17109  funcco  17135  funcpropd  17164  fucpropd  17241  initoeu2lem1  17268  xpcpropd  17452  curf2ndf  17491  drsdirfi  17542  mhmmnd  18216  gsmsymgreqlem2  18554  dfod2  18686  ghmcmn  18948  psgndif  20295  mhpmulcl  20805  dmatscmcl  21115  smatvscl  21136  cpmatmcllem  21330  pm2mpmhmlem2  21431  chfacfscmulgsum  21472  chfacfpmmulgsum  21476  neitr  21792  1stcrest  22065  dissnref  22140  dissnlocfin  22141  neitx  22219  tgqtop  22324  ptcmplem3  22666  trust  22842  utoptop  22847  restutopopn  22851  ustuqtop2  22855  ustuqtop4  22857  utop3cls  22864  met1stc  23135  prdsxmslem2  23143  metustexhalf  23170  cfilucfil  23173  metucn  23185  aannenlem1  24931  ulmuni  24994  lgamucov  25630  2sqmo  26028  pntpbnd  26179  pntlem3  26200  istrkgb  26256  tgbtwndiff  26307  tgifscgr  26309  iscgrglt  26315  tgbtwnconn1lem3  26375  tgbtwnconn1  26376  legov  26386  legtrd  26390  legtri3  26391  ltgseg  26397  legso  26400  tglinethru  26437  tglnpt2  26442  colline  26450  miriso  26471  midexlem  26493  perpneq  26515  isperp2  26516  footexALT  26519  footex  26522  midex  26538  opphllem3  26550  opphl  26555  hlpasch  26557  lnopp2hpgb  26564  lmieu  26585  trgcopyeu  26607  dfcgra2  26631  f1otrg  26672  axcontlem2  26766  2pthon3v  27736  2ndresdju  30418  fnpreimac  30441  fsumiunle  30578  ressprs  30675  dfmgc2  30711  omndmul2  30770  tocyccntz  30843  cyc3genpm  30851  cycpmconjs  30855  cyc3conja  30856  isarchi3  30873  isarchiofld  30948  imaslmod  30980  intlidl  31017  elrspunidl  31021  idlinsubrg  31023  rhmimaidl  31024  isprmidlc  31038  rhmpreimaprmidl  31042  qsidomlem2  31044  mxidlprm  31055  ssmxidllem  31056  ssmxidl  31057  lbsdiflsp0  31122  dimkerim  31123  fedgmul  31127  ist0cld  31198  txomap  31199  qtophaus  31201  zarcls1  31234  zarclsint  31237  zarclssn  31238  pstmxmet  31262  sqsscirc1  31273  lmxrge0  31317  esumcst  31444  esumfsup  31451  esum2dlem  31473  esum2d  31474  esumiun  31475  ldsysgenld  31541  sigapildsys  31543  omssubadd  31680  signstfvneq0  31964  actfunsnf1o  31997  afsval  32064  noetalem3  33344  nn0prpwlem  33795  lindsenlbs  35068  matunitlindflem1  35069  matunitlindflem2  35070  mblfinlem3  35112  itg2addnclem  35124  sstotbnd2  35228  prdstotbnd  35248  lcfl8  38814  dffltz  39630  diophren  39769  rencldnfilem  39776  pellex  39791  pell1234qrdich  39817  pell1qrgap  39830  pellfundex  39842  iunconnlem2  41656  suplesup  41986  infleinflem2  42018  xrralrecnnle  42032  rexabslelem  42070  limcrecl  42286  limcleqr  42301  0ellimcdiv  42306  limclner  42308  limsupubuz  42370  limsupvaluz2  42395  supcnvlimsup  42397  climxrre  42407  xlimmnfvlem2  42490  xlimmnfv  42491  xlimpnfvlem2  42494  xlimpnfv  42495  icccncfext  42544  ioodvbdlimc1lem2  42589  ioodvbdlimc2lem  42591  fourierdlem50  42813  fourierdlem51  42814  fourierdlem80  42843  fourierdlem87  42850  fourierdlem103  42866  fourierdlem104  42867  meaiuninc3v  43138  omef  43150  smflimlem2  43420  smflimlem4  43422  smfmullem3  43440
 Copyright terms: Public domain W3C validator