MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpllr Structured version   Visualization version   GIF version

Theorem simpllr 815
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)
Assertion
Ref Expression
simpllr ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad3antlr 767 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  simp-4r  824  fsnex  6578  soisoi  6618  f1o2ndf1  7330  tz7.49  7585  omabs  7772  omxpenlem  8102  fopwdom  8109  findcard3  8244  frfi  8246  finsschain  8314  marypha1lem  8380  wdomtr  8521  cantnfp1  8616  harcard  8842  numacn  8910  infunsdom1  9073  cofsmo  9129  sornom  9137  ssfin4  9170  fin1a2lem11  9270  fin1a2lem13  9272  ttukeylem5  9373  fpwwe2lem13  9502  pwfseq  9524  mulcmpblnr  9930  00id  10249  addid1  10254  cnegex  10255  negeu  10309  add20  10578  ltmul12a  10917  lediv12a  10954  fiminre  11010  cru  11050  qextltlem  12071  xleadd1a  12121  xmullem  12132  xlemul1a  12156  ixxss12  12233  ioodisj  12340  fsuppmapnn0fz  12836  seqf1o  12882  mulexpz  12940  leexp1a  12959  faclbnd  13117  swrdswrdlem  13505  abs3lem  14122  cau3lem  14138  rlim3  14273  ello12  14291  lo1bdd2  14299  elo12  14302  rlimconst  14319  isercoll  14442  climcau  14445  climbdd  14446  summolem2  14491  fsumconst  14566  o1fsum  14589  incexclem  14612  fprodconst  14752  bitsfzo  15204  dvdsmulgcd  15321  pc2dvds  15630  pcz  15632  pcadd  15640  pcfac  15650  vdwmc2  15730  vdwlem2  15733  vdwlem10  15741  vdw  15745  ramcl  15780  sbcie3s  15964  firest  16140  prdsval  16162  mreexd  16349  mreexexlemd  16351  iscat  16380  cidfval  16384  iscatd2  16389  catcocl  16393  catass  16394  catpropd  16416  cidpropd  16417  moni  16443  monpropd  16444  issubc  16542  subccocl  16552  funcco  16578  funcpropd  16607  fullpropd  16627  nati  16662  natpropd  16683  fucpropd  16684  xpcpropd  16895  curfuncf  16925  curf2ndf  16934  yonffthlem  16969  acsfiindd  17224  mndpropd  17363  mhmeql  17411  isgrpinv  17519  dfgrp3lem  17560  mhmmnd  17584  conjnmzb  17742  gass  17780  symgextf  17883  dfod2  18027  gexdvds  18045  sylow3lem2  18089  efgredlem  18206  efgredeu  18211  ghmcmn  18283  oddvdssubg  18304  dprdfcntz  18460  pgpfaclem3  18528  issrg  18553  isring  18597  dvdsrmul1  18699  issubdrg  18853  islmhm2  19086  lmhmeql  19103  lssacsex  19192  issubassa2  19393  opsrval  19522  isphl  20021  uvcf1  20179  lindfmm  20214  scmatmats  20365  smatvscl  20378  mdetunilem7  20472  gsummatr01lem4  20512  m2cpmfo  20609  decpmatmulsumfsupp  20626  pmatcollpw3fi1lem1  20639  pm2mpf1lem  20647  pm2mpf1  20652  mp2pm2mplem4  20662  pm2mpghm  20669  pm2mpmhmlem1  20671  pm2mpmhmlem2  20672  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  cctop  20858  neiptoptop  20983  neiptopreu  20985  tgrest  21011  ordtrest2lem  21055  cnss1  21128  cncnp  21132  isnrm3  21211  uncmp  21254  cmpfi  21259  iunconn  21279  1stcrest  21304  subislly  21332  islly2  21335  cldllycmp  21346  lly1stc  21347  llycmpkgen2  21401  kgencn  21407  xkoccn  21470  ptcnplem  21472  pthaus  21489  txhaus  21498  txkgen  21503  xkohaus  21504  xkococnlem  21510  txconn  21540  regr1lem2  21591  kqreglem1  21592  reghmph  21644  nrmhmph  21645  trfil2  21738  ufileu  21770  flimopn  21826  flimcf  21833  fclscf  21876  ufilcmp  21883  cnpfcf  21892  cnextfun  21915  tgpmulg  21944  symgtgp  21952  tgpt0  21969  qustgplem  21971  ustex2sym  22067  ustex3sym  22068  trust  22080  restutop  22088  restutopopn  22089  ustuqtop2  22093  ustuqtop4  22095  utop3cls  22102  utopreg  22103  cstucnd  22135  ucncn  22136  trcfilu  22145  neipcfilu  22147  ismet2  22185  metequiv2  22362  metcnp  22393  metcnp2  22394  metcnpi3  22398  txmetcnp  22399  metustto  22405  metustsym  22407  metust  22410  cfilucfil  22411  metuel2  22417  psmetutop  22419  restmetu  22422  metucn  22423  ngptgp  22487  tngngp  22505  nmoleub  22582  icccmp  22675  reconnlem2  22677  reconn  22678  xmetdcn2  22687  metdseq0  22704  metdscn  22706  elcncf2  22740  cncfmet  22758  cnheibor  22801  nmoleub2lem2  22962  nmoleub3  22965  cvsi  22976  iscfil2  23110  iscfil3  23117  cfilfcls  23118  equivcfil  23143  caubl  23152  bcthlem5  23171  pmltpc  23265  ovollb2  23303  ovoliunnul  23321  ovolicc2lem4  23334  volsup  23370  ioorf  23387  dyadss  23408  dyaddisjlem  23409  mbfposr  23464  cncombf  23470  mbflimsup  23478  i1fmulclem  23514  mbfi1fseqlem4  23530  iblss2  23617  ellimc2  23686  ellimc3  23688  dvnadd  23737  dvmptfsum  23783  dvferm1  23793  dvferm2  23795  fta1g  23972  plyeq0lem  24011  plydivex  24097  fta1  24108  aalioulem2  24133  aalioulem3  24134  ulmuni  24191  ulmbdd  24197  ulmdvlem3  24201  mtest  24203  abelthlem8  24238  pilem3  24252  efopn  24449  cxpmul2z  24482  cxpcn3lem  24533  jensen  24760  lgambdd  24808  lgamucov  24809  isppw2  24886  sqf11  24910  mersenne  24997  dchrelbas3  25008  dchrptlem1  25034  dchrpt  25037  lgsval2lem  25077  lgsdchrval  25124  lgsquad3  25157  2sqb  25202  pntrsumbnd2  25301  pntpbnd  25322  pntibnd  25327  istrkgc  25398  istrkgb  25399  tglowdim1i  25441  tgbtwndiff  25446  tgifscgr  25448  iscgrglt  25454  tgcgrxfr  25458  lnext  25507  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  legval  25524  legov  25525  legov2  25526  legtrd  25529  legtri3  25530  legso  25539  hlcgrex  25556  hlcgreu  25558  tglnne  25568  tglndim0  25569  tglineeltr  25571  tglinethru  25576  tglnne0  25580  tglnpt2  25581  colline  25589  tglowdim2l  25590  tglowdim2ln  25591  mirreu3  25594  miriso  25610  midexlem  25632  isperp  25652  perpcom  25653  perpneq  25654  isperp2  25655  footex  25658  colperpexlem3  25669  opphllem  25672  midex  25674  oppne3  25680  opptgdim2  25682  opphllem2  25685  opphllem3  25686  opphllem5  25688  opphllem6  25689  opphl  25691  outpasch  25692  lnopp2hpgb  25700  colopp  25706  lmieu  25721  trgcopy  25741  trgcopyeu  25743  iscgra1  25747  cgrane1  25749  cgrane2  25750  cgrane3  25751  cgrahl1  25753  cgrahl2  25754  cgracgr  25755  cgraswap  25757  cgracom  25759  cgratr  25760  cgrabtwn  25762  cgrahl  25763  dfcgra2  25766  sacgr  25767  acopyeu  25770  inaghl  25776  cgrg3col4  25779  f1otrg  25796  f1otrge  25797  axsegcon  25852  axeuclidlem  25887  axcontlem2  25890  upgr1eopALT  26057  usgr1eop  26187  pthdepisspth  26687  wpthswwlks2on  26927  clwwlkf1  27012  clwwlknscsh  27027  2pthfrgr  27264  n4cyclfrgr  27271  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  friendshipgt3  27385  smcnlem  27680  0lno  27773  ubthlem1  27854  ubthlem3  27856  chocunii  28288  occl  28291  5oalem1  28641  3oalem2  28650  nmopub2tALT  28896  nmfnleub2  28913  lnconi  29020  kbass5  29107  mdslmd1lem1  29312  mdslmd1lem2  29313  cdj1i  29420  disjabrex  29521  disjabrexf  29522  acunirnmpt  29587  acunirnmpt2  29588  acunirnmpt2f  29589  aciunf1lem  29590  fgreu  29599  xrge0infss  29653  xrofsup  29661  fsumiunle  29703  2sqmo  29777  ressprs  29783  xrge0addgt0  29819  submarchi  29868  isarchi3  29869  archiabllem1  29875  archiabllem2a  29876  gsumle  29907  suborng  29943  isarchiofld  29945  psgnfzto1stlem  29978  fzto1st1  29980  mdetpmtr1  30017  fimaproj  30028  txomap  30029  qtophaus  30031  cmpcref  30045  pstmxmet  30068  sqsscirc1  30082  ordtrest2NEWlem  30096  ordtconnlem1  30098  pnfneige0  30125  lmxrge0  30126  lmdvg  30127  qqhval2  30154  esumcst  30253  esumrnmpt2  30258  esumfsup  30260  esumcvg  30276  esum2d  30283  esumiun  30284  sigaclfu2  30312  insiga  30328  ldsysgenld  30351  ldgenpisyslem1  30354  fiunelros  30365  measinb  30412  imambfm  30452  oms0  30487  omssubadd  30490  carsgclctunlem3  30510  eulerpartlemgvv  30566  dstrvprob  30661  sgnsub  30734  signstfvneq0  30777  actfunsnrndisj  30811  reprinfz1  30828  breprexp  30839  afsval  30877  derangenlem  31279  sconnpi1  31347  cvmsss2  31382  cvmopnlem  31386  cvmlift3lem7  31433  msrval  31561  frpomin  31863  nosupno  31974  noetalem3  31990  noetalem5  31992  ifscgr  32276  cgrxfr  32287  btwnconn1lem13  32331  outsideofeu  32363  neibastop2lem  32480  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem14  33553  poimirlem22  33561  poimirlem29  33568  broucube  33573  heicant  33574  mblfinlem1  33576  itg2addnclem  33591  ftc1cnnc  33614  ftc1anclem7  33621  sstotbnd2  33703  equivtotbnd  33707  isbnd3  33713  ssbnd  33717  totbndbnd  33718  cntotbnd  33725  heibor1lem  33738  rrncmslem  33761  lssats  34617  lsat0cv  34638  lkrlss  34700  lfl1dim  34726  lfl1dim2N  34727  lkrpssN  34768  hlhgt2  34993  3dim2  35072  2dim  35074  lplncvrlvol  35220  paddasslem11  35434  pmapjat1  35457  2polssN  35519  pclfinclN  35554  pexmidlem8N  35581  lhpexle1lem  35611  4atex  35680  ltrnid  35739  trlator0  35776  cdlemg2cex  36196  tendodi1  36389  tendodi2  36390  diblss  36776  dihopelvalcpre  36854  dihatexv  36944  mapdval4N  37238  mzpindd  37626  mzpsubst  37628  mzpcompact2lem  37631  eldioph2b  37643  irrapxlem3  37705  irrapxlem5  37707  pellex  37716  pell1234qrdich  37742  pell14qrexpcl  37748  congabseq  37858  jm2.26a  37884  jm2.26lem3  37885  rmydioph  37898  lnrfg  38006  hbt  38017  rfovcnvf1od  38615  clsk3nimkb  38655  ntrneiiso  38706  ntrneikb  38709  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  4an4132  39022  iunconnlem2  39485  fnchoice  39502  cncmpmax  39505  ssinc  39578  ssdec  39579  disjf1  39683  supxrge  39867  suplesup  39868  infxr  39896  infleinf  39901  unb2ltle  39955  rexabslelem  39958  uzub  39971  supminfxr  40007  climrec  40153  climsuse  40158  islptre  40169  addlimc  40198  0ellimcdiv  40199  limsuppnfdlem  40251  limsupub  40254  limsuppnflem  40260  limsupubuz  40263  climinf3  40266  limsupmnflem  40270  climxrre  40300  liminfreuzlem  40352  liminflimsupclim  40357  icccncfext  40418  cncfiooicclem1  40424  fperdvper  40451  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvmptfprodlem  40477  dvmptfprod  40478  dvnprodlem2  40480  stoweidlem7  40542  stoweidlem34  40569  stoweidlem52  40587  stoweidlem60  40595  wallispilem3  40602  fourierdlem34  40676  fourierdlem38  40680  fourierdlem39  40681  fourierdlem48  40689  fourierdlem50  40691  fourierdlem51  40692  fourierdlem73  40714  fourierdlem76  40717  fourierdlem77  40718  fourierdlem80  40721  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  etransclem32  40801  etransclem33  40802  sge0f1o  40917  sge0pr  40929  sge0isum  40962  iundjiun  40995  meaiininclem  41021  pimdecfgtioo  41248  pimincfltioo  41249  preimageiingt  41251  preimaleiinlt  41252  smflimlem2  41301  smflimlem4  41303  smfmullem3  41321  smflimmpt  41337  smfinflem  41344  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  mgmhmeql  42128  isrng  42201  2zlidl  42259  lindslinindsimp2  42577  snlindsntor  42585  lincresunit2  42592  islindeps2  42597
  Copyright terms: Public domain W3C validator