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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad3antlr 730	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  frpomin  6372  fsnex  7319  soisoi  7364  f1o2ndf1  8163  fimaproj  8176  fprlem2  8342  tz7.49  8501  omabs  8707  cofon1  8728  naddssim  8741  omxpenlem  9139  fopwdom  9146  findcard3  9346  findcard3OLD  9347  frfi  9349  finsschain  9429  marypha1lem  9502  wemappo  9618  wdomtr  9644  cantnfp1  9750  ttrcltr  9785  harcard  10047  numacn  10118  infunsdom1  10281  sornom  10346  ssfin4  10379  fin1a2lem11  10479  fin1a2lem13  10481  fpwwe2lem12  10711  pwfseq  10733  mulcmpblnr  11140  00id  11465  addrid  11470  cnegex  11471  negeu  11526  add20  11802  ltmul12a  12150  lediv12a  12188  cru  12285  qextltlem  13264  xleadd1a  13315  xmullem  13326  xlemul1a  13350  ixxss12  13427  ioodisj  13542  fvf1tp  13840  fsuppmapnn0fz  14047  seqf1o  14094  mulexpz  14153  leexp1a  14225  faclbnd  14339  swrdswrdlem  14752  abs3lem  15387  rexico  15402  cau3lem  15403  rlim3  15544  ello12  15562  lo1bdd2  15570  elo12  15573  rlimconst  15590  isercoll  15716  climcau  15719  climbdd  15720  summolem2  15764  fsumconst  15838  o1fsum  15861  incexclem  15884  fprodconst  16026  bitsfzo  16481  dvdsmulgcd  16603  pc2dvds  16926  pcz  16928  pcadd  16936  pcfac  16946  vdwmc2  17026  vdwlem2  17029  vdwlem10  17037  vdw  17041  ramcl  17076  sbcie3s  17209  firest  17492  prdsval  17515  mreexd  17700  mreexexlemd  17702  iscat  17730  cidfval  17734  iscatd2  17739  catcocl  17743  catass  17744  catpropd  17767  cidpropd  17768  moni  17797  monpropd  17798  issubc  17899  subccocl  17909  funcco  17935  funcpropd  17967  fullpropd  17987  nati  18023  natpropd  18046  fucpropd  18047  xpcpropd  18278  curfuncf  18308  curf2ndf  18317  yonffthlem  18352  acsfiindd  18623  mgmhmeql  18754  sgrppropd  18769  mndpropd  18797  mhmeql  18861  smndex1mgm  18942  isgrpinv  19033  dfgrp3lem  19078  mhmmnd  19104  cycsubm  19242  cycsubmcom  19244  conjnmzb  19293  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  gass  19341  symgextf  19459  dfod2  19606  gexdvds  19626  sylow3lem2  19670  efgredlem  19789  efgredeu  19794  ghmcmn  19873  oddvdssubg  19897  dprdfcntz  20059  pgpfaclem3  20127  isrng  20181  issrg  20215  isring  20264  dvdsrmul1  20395  issubdrg  20803  islmhm2  21060  lmhmeql  21077  lssacsex  21169  rhmpreimaidl  21310  rhmqusnsg  21318  isphl  21669  uvcf1  21835  lindfmm  21870  sraassab  21911  issubassa2  21935  opsrval  22087  psdmul  22193  scmatmats  22538  smatvscl  22551  mdetunilem7  22645  gsummatr01lem4  22685  m2cpmfo  22783  pmatcollpw3fi1lem1  22813  pm2mpf1lem  22821  pm2mpf1  22826  mp2pm2mplem4  22836  pm2mpghm  22843  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  cctop  23034  neiptoptop  23160  neiptopreu  23162  tgrest  23188  ordtrest2lem  23232  cnss1  23305  cncnp  23309  isnrm3  23388  uncmp  23432  cmpfi  23437  iunconn  23457  1stcrest  23482  subislly  23510  islly2  23513  cldllycmp  23524  lly1stc  23525  llycmpkgen2  23579  kgencn  23585  xkoccn  23648  ptcnplem  23650  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  txconn  23718  regr1lem2  23769  kqreglem1  23770  reghmph  23822  nrmhmph  23823  trfil2  23916  ufileu  23948  flimopn  24004  flimcf  24011  fclscf  24054  ufilcmp  24061  cnpfcf  24070  cnextfun  24093  tgpmulg  24122  symgtgp  24135  tgpt0  24148  qustgplem  24150  ustex2sym  24246  ustex3sym  24247  trust  24259  restutop  24267  restutopopn  24268  ustuqtop4  24274  utop3cls  24281  utopreg  24282  cstucnd  24314  ucncn  24315  trcfilu  24324  neipcfilu  24326  ismet2  24364  metequiv2  24544  metcnp  24575  metcnp2  24576  metcnpi3  24580  txmetcnp  24581  metustto  24587  metustsym  24589  metust  24592  cfilucfil  24593  metuel2  24599  psmetutop  24601  restmetu  24604  metucn  24605  ngptgp  24670  tngngp  24696  nmoleub  24773  icccmp  24866  reconnlem2  24868  reconn  24869  xmetdcn2  24878  metdseq0  24895  metdscn  24897  elcncf2  24935  cncfmet  24954  cnheibor  25006  nmoleub2lem2  25168  nmoleub3  25171  cvsi  25182  iscfil2  25319  iscfil3  25326  cfilfcls  25327  equivcfil  25352  caubl  25361  bcthlem5  25381  pmltpc  25504  ovollb2  25543  ovoliunnul  25561  ovolicc2lem4  25574  volsup  25610  ioorf  25627  dyadss  25648  dyaddisjlem  25649  mbfposr  25706  cncombf  25712  mbflimsup  25720  i1fmulclem  25757  mbfi1fseqlem4  25773  iblss2  25861  ellimc2  25932  ellimc3  25934  dvnadd  25985  dvmptfsum  26033  dvferm1  26043  dvferm2  26045  fta1g  26229  plyeq0lem  26269  plydivex  26357  fta1  26368  aalioulem2  26393  aalioulem3  26394  ulmuni  26453  ulmbdd  26459  ulmdvlem3  26463  mtest  26465  abelthlem8  26501  efopn  26718  cxpmul2z  26751  cxpcn3lem  26808  jensen  27050  lgambdd  27098  lgamucov  27099  isppw2  27176  mersenne  27289  dchrelbas3  27300  dchrptlem1  27326  dchrpt  27329  lgsval2lem  27369  lgsdchrval  27416  lgsquad3  27449  2sqb  27494  2sqmo  27499  pntrsumbnd2  27629  pntpbnd  27650  pntibnd  27655  nosupno  27766  noinfno  27781  noetasuplem4  27799  noetalem1  27804  madebday  27956  cofcutr  27976  negsprop  28085  mulscom  28183  absmuls  28286  remulscl  28452  tgjustr  28500  tglowdim1i  28527  tgbtwndiff  28532  tgifscgr  28534  iscgrglt  28540  tgcgrxfr  28544  lnext  28593  tgbtwnconn1lem3  28600  tgbtwnconn1  28601  legval  28610  legov  28611  legov2  28612  legtrd  28615  legtri3  28616  legso  28625  hlcgrex  28642  hlcgreu  28644  tglnne  28654  tglndim0  28655  tglineeltr  28657  tglinethru  28662  tglnne0  28666  tglnpt2  28667  colline  28675  tglowdim2l  28676  tglowdim2ln  28677  mirreu3  28680  miriso  28696  midexlem  28718  isperp  28738  perpcom  28739  perpneq  28740  isperp2  28741  footexALT  28744  footex  28747  colperpexlem3  28758  opphllem  28761  midex  28763  oppne3  28769  opptgdim2  28771  opphllem2  28774  opphllem3  28775  opphllem5  28777  opphllem6  28778  opphl  28780  outpasch  28781  lnopp2hpgb  28789  colopp  28795  lmieu  28810  trgcopy  28830  trgcopyeu  28832  iscgra1  28836  cgrane1  28838  cgrane2  28839  cgrane3  28840  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  cgrabtwn  28852  cgrahl  28853  dfcgra2  28856  sacgr  28857  acopyeu  28860  inaghl  28871  cgrg3col4  28879  f1otrg  28897  f1otrge  28898  axsegcon  28960  axeuclidlem  28995  upgr1eopALT  29152  usgr1eop  29285  pthdepisspth  29771  wpthswwlks2on  29994  clwwlkf1  30081  clwwlknscsh  30094  2pthfrgr  30316  n4cyclfrgr  30323  frgrwopreglem5  30353  frgrwopreglem5ALT  30354  friendshipgt3  30430  smcnlem  30729  0lno  30822  ubthlem1  30902  ubthlem3  30904  chocunii  31333  occl  31336  5oalem1  31686  3oalem2  31695  nmopub2tALT  31941  nmfnleub2  31958  lnconi  32065  kbass5  32152  mdslmd1lem1  32357  mdslmd1lem2  32358  cdj1i  32465  opreu2reuALT  32505  disjabrex  32604  disjabrexf  32605  2ndresdju  32667  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1lem  32680  fnpreimac  32689  fgreu  32690  suppovss  32697  xrge0infss  32767  xrofsup  32774  fsumiunle  32833  s3f1  32913  ccatf1  32915  ccatws1f1o  32918  swrdf1  32923  ressprs  32936  dfmgc2  32969  mgcf1o  32976  chnind  32983  chnso  32986  xrge0addgt0  33003  mndlrinvb  33011  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  mndlactf1o  33016  gsumle  33074  psgnfzto1stlem  33093  fzto1st1  33095  cycpmco2  33126  cycpmrn  33136  cyc3genpm  33145  cycpmconjs  33149  cyc3conja  33150  submarchi  33166  isarchi3  33167  archiabllem1  33173  archiabllem2a  33174  erler  33237  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rloc1r  33244  subrdom  33254  isdrng4  33264  fracfld  33275  suborng  33310  isarchiofld  33312  imaslmod  33346  dvdsruasso  33378  unitprodclb  33382  nsgqusf1olem2  33407  lmhmqusker  33410  intlidl  33413  rhmquskerlem  33418  elrspunidl  33421  elrspunsn  33422  rhmimaidl  33425  prmidl2  33434  isprmidlc  33440  rhmpreimaprmidl  33444  qsidomlem2  33446  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  ssmxidl  33467  opprqusplusg  33482  opprqusmulr  33484  qsdrngilem  33487  qsdrngi  33488  rsprprmprmidl  33515  rsprprmprmidlb  33516  rprmirred  33524  rprmirredb  33525  rprmdvdspow  33526  rprmdvdsprod  33527  1arithidom  33530  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  dfufd2  33543  zringfrac  33547  ply1dg3rt0irred  33572  r1plmhm  33595  r1pquslmic  33596  lindsunlem  33637  lindsun  33638  dimkerim  33640  fedgmullem1  33642  fedgmul  33644  dimlssid  33645  evls1fldgencl  33680  minplyirred  33704  fldext2chn  33719  constrmon  33734  constrconj  33735  constrfin  33736  constrelextdg2  33737  mdetpmtr1  33769  txomap  33780  qtophaus  33782  cmpcref  33796  zarclsun  33816  zarclssn  33819  zarcmplem  33827  pstmxmet  33843  sqsscirc1  33854  ordtrest2NEWlem  33868  ordtconnlem1  33870  pnfneige0  33897  lmxrge0  33898  lmdvg  33899  qqhval2  33928  esumcst  34027  esumrnmpt2  34032  esumfsup  34034  esumcvg  34050  esum2d  34057  esumiun  34058  sigaclfu2  34085  insiga  34101  ldsysgenld  34124  ldgenpisyslem1  34127  fiunelros  34138  measinb  34185  imambfm  34227  oms0  34262  omssubadd  34265  carsgclctunlem3  34285  eulerpartlemgvv  34341  dstrvprob  34436  sgnsub  34509  signstfvneq0  34549  actfunsnrndisj  34582  reprinfz1  34599  breprexp  34610  afsval  34648  derangenlem  35139  sconnpi1  35207  cvmsss2  35242  cvmopnlem  35246  cvmlift3lem7  35293  msrval  35506  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  outsideofeu  36095  neibastop2lem  36326  weiunso  36432  irrdifflemf  37291  irrdiff  37292  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem14  37594  poimirlem22  37602  poimirlem29  37609  broucube  37614  heicant  37615  mblfinlem1  37617  itg2addnclem  37631  ftc1cnnc  37652  ftc1anclem7  37659  sstotbnd2  37734  equivtotbnd  37738  isbnd3  37744  ssbnd  37748  totbndbnd  37749  cntotbnd  37756  heibor1lem  37769  rrncmslem  37792  lssats  38968  lsat0cv  38989  lkrlss  39051  lfl1dim  39077  lfl1dim2N  39078  lkrpssN  39119  hlhgt2  39346  3dim2  39425  2dim  39427  lplncvrlvol  39573  paddasslem11  39787  pmapjat1  39810  2polssN  39872  pclfinclN  39907  pexmidlem8N  39934  lhpexle1lem  39964  4atex  40033  ltrnid  40092  trlator0  40128  cdlemg2cex  40548  tendodi1  40741  tendodi2  40742  diblss  41127  dihopelvalcpre  41205  dihatexv  41295  mapdval4N  41589  fldhmf1  42047  mndmolinv  42052  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij2  42060  primrootspoweq0  42063  aks6d1c2p2  42076  hashscontpow  42079  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5  42096  sticksstones8  42110  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6isolem1  42131  unitscyglem3  42154  aks5  42161  metakunt1  42162  metakunt2  42163  sn-subeu  42402  sn-0tie0  42415  fiabv  42491  frlmsnic  42495  fsuppind  42545  prjspersym  42562  dffltz  42589  nna4b4nsq  42615  mzpindd  42702  mzpsubst  42704  mzpcompact2lem  42707  eldioph2b  42719  irrapxlem3  42780  irrapxlem5  42782  pellex  42791  pell1234qrdich  42817  pell14qrexpcl  42823  congabseq  42931  jm2.26a  42957  jm2.26lem3  42958  rmydioph  42971  lnrfg  43076  hbt  43087  cantnftermord  43282  cantnfresb  43286  cantnf2  43287  oawordex2  43288  omabs2  43294  tfsconcatfv  43303  tfsconcatrev  43310  ofoaass  43322  nadd2rabtr  43346  nadd1suc  43354  naddgeoa  43356  rfovcnvf1od  43966  clsk3nimkb  44002  ntrneiiso  44053  ntrneikb  44056  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  4an4132  44470  iunconnlem2  44906  fnchoice  44929  cncmpmax  44932  ssinc  44989  ssdec  44990  disjf1  45090  supxrge  45253  suplesup  45254  infxr  45282  infleinf  45287  unb2ltle  45330  rexabslelem  45333  uzub  45346  supminfxr  45379  climrec  45524  climsuse  45529  islptre  45540  addlimc  45569  0ellimcdiv  45570  limsuppnfdlem  45622  limsupub  45625  limsuppnflem  45631  limsupubuz  45634  climinf3  45637  limsupmnflem  45641  climxrre  45671  liminfreuzlem  45723  liminflimsupclim  45728  xlimliminflimsup  45783  icccncfext  45808  cncfiooicclem1  45814  fperdvper  45840  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem2  45868  stoweidlem7  45928  stoweidlem34  45955  stoweidlem52  45973  stoweidlem60  45981  wallispilem3  45988  fourierdlem34  46062  fourierdlem38  46066  fourierdlem39  46067  fourierdlem48  46075  fourierdlem50  46077  fourierdlem51  46078  fourierdlem73  46100  fourierdlem76  46103  fourierdlem77  46104  fourierdlem80  46107  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  etransclem32  46187  etransclem33  46188  sge0f1o  46303  sge0pr  46315  sge0isum  46348  iundjiun  46381  meaiininclem  46407  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  smflimlem2  46693  smflimlem4  46695  smfmullem3  46714  smflimmpt  46731  smfinflem  46738  smfpimne2  46761  fsupdm  46763  finfdm  46767  cfsetsnfsetfo  46975  funressnbrafv2  47159  imasetpreimafvbijlemf1  47278  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  isuspgrim  47759  2zlidl  47963  lindslinindsimp2  48192  snlindsntor  48200  lincresunit2  48207  islindeps2  48212