Theorem simpllr 795

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 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	ad2antrr 758	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

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 196  df-an 385

This theorem is referenced by:  simp-4r  803  fsnex  6438  soisoi  6478  f1o2ndf1  7172  tz7.49  7427  omabs  7614  omxpenlem  7946  fopwdom  7953  findcard3  8088  frfi  8090  finsschain  8156  marypha1lem  8222  wdomtr  8363  cantnfp1  8461  harcard  8687  numacn  8755  infunsdom1  8918  cofsmo  8974  sornom  8982  ssfin4  9015  fin1a2lem11  9115  fin1a2lem13  9117  ttukeylem5  9218  fpwwe2lem13  9343  pwfseq  9365  mulcmpblnr  9771  00id  10090  addid1  10095  cnegex  10096  negeu  10150  add20  10419  ltmul12a  10758  lediv12a  10795  fiminre  10851  cru  10889  qextltlem  11907  xleadd1a  11955  xmullem  11966  xlemul1a  11990  ixxss12  12066  ioodisj  12173  fsuppmapnn0fz  12658  seqf1o  12704  mulexpz  12762  leexp1a  12781  faclbnd  12939  swrdswrdlem  13311  abs3lem  13926  cau3lem  13942  rlim3  14077  ello12  14095  lo1bdd2  14103  elo12  14106  rlimconst  14123  isercoll  14246  climcau  14249  climbdd  14250  summolem2  14294  fsumconst  14364  o1fsum  14386  incexclem  14407  fprodconst  14547  bitsfzo  14995  dvdsmulgcd  15112  pc2dvds  15421  pcz  15423  pcadd  15431  pcfac  15441  vdwmc2  15521  vdwlem2  15524  vdwlem10  15532  vdw  15536  ramcl  15571  sbcie3s  15745  firest  15916  prdsval  15938  mreexd  16125  mreexexlemd  16127  iscat  16156  cidfval  16160  iscatd2  16165  catcocl  16169  catass  16170  catpropd  16192  cidpropd  16193  moni  16219  monpropd  16220  issubc  16318  subccocl  16328  funcco  16354  funcpropd  16383  fullpropd  16403  nati  16438  natpropd  16459  fucpropd  16460  xpcpropd  16671  curfuncf  16701  curf2ndf  16710  yonffthlem  16745  acsfiindd  17000  mndpropd  17139  mhmeql  17187  isgrpinv  17295  dfgrp3lem  17336  mhmmnd  17360  conjnmzb  17518  gass  17557  symgextf  17660  dfod2  17804  gexdvds  17822  sylow3lem2  17866  efgredlem  17983  efgredeu  17988  ghmcmn  18060  oddvdssubg  18081  dprdfcntz  18237  pgpfaclem3  18305  issrg  18330  isring  18374  dvdsrmul1  18476  issubdrg  18628  islmhm2  18859  lmhmeql  18876  lssacsex  18965  issubassa2  19166  opsrval  19295  isphl  19792  uvcf1  19950  lindfmm  19985  scmatmats  20136  smatvscl  20149  mdetunilem7  20243  gsummatr01lem4  20283  m2cpmfo  20380  decpmatmulsumfsupp  20397  pmatcollpw3fi1lem1  20410  pm2mpf1lem  20418  pm2mpf1  20423  mp2pm2mplem4  20433  pm2mpghm  20440  pm2mpmhmlem1  20442  pm2mpmhmlem2  20443  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  cctop  20620  neiptoptop  20745  neiptopreu  20747  tgrest  20773  ordtrest2lem  20817  cnss1  20890  cncnp  20894  isnrm3  20973  uncmp  21016  cmpfi  21021  iuncon  21041  1stcrest  21066  subislly  21094  islly2  21097  cldllycmp  21108  lly1stc  21109  llycmpkgen2  21163  kgencn  21169  xkoccn  21232  ptcnplem  21234  pthaus  21251  txhaus  21260  txkgen  21265  xkohaus  21266  xkococnlem  21272  txcon  21302  regr1lem2  21353  kqreglem1  21354  reghmph  21406  nrmhmph  21407  trfil2  21501  ufileu  21533  flimopn  21589  flimcf  21596  fclscf  21639  ufilcmp  21646  cnpfcf  21655  cnextfun  21678  tgpmulg  21707  symgtgp  21715  tgpt0  21732  qustgplem  21734  ustex2sym  21830  ustex3sym  21831  trust  21843  restutop  21851  restutopopn  21852  ustuqtop2  21856  ustuqtop4  21858  utop3cls  21865  utopreg  21866  cstucnd  21898  ucncn  21899  trcfilu  21908  neipcfilu  21910  ismet2  21948  metequiv2  22125  metcnp  22156  metcnp2  22157  metcnpi3  22161  txmetcnp  22162  metustto  22168  metustsym  22170  metust  22173  cfilucfil  22174  metuel2  22180  psmetutop  22182  restmetu  22185  metucn  22186  ngptgp  22250  tngngp  22268  nmoleub  22345  icccmp  22436  reconnlem2  22438  reconn  22439  xmetdcn2  22448  metdseq0  22465  metdscn  22467  elcncf2  22501  cncfmet  22519  cnheibor  22562  nmoleub2lem2  22724  nmoleub3  22727  cvsi  22738  iscfil2  22872  iscfil3  22879  cfilfcls  22880  equivcfil  22905  caubl  22914  bcthlem5  22933  pmltpc  23026  ovollb2  23064  ovoliunnul  23082  ovolicc2lem4  23095  volsup  23131  ioorf  23147  dyadss  23168  dyaddisjlem  23169  mbfposr  23225  cncombf  23231  mbflimsup  23239  i1fmulclem  23275  mbfi1fseqlem4  23291  iblss2  23378  ellimc2  23447  ellimc3  23449  dvnadd  23498  dvmptfsum  23542  dvferm1  23552  dvferm2  23554  fta1g  23731  plyeq0lem  23770  plydivex  23856  fta1  23867  aalioulem2  23892  aalioulem3  23893  ulmuni  23950  ulmbdd  23956  ulmdvlem3  23960  mtest  23962  abelthlem8  23997  pilem3  24011  efopn  24204  cxpmul2z  24237  cxpcn3lem  24288  jensen  24515  lgambdd  24563  lgamucov  24564  isppw2  24641  sqf11  24665  mersenne  24752  dchrelbas3  24763  dchrptlem1  24789  dchrpt  24792  lgsval2lem  24832  lgsdchrval  24879  lgsquad3  24912  2sqb  24957  pntrsumbnd2  25056  pntpbnd  25077  pntibnd  25082  istrkgc  25153  istrkgb  25154  tglowdim1i  25196  tgbtwndiff  25201  tgifscgr  25203  iscgrglt  25209  tgcgrxfr  25213  lnext  25262  tgbtwnconn1lem3  25269  tgbtwnconn1  25270  legval  25279  legov  25280  legov2  25281  legtrd  25284  legtri3  25285  legso  25294  hlcgrex  25311  hlcgreu  25313  tglnne  25323  tglndim0  25324  tglineeltr  25326  tglinethru  25331  tglnne0  25335  tglnpt2  25336  colline  25344  tglowdim2l  25345  tglowdim2ln  25346  mirreu3  25349  miriso  25365  midexlem  25387  isperp  25407  perpcom  25408  perpneq  25409  isperp2  25410  footex  25413  colperpexlem3  25424  opphllem  25427  midex  25429  oppne3  25435  opptgdim2  25437  opphllem2  25440  opphllem3  25441  opphllem5  25443  opphllem6  25444  opphl  25446  outpasch  25447  lnopp2hpgb  25455  colopp  25461  lmieu  25476  trgcopy  25496  trgcopyeu  25498  iscgra1  25502  cgrane1  25504  cgrane2  25505  cgrane3  25506  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgraswap  25512  cgracom  25514  cgratr  25515  cgrabtwn  25517  cgrahl  25518  dfcgra2  25521  sacgr  25522  acopyeu  25525  inaghl  25531  cgrg3col4  25534  f1otrg  25551  f1otrge  25552  axsegcon  25607  axeuclidlem  25642  axcontlem2  25645  upgr1eopALT  25783  usgra1  25902  usgrares1  25939  nbgraf1olem5  25974  pthdepisspth  26104  clwwlkf1  26324  clwwlknscsh  26347  el2spthonot  26397  usg2wotspth  26411  iseupa  26492  eupath2  26507  frgrancvvdeqlem9  26568  friendshipgt3  26648  smcnlem  26936  0lno  27029  ubthlem1  27110  ubthlem3  27112  chocunii  27544  occl  27547  5oalem1  27897  3oalem2  27906  nmopub2tALT  28152  nmfnleub2  28169  lnconi  28276  kbass5  28363  mdslmd1lem1  28568  mdslmd1lem2  28569  cdj1i  28676  disjabrex  28777  disjabrexf  28778  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  fgreu  28854  xrge0infss  28915  xrofsup  28923  2sqmo  28980  ressprs  28986  xrge0addgt0  29022  submarchi  29071  isarchi3  29072  archiabllem1  29078  archiabllem2a  29079  gsumle  29110  suborng  29146  isarchiofld  29148  psgnfzto1stlem  29181  fzto1st1  29183  mdetpmtr1  29217  fimaproj  29228  txomap  29229  qtophaus  29231  cmpcref  29245  pstmxmet  29268  sqsscirc1  29282  ordtrest2NEWlem  29296  ordtconlem1  29298  pnfneige0  29325  lmxrge0  29326  lmdvg  29327  qqhval2  29354  esumcst  29452  esumrnmpt2  29457  esumfsup  29459  esumcvg  29475  esum2d  29482  esumiun  29483  sigaclfu2  29511  insiga  29527  ldsysgenld  29550  ldgenpisyslem1  29553  fiunelros  29564  measinb  29611  imambfm  29651  oms0  29686  omssubadd  29689  carsgclctunlem3  29709  eulerpartlemgvv  29765  dstrvprob  29860  sgnsub  29933  signstfvneq0  29975  afsval  30002  derangenlem  30407  sconpi1  30475  cvmsss2  30510  cvmopnlem  30514  cvmlift3lem7  30561  msrval  30689  ifscgr  31321  cgrxfr  31332  btwnconn1lem13  31376  outsideofeu  31408  neibastop2lem  31525  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem14  32593  poimirlem22  32601  poimirlem29  32608  broucube  32613  heicant  32614  mblfinlem1  32616  itg2addnclem  32631  ftc1cnnc  32654  ftc1anclem7  32661  sstotbnd2  32743  equivtotbnd  32747  isbnd3  32753  ssbnd  32757  totbndbnd  32758  cntotbnd  32765  heibor1lem  32778  rrncmslem  32801  lssats  33317  lsat0cv  33338  lkrlss  33400  lfl1dim  33426  lfl1dim2N  33427  lkrpssN  33468  hlhgt2  33693  3dim2  33772  2dim  33774  lplncvrlvol  33920  paddasslem11  34134  pmapjat1  34157  2polssN  34219  pclfinclN  34254  pexmidlem8N  34281  lhpexle1lem  34311  4atex  34380  ltrnid  34439  trlator0  34476  cdlemg2cex  34897  tendodi1  35090  tendodi2  35091  diblss  35477  dihopelvalcpre  35555  dihatexv  35645  mapdval4N  35939  mzpindd  36327  mzpsubst  36329  mzpcompact2lem  36332  eldioph2b  36344  irrapxlem3  36406  irrapxlem5  36408  pellex  36417  pell1234qrdich  36443  pell14qrexpcl  36449  congabseq  36559  jm2.26a  36585  jm2.26lem3  36586  rmydioph  36599  lnrfg  36708  hbt  36719  rfovcnvf1od  37318  clsk3nimkb  37358  ntrneiiso  37409  ntrneikb  37412  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  4an4132  37726  iunconlem2  38193  fnchoice  38211  cncmpmax  38214  ssinc  38292  ssdec  38293  disjf1  38364  supxrge  38495  suplesup  38496  infxr  38524  infleinf  38529  climrec  38670  climsuse  38675  islptre  38686  addlimc  38715  0ellimcdiv  38716  icccncfext  38773  cncfiooicclem1  38779  fperdvper  38808  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem2  38837  stoweidlem7  38900  stoweidlem34  38927  stoweidlem52  38945  stoweidlem60  38953  wallispilem3  38960  fourierdlem34  39034  fourierdlem38  39038  fourierdlem39  39039  fourierdlem48  39047  fourierdlem50  39049  fourierdlem51  39050  fourierdlem73  39072  fourierdlem76  39075  fourierdlem77  39076  fourierdlem80  39079  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  etransclem32  39159  etransclem33  39160  sge0f1o  39275  sge0pr  39287  sge0isum  39320  iundjiun  39353  meaiininclem  39376  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  smflimlem2  39658  smflimlem4  39660  smfmullem3  39678  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  usgr1eop  40476  pthdepissPth  40941  clwwlksf1  41224  clwwlksnscsh  41247  2pthfrgr  41454  n4cyclfrgr  41461  av-friendshipgt3  41552  mgmhmeql  41593  isrng  41666  2zlidl  41724  lindslinindsimp2  42046  snlindsntor  42054  lincresunit2  42061  islindeps2  42066