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

Theorem simpllr 775
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 730 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:  fsnex  7021  soisoi  7064  f1o2ndf1  7805  fimaproj  7816  tz7.49  8068  omabs  8261  omxpenlem  8605  fopwdom  8612  findcard3  8749  frfi  8751  finsschain  8819  marypha1lem  8885  wdomtr  9027  cantnfp1  9132  harcard  9395  numacn  9464  infunsdom1  9628  sornom  9692  ssfin4  9725  fin1a2lem11  9825  fin1a2lem13  9827  fpwwe2lem13  10057  pwfseq  10079  mulcmpblnr  10486  00id  10808  addid1  10813  cnegex  10814  negeu  10869  add20  11145  ltmul12a  11489  lediv12a  11526  cru  11621  qextltlem  12587  xleadd1a  12638  xmullem  12649  xlemul1a  12673  ixxss12  12750  ioodisj  12864  fsuppmapnn0fz  13363  seqf1o  13411  mulexpz  13469  leexp1a  13539  faclbnd  13650  swrdswrdlem  14061  abs3lem  14694  rexico  14709  cau3lem  14710  rlim3  14851  ello12  14869  lo1bdd2  14877  elo12  14880  rlimconst  14897  isercoll  15020  climcau  15023  climbdd  15024  summolem2  15069  fsumconst  15141  o1fsum  15164  incexclem  15187  fprodconst  15328  bitsfzo  15778  dvdsmulgcd  15899  pc2dvds  16209  pcz  16211  pcadd  16219  pcfac  16229  vdwmc2  16309  vdwlem2  16312  vdwlem10  16320  vdw  16324  ramcl  16359  sbcie3s  16537  firest  16702  prdsval  16724  mreexd  16909  mreexexlemd  16911  iscat  16939  cidfval  16943  iscatd2  16948  catcocl  16952  catass  16953  catpropd  16975  cidpropd  16976  moni  17002  monpropd  17003  issubc  17101  subccocl  17111  funcco  17137  funcpropd  17166  fullpropd  17186  nati  17221  natpropd  17242  fucpropd  17243  xpcpropd  17454  curfuncf  17484  curf2ndf  17493  yonffthlem  17528  acsfiindd  17783  mndpropd  17932  mhmeql  17986  smndex1mgm  18068  isgrpinv  18152  dfgrp3lem  18193  mhmmnd  18217  cycsubm  18341  cycsubmcom  18343  conjnmzb  18389  gass  18427  symgextf  18541  dfod2  18687  gexdvds  18705  sylow3lem2  18749  efgredlem  18869  efgredeu  18874  ghmcmn  18949  oddvdssubg  18972  dprdfcntz  19134  pgpfaclem3  19202  issrg  19254  isring  19298  dvdsrmul1  19403  issubdrg  19557  islmhm2  19807  lmhmeql  19824  lssacsex  19913  isphl  20321  uvcf1  20485  lindfmm  20520  issubassa2  20582  opsrval  20718  scmatmats  21120  smatvscl  21133  mdetunilem7  21227  gsummatr01lem4  21267  m2cpmfo  21365  pmatcollpw3fi1lem1  21395  pm2mpf1lem  21403  pm2mpf1  21408  mp2pm2mplem4  21418  pm2mpghm  21425  chfacfscmulfsupp  21468  chfacfpmmulfsupp  21472  cctop  21615  neiptoptop  21740  neiptopreu  21742  tgrest  21768  ordtrest2lem  21812  cnss1  21885  cncnp  21889  isnrm3  21968  uncmp  22012  cmpfi  22017  iunconn  22037  1stcrest  22062  subislly  22090  islly2  22093  cldllycmp  22104  lly1stc  22105  llycmpkgen2  22159  kgencn  22165  xkoccn  22228  ptcnplem  22230  pthaus  22247  txhaus  22256  txkgen  22261  xkohaus  22262  xkococnlem  22268  txconn  22298  regr1lem2  22349  kqreglem1  22350  reghmph  22402  nrmhmph  22403  trfil2  22496  ufileu  22528  flimopn  22584  flimcf  22591  fclscf  22634  ufilcmp  22641  cnpfcf  22650  cnextfun  22673  tgpmulg  22702  symgtgp  22715  tgpt0  22728  qustgplem  22730  ustex2sym  22826  ustex3sym  22827  trust  22839  restutop  22847  restutopopn  22848  ustuqtop4  22854  utop3cls  22861  utopreg  22862  cstucnd  22894  ucncn  22895  trcfilu  22904  neipcfilu  22906  ismet2  22944  metequiv2  23121  metcnp  23152  metcnp2  23153  metcnpi3  23157  txmetcnp  23158  metustto  23164  metustsym  23166  metust  23169  cfilucfil  23170  metuel2  23176  psmetutop  23178  restmetu  23181  metucn  23182  ngptgp  23246  tngngp  23264  nmoleub  23341  icccmp  23434  reconnlem2  23436  reconn  23437  xmetdcn2  23446  metdseq0  23463  metdscn  23465  elcncf2  23499  cncfmet  23518  cnheibor  23564  nmoleub2lem2  23725  nmoleub3  23728  cvsi  23739  iscfil2  23874  iscfil3  23881  cfilfcls  23882  equivcfil  23907  caubl  23916  bcthlem5  23936  pmltpc  24058  ovollb2  24097  ovoliunnul  24115  ovolicc2lem4  24128  volsup  24164  ioorf  24181  dyadss  24202  dyaddisjlem  24203  mbfposr  24260  cncombf  24266  mbflimsup  24274  i1fmulclem  24310  mbfi1fseqlem4  24326  iblss2  24413  ellimc2  24484  ellimc3  24486  dvnadd  24536  dvmptfsum  24582  dvferm1  24592  dvferm2  24594  fta1g  24772  plyeq0lem  24811  plydivex  24897  fta1  24908  aalioulem2  24933  aalioulem3  24934  ulmuni  24991  ulmbdd  24997  ulmdvlem3  25001  mtest  25003  abelthlem8  25038  efopn  25253  cxpmul2z  25286  cxpcn3lem  25340  jensen  25578  lgambdd  25626  lgamucov  25627  isppw2  25704  mersenne  25815  dchrelbas3  25826  dchrptlem1  25852  dchrpt  25855  lgsval2lem  25895  lgsdchrval  25942  lgsquad3  25975  2sqb  26020  2sqmo  26025  pntrsumbnd2  26155  pntpbnd  26176  pntibnd  26181  istrkgc  26252  istrkgb  26253  tgjustr  26272  tglowdim1i  26299  tgbtwndiff  26304  tgifscgr  26306  iscgrglt  26312  tgcgrxfr  26316  lnext  26365  tgbtwnconn1lem3  26372  tgbtwnconn1  26373  legval  26382  legov  26383  legov2  26384  legtrd  26387  legtri3  26388  legso  26397  hlcgrex  26414  hlcgreu  26416  tglnne  26426  tglndim0  26427  tglineeltr  26429  tglinethru  26434  tglnne0  26438  tglnpt2  26439  colline  26447  tglowdim2l  26448  tglowdim2ln  26449  mirreu3  26452  miriso  26468  midexlem  26490  isperp  26510  perpcom  26511  perpneq  26512  isperp2  26513  footexALT  26516  footex  26519  colperpexlem3  26530  opphllem  26533  midex  26535  oppne3  26541  opptgdim2  26543  opphllem2  26546  opphllem3  26547  opphllem5  26549  opphllem6  26550  opphl  26552  outpasch  26553  lnopp2hpgb  26561  colopp  26567  lmieu  26582  trgcopy  26602  trgcopyeu  26604  iscgra1  26608  cgrane1  26610  cgrane2  26611  cgrane3  26612  cgrahl1  26614  cgrahl2  26615  cgracgr  26616  cgraswap  26618  cgracom  26620  cgratr  26621  flatcgra  26622  cgrabtwn  26624  cgrahl  26625  dfcgra2  26628  sacgr  26629  acopyeu  26632  inaghl  26643  cgrg3col4  26651  f1otrg  26669  f1otrge  26670  axsegcon  26725  axeuclidlem  26760  upgr1eopALT  26914  usgr1eop  27044  pthdepisspth  27528  wpthswwlks2on  27751  clwwlkf1  27838  clwwlknscsh  27851  2pthfrgr  28073  n4cyclfrgr  28080  frgrwopreglem5  28110  frgrwopreglem5ALT  28111  friendshipgt3  28187  smcnlem  28484  0lno  28577  ubthlem1  28657  ubthlem3  28659  chocunii  29088  occl  29091  5oalem1  29441  3oalem2  29450  nmopub2tALT  29696  nmfnleub2  29713  lnconi  29820  kbass5  29907  mdslmd1lem1  30112  mdslmd1lem2  30113  cdj1i  30220  opreu2reuALT  30251  disjabrex  30349  disjabrexf  30350  2ndresdju  30415  acunirnmpt  30426  acunirnmpt2  30427  acunirnmpt2f  30428  aciunf1lem  30429  fnpreimac  30438  fgreu  30439  suppovss  30447  xrge0infss  30514  xrofsup  30522  fsumiunle  30575  s3f1  30653  ccatf1  30655  swrdf1  30660  ressprs  30672  dfmgc2  30708  xrge0addgt0  30729  gsumle  30779  psgnfzto1stlem  30796  fzto1st1  30798  cycpmco2  30829  cycpmrn  30839  cyc3genpm  30848  cycpmconjs  30852  cyc3conja  30853  submarchi  30869  isarchi3  30870  archiabllem1  30876  archiabllem2a  30877  suborng  30943  isarchiofld  30945  imaslmod  30977  intlidl  31014  rhmpreimaidl  31015  elrspunidl  31018  rhmimaidl  31021  prmidl2  31028  isprmidlc  31035  rhmpreimaprmidl  31039  qsidomlem2  31041  mxidlprm  31052  ssmxidl  31054  lindsunlem  31112  lindsun  31113  dimkerim  31115  fedgmullem1  31117  fedgmul  31119  mdetpmtr1  31180  txomap  31191  qtophaus  31193  cmpcref  31207  zarclsun  31227  zarclssn  31230  zarcmplem  31238  pstmxmet  31254  sqsscirc1  31265  ordtrest2NEWlem  31279  ordtconnlem1  31281  pnfneige0  31308  lmxrge0  31309  lmdvg  31310  qqhval2  31337  esumcst  31436  esumrnmpt2  31441  esumfsup  31443  esumcvg  31459  esum2d  31466  esumiun  31467  sigaclfu2  31494  insiga  31510  ldsysgenld  31533  ldgenpisyslem1  31536  fiunelros  31547  measinb  31594  imambfm  31634  oms0  31669  omssubadd  31672  carsgclctunlem3  31692  eulerpartlemgvv  31748  dstrvprob  31843  sgnsub  31916  signstfvneq0  31956  actfunsnrndisj  31990  reprinfz1  32007  breprexp  32018  afsval  32056  derangenlem  32532  sconnpi1  32600  cvmsss2  32635  cvmopnlem  32639  cvmlift3lem7  32686  msrval  32899  frpomin  33192  fprlem2  33252  frrlem16  33257  nosupno  33317  noetalem3  33333  noetalem5  33335  ifscgr  33619  cgrxfr  33630  btwnconn1lem13  33674  outsideofeu  33706  neibastop2lem  33822  irrdifflemf  34740  irrdiff  34741  matunitlindflem1  35052  matunitlindflem2  35053  poimirlem14  35070  poimirlem22  35078  poimirlem29  35085  broucube  35090  heicant  35091  mblfinlem1  35093  itg2addnclem  35107  ftc1cnnc  35128  ftc1anclem7  35135  sstotbnd2  35211  equivtotbnd  35215  isbnd3  35221  ssbnd  35225  totbndbnd  35226  cntotbnd  35233  heibor1lem  35246  rrncmslem  35269  lssats  36307  lsat0cv  36328  lkrlss  36390  lfl1dim  36416  lfl1dim2N  36417  lkrpssN  36458  hlhgt2  36684  3dim2  36763  2dim  36765  lplncvrlvol  36911  paddasslem11  37125  pmapjat1  37148  2polssN  37210  pclfinclN  37245  pexmidlem8N  37272  lhpexle1lem  37302  4atex  37371  ltrnid  37430  trlator0  37466  cdlemg2cex  37886  tendodi1  38079  tendodi2  38080  diblss  38465  dihopelvalcpre  38543  dihatexv  38633  mapdval4N  38927  metakunt1  39347  metakunt2  39348  frlmsnic  39446  fsuppind  39449  sn-subeu  39556  sn-0tie0  39569  prjspersym  39594  dffltz  39608  mzpindd  39680  mzpsubst  39682  mzpcompact2lem  39685  eldioph2b  39697  irrapxlem3  39758  irrapxlem5  39760  pellex  39769  pell1234qrdich  39795  pell14qrexpcl  39801  congabseq  39908  jm2.26a  39934  jm2.26lem3  39935  rmydioph  39948  lnrfg  40056  hbt  40067  rfovcnvf1od  40698  clsk3nimkb  40736  ntrneiiso  40787  ntrneikb  40790  ntrneixb  40791  ntrneik3  40792  ntrneix3  40793  ntrneik13  40794  ntrneix13  40795  4an4132  41198  iunconnlem2  41634  fnchoice  41651  cncmpmax  41654  ssinc  41716  ssdec  41717  disjf1  41802  supxrge  41963  suplesup  41964  infxr  41992  infleinf  41997  unb2ltle  42045  rexabslelem  42048  uzub  42061  supminfxr  42096  climrec  42238  climsuse  42243  islptre  42254  addlimc  42283  0ellimcdiv  42284  limsuppnfdlem  42336  limsupub  42339  limsuppnflem  42345  limsupubuz  42348  climinf3  42351  limsupmnflem  42355  climxrre  42385  liminfreuzlem  42437  liminflimsupclim  42442  xlimliminflimsup  42497  icccncfext  42522  cncfiooicclem1  42528  fperdvper  42554  ioodvbdlimc1lem2  42567  ioodvbdlimc2lem  42569  dvmptfprodlem  42579  dvmptfprod  42580  dvnprodlem2  42582  stoweidlem7  42642  stoweidlem34  42669  stoweidlem52  42687  stoweidlem60  42695  wallispilem3  42702  fourierdlem34  42776  fourierdlem38  42780  fourierdlem39  42781  fourierdlem48  42789  fourierdlem50  42791  fourierdlem51  42792  fourierdlem73  42814  fourierdlem76  42817  fourierdlem77  42818  fourierdlem80  42821  fourierdlem87  42828  fourierdlem103  42844  fourierdlem104  42845  etransclem32  42901  etransclem33  42902  sge0f1o  43014  sge0pr  43026  sge0isum  43059  iundjiun  43092  meaiininclem  43118  pimdecfgtioo  43345  pimincfltioo  43346  preimageiingt  43348  preimaleiinlt  43349  smflimlem2  43398  smflimlem4  43400  smfmullem3  43418  smflimmpt  43434  smfinflem  43441  funressnbrafv2  43793  imasetpreimafvbijlemf1  43914  bgoldbtbndlem2  44317  bgoldbtbndlem3  44318  bgoldbtbnd  44320  isomuspgrlem2  44344  mgmhmeql  44416  isrng  44493  2zlidl  44551  lindslinindsimp2  44865  snlindsntor  44873  lincresunit2  44880  islindeps2  44885
  Copyright terms: Public domain W3C validator