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 397
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 206  df-an 398
This theorem is referenced by:  frpomin  6295  fsnex  7230  soisoi  7274  f1o2ndf1  8055  fimaproj  8068  fprlem2  8233  tz7.49  8392  omabs  8598  cofon1  8619  naddssim  8631  omxpenlem  9018  fopwdom  9025  findcard3  9230  findcard3OLD  9231  frfi  9233  finsschain  9304  marypha1lem  9370  wemappo  9486  wdomtr  9512  cantnfp1  9618  ttrcltr  9653  harcard  9915  numacn  9986  infunsdom1  10150  sornom  10214  ssfin4  10247  fin1a2lem11  10347  fin1a2lem13  10349  fpwwe2lem12  10579  pwfseq  10601  mulcmpblnr  11008  00id  11331  addid1  11336  cnegex  11337  negeu  11392  add20  11668  ltmul12a  12012  lediv12a  12049  cru  12146  qextltlem  13122  xleadd1a  13173  xmullem  13184  xlemul1a  13208  ixxss12  13285  ioodisj  13400  fsuppmapnn0fz  13902  seqf1o  13950  mulexpz  14009  leexp1a  14081  faclbnd  14191  swrdswrdlem  14593  abs3lem  15224  rexico  15239  cau3lem  15240  rlim3  15381  ello12  15399  lo1bdd2  15407  elo12  15410  rlimconst  15427  isercoll  15553  climcau  15556  climbdd  15557  summolem2  15602  fsumconst  15676  o1fsum  15699  incexclem  15722  fprodconst  15862  bitsfzo  16316  dvdsmulgcd  16437  pc2dvds  16752  pcz  16754  pcadd  16762  pcfac  16772  vdwmc2  16852  vdwlem2  16855  vdwlem10  16863  vdw  16867  ramcl  16902  sbcie3s  17035  firest  17315  prdsval  17338  mreexd  17523  mreexexlemd  17525  iscat  17553  cidfval  17557  iscatd2  17562  catcocl  17566  catass  17567  catpropd  17590  cidpropd  17591  moni  17620  monpropd  17621  issubc  17722  subccocl  17732  funcco  17758  funcpropd  17788  fullpropd  17808  nati  17843  natpropd  17866  fucpropd  17867  xpcpropd  18098  curfuncf  18128  curf2ndf  18137  yonffthlem  18172  acsfiindd  18443  mndpropd  18582  mhmeql  18637  smndex1mgm  18718  isgrpinv  18805  dfgrp3lem  18846  mhmmnd  18870  cycsubm  18996  cycsubmcom  18998  conjnmzb  19044  gass  19082  symgextf  19200  dfod2  19347  gexdvds  19367  sylow3lem2  19411  efgredlem  19530  efgredeu  19535  ghmcmn  19611  oddvdssubg  19634  dprdfcntz  19795  pgpfaclem3  19863  issrg  19920  isring  19969  dvdsrmul1  20083  issubdrg  20250  islmhm2  20502  lmhmeql  20519  lssacsex  20608  isphl  21035  uvcf1  21201  lindfmm  21236  issubassa2  21298  opsrval  21450  mhpmulcl  21542  scmatmats  21863  smatvscl  21876  mdetunilem7  21970  gsummatr01lem4  22010  m2cpmfo  22108  pmatcollpw3fi1lem1  22138  pm2mpf1lem  22146  pm2mpf1  22151  mp2pm2mplem4  22161  pm2mpghm  22168  chfacfscmulfsupp  22211  chfacfpmmulfsupp  22215  cctop  22359  neiptoptop  22485  neiptopreu  22487  tgrest  22513  ordtrest2lem  22557  cnss1  22630  cncnp  22634  isnrm3  22713  uncmp  22757  cmpfi  22762  iunconn  22782  1stcrest  22807  subislly  22835  islly2  22838  cldllycmp  22849  lly1stc  22850  llycmpkgen2  22904  kgencn  22910  xkoccn  22973  ptcnplem  22975  pthaus  22992  txhaus  23001  txkgen  23006  xkohaus  23007  xkococnlem  23013  txconn  23043  regr1lem2  23094  kqreglem1  23095  reghmph  23147  nrmhmph  23148  trfil2  23241  ufileu  23273  flimopn  23329  flimcf  23336  fclscf  23379  ufilcmp  23386  cnpfcf  23395  cnextfun  23418  tgpmulg  23447  symgtgp  23460  tgpt0  23473  qustgplem  23475  ustex2sym  23571  ustex3sym  23572  trust  23584  restutop  23592  restutopopn  23593  ustuqtop4  23599  utop3cls  23606  utopreg  23607  cstucnd  23639  ucncn  23640  trcfilu  23649  neipcfilu  23651  ismet2  23689  metequiv2  23869  metcnp  23900  metcnp2  23901  metcnpi3  23905  txmetcnp  23906  metustto  23912  metustsym  23914  metust  23917  cfilucfil  23918  metuel2  23924  psmetutop  23926  restmetu  23929  metucn  23930  ngptgp  23995  tngngp  24021  nmoleub  24098  icccmp  24191  reconnlem2  24193  reconn  24194  xmetdcn2  24203  metdseq0  24220  metdscn  24222  elcncf2  24256  cncfmet  24275  cnheibor  24321  nmoleub2lem2  24482  nmoleub3  24485  cvsi  24496  iscfil2  24633  iscfil3  24640  cfilfcls  24641  equivcfil  24666  caubl  24675  bcthlem5  24695  pmltpc  24817  ovollb2  24856  ovoliunnul  24874  ovolicc2lem4  24887  volsup  24923  ioorf  24940  dyadss  24961  dyaddisjlem  24962  mbfposr  25019  cncombf  25025  mbflimsup  25033  i1fmulclem  25070  mbfi1fseqlem4  25086  iblss2  25173  ellimc2  25244  ellimc3  25246  dvnadd  25296  dvmptfsum  25342  dvferm1  25352  dvferm2  25354  fta1g  25535  plyeq0lem  25574  plydivex  25660  fta1  25671  aalioulem2  25696  aalioulem3  25697  ulmuni  25754  ulmbdd  25760  ulmdvlem3  25764  mtest  25766  abelthlem8  25801  efopn  26016  cxpmul2z  26049  cxpcn3lem  26103  jensen  26341  lgambdd  26389  lgamucov  26390  isppw2  26467  mersenne  26578  dchrelbas3  26589  dchrptlem1  26615  dchrpt  26618  lgsval2lem  26658  lgsdchrval  26705  lgsquad3  26738  2sqb  26783  2sqmo  26788  pntrsumbnd2  26918  pntpbnd  26939  pntibnd  26944  nosupno  27054  noinfno  27069  noetasuplem4  27087  noetalem1  27092  madebday  27232  cofcutr  27246  negsprop  27336  istrkgc  27399  istrkgb  27400  tgjustr  27419  tglowdim1i  27446  tgbtwndiff  27451  tgifscgr  27453  iscgrglt  27459  tgcgrxfr  27463  lnext  27512  tgbtwnconn1lem3  27519  tgbtwnconn1  27520  legval  27529  legov  27530  legov2  27531  legtrd  27534  legtri3  27535  legso  27544  hlcgrex  27561  hlcgreu  27563  tglnne  27573  tglndim0  27574  tglineeltr  27576  tglinethru  27581  tglnne0  27585  tglnpt2  27586  colline  27594  tglowdim2l  27595  tglowdim2ln  27596  mirreu3  27599  miriso  27615  midexlem  27637  isperp  27657  perpcom  27658  perpneq  27659  isperp2  27660  footexALT  27663  footex  27666  colperpexlem3  27677  opphllem  27680  midex  27682  oppne3  27688  opptgdim2  27690  opphllem2  27693  opphllem3  27694  opphllem5  27696  opphllem6  27697  opphl  27699  outpasch  27700  lnopp2hpgb  27708  colopp  27714  lmieu  27729  trgcopy  27749  trgcopyeu  27751  iscgra1  27755  cgrane1  27757  cgrane2  27758  cgrane3  27759  cgrahl1  27761  cgrahl2  27762  cgracgr  27763  cgraswap  27765  cgracom  27767  cgratr  27768  flatcgra  27769  cgrabtwn  27771  cgrahl  27772  dfcgra2  27775  sacgr  27776  acopyeu  27779  inaghl  27790  cgrg3col4  27798  f1otrg  27816  f1otrge  27817  axsegcon  27879  axeuclidlem  27914  upgr1eopALT  28071  usgr1eop  28201  pthdepisspth  28686  wpthswwlks2on  28909  clwwlkf1  28996  clwwlknscsh  29009  2pthfrgr  29231  n4cyclfrgr  29238  frgrwopreglem5  29268  frgrwopreglem5ALT  29269  friendshipgt3  29345  smcnlem  29642  0lno  29735  ubthlem1  29815  ubthlem3  29817  chocunii  30246  occl  30249  5oalem1  30599  3oalem2  30608  nmopub2tALT  30854  nmfnleub2  30871  lnconi  30978  kbass5  31065  mdslmd1lem1  31270  mdslmd1lem2  31271  cdj1i  31378  opreu2reuALT  31408  disjabrex  31503  disjabrexf  31504  2ndresdju  31568  acunirnmpt  31578  acunirnmpt2  31579  acunirnmpt2f  31580  aciunf1lem  31581  fnpreimac  31590  fgreu  31591  suppovss  31601  xrge0infss  31668  xrofsup  31675  fsumiunle  31728  s3f1  31806  ccatf1  31808  swrdf1  31813  ressprs  31826  dfmgc2  31859  mgcf1o  31866  xrge0addgt0  31885  gsumle  31935  psgnfzto1stlem  31952  fzto1st1  31954  cycpmco2  31985  cycpmrn  31995  cyc3genpm  32004  cycpmconjs  32008  cyc3conja  32009  submarchi  32025  isarchi3  32026  archiabllem1  32032  archiabllem2a  32033  suborng  32113  isarchiofld  32115  imaslmod  32148  nsgqusf1olem2  32195  ghmqusker  32201  intlidl  32202  rhmpreimaidl  32203  elrspunidl  32206  rhmimaidl  32209  prmidl2  32216  isprmidlc  32223  rhmpreimaprmidl  32227  qsidomlem2  32229  mxidlprm  32240  ssmxidl  32242  lindsunlem  32322  lindsun  32323  dimkerim  32325  fedgmullem1  32327  fedgmul  32329  mdetpmtr1  32407  txomap  32418  qtophaus  32420  cmpcref  32434  zarclsun  32454  zarclssn  32457  zarcmplem  32465  pstmxmet  32481  sqsscirc1  32492  ordtrest2NEWlem  32506  ordtconnlem1  32508  pnfneige0  32535  lmxrge0  32536  lmdvg  32537  qqhval2  32566  esumcst  32665  esumrnmpt2  32670  esumfsup  32672  esumcvg  32688  esum2d  32695  esumiun  32696  sigaclfu2  32723  insiga  32739  ldsysgenld  32762  ldgenpisyslem1  32765  fiunelros  32776  measinb  32823  imambfm  32865  oms0  32900  omssubadd  32903  carsgclctunlem3  32923  eulerpartlemgvv  32979  dstrvprob  33074  sgnsub  33147  signstfvneq0  33187  actfunsnrndisj  33221  reprinfz1  33238  breprexp  33249  afsval  33287  derangenlem  33768  sconnpi1  33836  cvmsss2  33871  cvmopnlem  33875  cvmlift3lem7  33922  msrval  34135  ifscgr  34632  cgrxfr  34643  btwnconn1lem13  34687  outsideofeu  34719  neibastop2lem  34835  irrdifflemf  35799  irrdiff  35800  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem14  36095  poimirlem22  36103  poimirlem29  36110  broucube  36115  heicant  36116  mblfinlem1  36118  itg2addnclem  36132  ftc1cnnc  36153  ftc1anclem7  36160  sstotbnd2  36236  equivtotbnd  36240  isbnd3  36246  ssbnd  36250  totbndbnd  36251  cntotbnd  36258  heibor1lem  36271  rrncmslem  36294  lssats  37477  lsat0cv  37498  lkrlss  37560  lfl1dim  37586  lfl1dim2N  37587  lkrpssN  37628  hlhgt2  37855  3dim2  37934  2dim  37936  lplncvrlvol  38082  paddasslem11  38296  pmapjat1  38319  2polssN  38381  pclfinclN  38416  pexmidlem8N  38443  lhpexle1lem  38473  4atex  38542  ltrnid  38601  trlator0  38637  cdlemg2cex  39057  tendodi1  39250  tendodi2  39251  diblss  39636  dihopelvalcpre  39714  dihatexv  39804  mapdval4N  40098  fldhmf1  40550  aks6d1c2p2  40552  sticksstones8  40564  sticksstones12  40569  sticksstones22  40579  metakunt1  40580  metakunt2  40581  frlmsnic  40731  fsuppind  40768  sn-subeu  40898  sn-0tie0  40911  prjspersym  40948  dffltz  40975  nna4b4nsq  41001  mzpindd  41072  mzpsubst  41074  mzpcompact2lem  41077  eldioph2b  41089  irrapxlem3  41150  irrapxlem5  41152  pellex  41161  pell1234qrdich  41187  pell14qrexpcl  41193  congabseq  41301  jm2.26a  41327  jm2.26lem3  41328  rmydioph  41341  lnrfg  41449  hbt  41460  cantnftermord  41657  cantnfresb  41661  cantnf2  41662  oawordex2  41663  omabs2  41668  ofoaass  41677  rfovcnvf1od  42283  clsk3nimkb  42319  ntrneiiso  42370  ntrneikb  42373  ntrneixb  42374  ntrneik3  42375  ntrneix3  42376  ntrneik13  42377  ntrneix13  42378  4an4132  42788  iunconnlem2  43224  fnchoice  43241  cncmpmax  43244  ssinc  43304  ssdec  43305  disjf1  43408  supxrge  43579  suplesup  43580  infxr  43608  infleinf  43613  unb2ltle  43657  rexabslelem  43660  uzub  43673  supminfxr  43706  climrec  43851  climsuse  43856  islptre  43867  addlimc  43896  0ellimcdiv  43897  limsuppnfdlem  43949  limsupub  43952  limsuppnflem  43958  limsupubuz  43961  climinf3  43964  limsupmnflem  43968  climxrre  43998  liminfreuzlem  44050  liminflimsupclim  44055  xlimliminflimsup  44110  icccncfext  44135  cncfiooicclem1  44141  fperdvper  44167  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvmptfprodlem  44192  dvmptfprod  44193  dvnprodlem2  44195  stoweidlem7  44255  stoweidlem34  44282  stoweidlem52  44300  stoweidlem60  44308  wallispilem3  44315  fourierdlem34  44389  fourierdlem38  44393  fourierdlem39  44394  fourierdlem48  44402  fourierdlem50  44404  fourierdlem51  44405  fourierdlem73  44427  fourierdlem76  44430  fourierdlem77  44431  fourierdlem80  44434  fourierdlem87  44441  fourierdlem103  44457  fourierdlem104  44458  etransclem32  44514  etransclem33  44515  sge0f1o  44630  sge0pr  44642  sge0isum  44675  iundjiun  44708  meaiininclem  44734  pimdecfgtioo  44965  pimincfltioo  44966  preimageiingt  44968  preimaleiinlt  44969  smflimlem2  45020  smflimlem4  45022  smfmullem3  45041  smflimmpt  45058  smfinflem  45065  smfpimne2  45088  fsupdm  45090  finfdm  45094  cfsetsnfsetfo  45301  funressnbrafv2  45483  imasetpreimafvbijlemf1  45603  bgoldbtbndlem2  46005  bgoldbtbndlem3  46006  bgoldbtbnd  46008  isomuspgrlem2  46032  mgmhmeql  46104  isrng  46181  2zlidl  46239  lindslinindsimp2  46551  snlindsntor  46559  lincresunit2  46566  islindeps2  46571
  Copyright terms: Public domain W3C validator