Theorem simpllr 799

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simpllr	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpllr

Step	Hyp	Ref	Expression
1		simpr 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 762	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  simp-4r  807  fsnex  6538  soisoi  6578  f1o2ndf1  7285  tz7.49  7540  omabs  7727  omxpenlem  8061  fopwdom  8068  findcard3  8203  frfi  8205  finsschain  8273  marypha1lem  8339  wdomtr  8480  cantnfp1  8578  harcard  8804  numacn  8872  infunsdom1  9035  cofsmo  9091  sornom  9099  ssfin4  9132  fin1a2lem11  9232  fin1a2lem13  9234  ttukeylem5  9335  fpwwe2lem13  9464  pwfseq  9486  mulcmpblnr  9892  00id  10211  addid1  10216  cnegex  10217  negeu  10271  add20  10540  ltmul12a  10879  lediv12a  10916  fiminre  10972  cru  11012  qextltlem  12033  xleadd1a  12083  xmullem  12094  xlemul1a  12118  ixxss12  12195  ioodisj  12302  fsuppmapnn0fz  12796  seqf1o  12842  mulexpz  12900  leexp1a  12919  faclbnd  13077  swrdswrdlem  13459  abs3lem  14078  cau3lem  14094  rlim3  14229  ello12  14247  lo1bdd2  14255  elo12  14258  rlimconst  14275  isercoll  14398  climcau  14401  climbdd  14402  summolem2  14447  fsumconst  14522  o1fsum  14545  incexclem  14568  fprodconst  14708  bitsfzo  15157  dvdsmulgcd  15274  pc2dvds  15583  pcz  15585  pcadd  15593  pcfac  15603  vdwmc2  15683  vdwlem2  15686  vdwlem10  15694  vdw  15698  ramcl  15733  sbcie3s  15917  firest  16093  prdsval  16115  mreexd  16302  mreexexlemd  16304  iscat  16333  cidfval  16337  iscatd2  16342  catcocl  16346  catass  16347  catpropd  16369  cidpropd  16370  moni  16396  monpropd  16397  issubc  16495  subccocl  16505  funcco  16531  funcpropd  16560  fullpropd  16580  nati  16615  natpropd  16636  fucpropd  16637  xpcpropd  16848  curfuncf  16878  curf2ndf  16887  yonffthlem  16922  acsfiindd  17177  mndpropd  17316  mhmeql  17364  isgrpinv  17472  dfgrp3lem  17513  mhmmnd  17537  conjnmzb  17695  gass  17734  symgextf  17837  dfod2  17981  gexdvds  17999  sylow3lem2  18043  efgredlem  18160  efgredeu  18165  ghmcmn  18237  oddvdssubg  18258  dprdfcntz  18414  pgpfaclem3  18482  issrg  18507  isring  18551  dvdsrmul1  18653  issubdrg  18805  islmhm2  19038  lmhmeql  19055  lssacsex  19144  issubassa2  19345  opsrval  19474  isphl  19973  uvcf1  20131  lindfmm  20166  scmatmats  20317  smatvscl  20330  mdetunilem7  20424  gsummatr01lem4  20464  m2cpmfo  20561  decpmatmulsumfsupp  20578  pmatcollpw3fi1lem1  20591  pm2mpf1lem  20599  pm2mpf1  20604  mp2pm2mplem4  20614  pm2mpghm  20621  pm2mpmhmlem1  20623  pm2mpmhmlem2  20624  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  cctop  20810  neiptoptop  20935  neiptopreu  20937  tgrest  20963  ordtrest2lem  21007  cnss1  21080  cncnp  21084  isnrm3  21163  uncmp  21206  cmpfi  21211  iunconn  21231  1stcrest  21256  subislly  21284  islly2  21287  cldllycmp  21298  lly1stc  21299  llycmpkgen2  21353  kgencn  21359  xkoccn  21422  ptcnplem  21424  pthaus  21441  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  txconn  21492  regr1lem2  21543  kqreglem1  21544  reghmph  21596  nrmhmph  21597  trfil2  21691  ufileu  21723  flimopn  21779  flimcf  21786  fclscf  21829  ufilcmp  21836  cnpfcf  21845  cnextfun  21868  tgpmulg  21897  symgtgp  21905  tgpt0  21922  qustgplem  21924  ustex2sym  22020  ustex3sym  22021  trust  22033  restutop  22041  restutopopn  22042  ustuqtop2  22046  ustuqtop4  22048  utop3cls  22055  utopreg  22056  cstucnd  22088  ucncn  22089  trcfilu  22098  neipcfilu  22100  ismet2  22138  metequiv2  22315  metcnp  22346  metcnp2  22347  metcnpi3  22351  txmetcnp  22352  metustto  22358  metustsym  22360  metust  22363  cfilucfil  22364  metuel2  22370  psmetutop  22372  restmetu  22375  metucn  22376  ngptgp  22440  tngngp  22458  nmoleub  22535  icccmp  22628  reconnlem2  22630  reconn  22631  xmetdcn2  22640  metdseq0  22657  metdscn  22659  elcncf2  22693  cncfmet  22711  cnheibor  22754  nmoleub2lem2  22916  nmoleub3  22919  cvsi  22930  iscfil2  23064  iscfil3  23071  cfilfcls  23072  equivcfil  23097  caubl  23106  bcthlem5  23125  pmltpc  23219  ovollb2  23257  ovoliunnul  23275  ovolicc2lem4  23288  volsup  23324  ioorf  23341  dyadss  23362  dyaddisjlem  23363  mbfposr  23419  cncombf  23425  mbflimsup  23433  i1fmulclem  23469  mbfi1fseqlem4  23485  iblss2  23572  ellimc2  23641  ellimc3  23643  dvnadd  23692  dvmptfsum  23738  dvferm1  23748  dvferm2  23750  fta1g  23927  plyeq0lem  23966  plydivex  24052  fta1  24063  aalioulem2  24088  aalioulem3  24089  ulmuni  24146  ulmbdd  24152  ulmdvlem3  24156  mtest  24158  abelthlem8  24193  pilem3  24207  efopn  24404  cxpmul2z  24437  cxpcn3lem  24488  jensen  24715  lgambdd  24763  lgamucov  24764  isppw2  24841  sqf11  24865  mersenne  24952  dchrelbas3  24963  dchrptlem1  24989  dchrpt  24992  lgsval2lem  25032  lgsdchrval  25079  lgsquad3  25112  2sqb  25157  pntrsumbnd2  25256  pntpbnd  25277  pntibnd  25282  istrkgc  25353  istrkgb  25354  tglowdim1i  25396  tgbtwndiff  25401  tgifscgr  25403  iscgrglt  25409  tgcgrxfr  25413  lnext  25462  tgbtwnconn1lem3  25469  tgbtwnconn1  25470  legval  25479  legov  25480  legov2  25481  legtrd  25484  legtri3  25485  legso  25494  hlcgrex  25511  hlcgreu  25513  tglnne  25523  tglndim0  25524  tglineeltr  25526  tglinethru  25531  tglnne0  25535  tglnpt2  25536  colline  25544  tglowdim2l  25545  tglowdim2ln  25546  mirreu3  25549  miriso  25565  midexlem  25587  isperp  25607  perpcom  25608  perpneq  25609  isperp2  25610  footex  25613  colperpexlem3  25624  opphllem  25627  midex  25629  oppne3  25635  opptgdim2  25637  opphllem2  25640  opphllem3  25641  opphllem5  25643  opphllem6  25644  opphl  25646  outpasch  25647  lnopp2hpgb  25655  colopp  25661  lmieu  25676  trgcopy  25696  trgcopyeu  25698  iscgra1  25702  cgrane1  25704  cgrane2  25705  cgrane3  25706  cgrahl1  25708  cgrahl2  25709  cgracgr  25710  cgraswap  25712  cgracom  25714  cgratr  25715  cgrabtwn  25717  cgrahl  25718  dfcgra2  25721  sacgr  25722  acopyeu  25725  inaghl  25731  cgrg3col4  25734  f1otrg  25751  f1otrge  25752  axsegcon  25807  axeuclidlem  25842  axcontlem2  25845  upgr1eopALT  26012  usgr1eop  26142  pthdepisspth  26631  clwwlksf1  26917  clwwlksnscsh  26940  2pthfrgr  27148  n4cyclfrgr  27155  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  friendshipgt3  27256  smcnlem  27552  0lno  27645  ubthlem1  27726  ubthlem3  27728  chocunii  28160  occl  28163  5oalem1  28513  3oalem2  28522  nmopub2tALT  28768  nmfnleub2  28785  lnconi  28892  kbass5  28979  mdslmd1lem1  29184  mdslmd1lem2  29185  cdj1i  29292  disjabrex  29395  disjabrexf  29396  acunirnmpt  29459  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1lem  29462  fgreu  29471  xrge0infss  29525  xrofsup  29533  fsumiunle  29575  2sqmo  29649  ressprs  29655  xrge0addgt0  29691  submarchi  29740  isarchi3  29741  archiabllem1  29747  archiabllem2a  29748  gsumle  29779  suborng  29815  isarchiofld  29817  psgnfzto1stlem  29850  fzto1st1  29852  mdetpmtr1  29889  fimaproj  29900  txomap  29901  qtophaus  29903  cmpcref  29917  pstmxmet  29940  sqsscirc1  29954  ordtrest2NEWlem  29968  ordtconnlem1  29970  pnfneige0  29997  lmxrge0  29998  lmdvg  29999  qqhval2  30026  esumcst  30125  esumrnmpt2  30130  esumfsup  30132  esumcvg  30148  esum2d  30155  esumiun  30156  sigaclfu2  30184  insiga  30200  ldsysgenld  30223  ldgenpisyslem1  30226  fiunelros  30237  measinb  30284  imambfm  30324  oms0  30359  omssubadd  30362  carsgclctunlem3  30382  eulerpartlemgvv  30438  dstrvprob  30533  sgnsub  30606  signstfvneq0  30649  actfunsnrndisj  30683  reprinfz1  30700  breprexp  30711  afsval  30749  derangenlem  31153  sconnpi1  31221  cvmsss2  31256  cvmopnlem  31260  cvmlift3lem7  31307  msrval  31435  nosupno  31849  noetalem3  31865  noetalem5  31867  ifscgr  32151  cgrxfr  32162  btwnconn1lem13  32206  outsideofeu  32238  neibastop2lem  32355  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem14  33423  poimirlem22  33431  poimirlem29  33438  broucube  33443  heicant  33444  mblfinlem1  33446  itg2addnclem  33461  ftc1cnnc  33484  ftc1anclem7  33491  sstotbnd2  33573  equivtotbnd  33577  isbnd3  33583  ssbnd  33587  totbndbnd  33588  cntotbnd  33595  heibor1lem  33608  rrncmslem  33631  lssats  34299  lsat0cv  34320  lkrlss  34382  lfl1dim  34408  lfl1dim2N  34409  lkrpssN  34450  hlhgt2  34675  3dim2  34754  2dim  34756  lplncvrlvol  34902  paddasslem11  35116  pmapjat1  35139  2polssN  35201  pclfinclN  35236  pexmidlem8N  35263  lhpexle1lem  35293  4atex  35362  ltrnid  35421  trlator0  35458  cdlemg2cex  35879  tendodi1  36072  tendodi2  36073  diblss  36459  dihopelvalcpre  36537  dihatexv  36627  mapdval4N  36921  mzpindd  37309  mzpsubst  37311  mzpcompact2lem  37314  eldioph2b  37326  irrapxlem3  37388  irrapxlem5  37390  pellex  37399  pell1234qrdich  37425  pell14qrexpcl  37431  congabseq  37541  jm2.26a  37567  jm2.26lem3  37568  rmydioph  37581  lnrfg  37689  hbt  37700  rfovcnvf1od  38298  clsk3nimkb  38338  ntrneiiso  38389  ntrneikb  38392  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  4an4132  38705  iunconnlem2  39171  fnchoice  39188  cncmpmax  39191  ssinc  39264  ssdec  39265  disjf1  39369  supxrge  39554  suplesup  39555  infxr  39583  infleinf  39588  unb2ltle  39642  rexabslelem  39645  uzub  39658  supminfxr  39694  climrec  39835  climsuse  39840  islptre  39851  addlimc  39880  0ellimcdiv  39881  limsuppnfdlem  39933  limsupub  39936  limsuppnflem  39942  limsupubuz  39945  climinf3  39948  limsupmnflem  39952  climxrre  39982  liminfreuzlem  40034  liminflimsupclim  40039  icccncfext  40100  cncfiooicclem1  40106  fperdvper  40133  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem2  40162  stoweidlem7  40224  stoweidlem34  40251  stoweidlem52  40269  stoweidlem60  40277  wallispilem3  40284  fourierdlem34  40358  fourierdlem38  40362  fourierdlem39  40363  fourierdlem48  40371  fourierdlem50  40373  fourierdlem51  40374  fourierdlem73  40396  fourierdlem76  40399  fourierdlem77  40400  fourierdlem80  40403  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  etransclem32  40483  etransclem33  40484  sge0f1o  40599  sge0pr  40611  sge0isum  40644  iundjiun  40677  meaiininclem  40700  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  smflimlem2  40980  smflimlem4  40982  smfmullem3  41000  smflimmpt  41016  smfinflem  41023  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  mgmhmeql  41803  isrng  41876  2zlidl  41934  lindslinindsimp2  42252  snlindsntor  42260  lincresunit2  42267  islindeps2  42272