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 731	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  6313  fsnex  7258  soisoi  7303  f1o2ndf1  8101  fimaproj  8114  fprlem2  8280  tz7.49  8413  omabs  8615  cofon1  8636  naddssim  8649  omxpenlem  9042  fopwdom  9049  findcard3  9229  findcard3OLD  9230  frfi  9232  finsschain  9310  marypha1lem  9384  wemappo  9502  wdomtr  9528  cantnfp1  9634  ttrcltr  9669  harcard  9931  numacn  10002  infunsdom1  10165  sornom  10230  ssfin4  10263  fin1a2lem11  10363  fin1a2lem13  10365  fpwwe2lem12  10595  pwfseq  10617  mulcmpblnr  11024  00id  11349  addrid  11354  cnegex  11355  negeu  11411  add20  11690  ltmul12a  12038  lediv12a  12076  cru  12178  qextltlem  13162  xleadd1a  13213  xmullem  13224  xlemul1a  13248  ixxss12  13326  ioodisj  13443  fvf1tp  13751  fsuppmapnn0fz  13961  seqf1o  14008  mulexpz  14067  leexp1a  14140  faclbnd  14255  swrdswrdlem  14669  abs3lem  15305  rexico  15320  cau3lem  15321  rlim3  15464  ello12  15482  lo1bdd2  15490  elo12  15493  rlimconst  15510  isercoll  15634  climcau  15637  climbdd  15638  summolem2  15682  fsumconst  15756  o1fsum  15779  incexclem  15802  fprodconst  15944  bitsfzo  16405  dvdsmulgcd  16526  pc2dvds  16850  pcz  16852  pcadd  16860  pcfac  16870  vdwmc2  16950  vdwlem2  16953  vdwlem10  16961  vdw  16965  ramcl  17000  sbcie3s  17132  firest  17395  prdsval  17418  mreexd  17603  mreexexlemd  17605  iscat  17633  cidfval  17637  iscatd2  17642  catcocl  17646  catass  17647  catpropd  17670  cidpropd  17671  moni  17698  monpropd  17699  issubc  17797  subccocl  17807  funcco  17833  funcpropd  17864  fullpropd  17884  nati  17920  natpropd  17941  fucpropd  17942  xpcpropd  18169  curfuncf  18199  curf2ndf  18208  yonffthlem  18243  acsfiindd  18512  mgmhmeql  18643  sgrppropd  18658  mndpropd  18686  mhmeql  18753  smndex1mgm  18834  isgrpinv  18925  dfgrp3lem  18970  mhmmnd  18996  cycsubm  19134  cycsubmcom  19136  conjnmzb  19185  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  gass  19233  symgextf  19347  dfod2  19494  gexdvds  19514  sylow3lem2  19558  efgredlem  19677  efgredeu  19682  ghmcmn  19761  oddvdssubg  19785  dprdfcntz  19947  pgpfaclem3  20015  isrng  20063  issrg  20097  isring  20146  dvdsrmul1  20278  issubdrg  20689  islmhm2  20945  lmhmeql  20962  lssacsex  21054  rhmpreimaidl  21187  rhmqusnsg  21195  isphl  21537  uvcf1  21701  lindfmm  21736  sraassab  21777  issubassa2  21801  opsrval  21953  psdmul  22053  scmatmats  22398  smatvscl  22411  mdetunilem7  22505  gsummatr01lem4  22545  m2cpmfo  22643  pmatcollpw3fi1lem1  22673  pm2mpf1lem  22681  pm2mpf1  22686  mp2pm2mplem4  22696  pm2mpghm  22703  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  cctop  22893  neiptoptop  23018  neiptopreu  23020  tgrest  23046  ordtrest2lem  23090  cnss1  23163  cncnp  23167  isnrm3  23246  uncmp  23290  cmpfi  23295  iunconn  23315  1stcrest  23340  subislly  23368  islly2  23371  cldllycmp  23382  lly1stc  23383  llycmpkgen2  23437  kgencn  23443  xkoccn  23506  ptcnplem  23508  pthaus  23525  txhaus  23534  txkgen  23539  xkohaus  23540  xkococnlem  23546  txconn  23576  regr1lem2  23627  kqreglem1  23628  reghmph  23680  nrmhmph  23681  trfil2  23774  ufileu  23806  flimopn  23862  flimcf  23869  fclscf  23912  ufilcmp  23919  cnpfcf  23928  cnextfun  23951  tgpmulg  23980  symgtgp  23993  tgpt0  24006  qustgplem  24008  ustex2sym  24104  ustex3sym  24105  trust  24117  restutop  24125  restutopopn  24126  ustuqtop4  24132  utop3cls  24139  utopreg  24140  cstucnd  24171  ucncn  24172  trcfilu  24181  neipcfilu  24183  ismet2  24221  metequiv2  24398  metcnp  24429  metcnp2  24430  metcnpi3  24434  txmetcnp  24435  metustto  24441  metustsym  24443  metust  24446  cfilucfil  24447  metuel2  24453  psmetutop  24455  restmetu  24458  metucn  24459  ngptgp  24524  tngngp  24542  nmoleub  24619  icccmp  24714  reconnlem2  24716  reconn  24717  xmetdcn2  24726  metdseq0  24743  metdscn  24745  elcncf2  24783  cncfmet  24802  cnheibor  24854  nmoleub2lem2  25016  nmoleub3  25019  cvsi  25030  iscfil2  25166  iscfil3  25173  cfilfcls  25174  equivcfil  25199  caubl  25208  bcthlem5  25228  pmltpc  25351  ovollb2  25390  ovoliunnul  25408  ovolicc2lem4  25421  volsup  25457  ioorf  25474  dyadss  25495  dyaddisjlem  25496  mbfposr  25553  cncombf  25559  mbflimsup  25567  i1fmulclem  25603  mbfi1fseqlem4  25619  iblss2  25707  ellimc2  25778  ellimc3  25780  dvnadd  25831  dvmptfsum  25879  dvferm1  25889  dvferm2  25891  fta1g  26075  plyeq0lem  26115  plydivex  26205  fta1  26216  aalioulem2  26241  aalioulem3  26242  ulmuni  26301  ulmbdd  26307  ulmdvlem3  26311  mtest  26313  abelthlem8  26349  efopn  26567  cxpmul2z  26600  cxpcn3lem  26657  jensen  26899  lgambdd  26947  lgamucov  26948  isppw2  27025  mersenne  27138  dchrelbas3  27149  dchrptlem1  27175  dchrpt  27178  lgsval2lem  27218  lgsdchrval  27265  lgsquad3  27298  2sqb  27343  2sqmo  27348  pntrsumbnd2  27478  pntpbnd  27499  pntibnd  27504  nosupno  27615  noinfno  27630  noetasuplem4  27648  noetalem1  27653  madebday  27811  cofcutr  27832  negsprop  27941  mulscom  28042  absmuls  28146  zs12ge0  28342  remulscl  28353  tgjustr  28401  tglowdim1i  28428  tgbtwndiff  28433  tgifscgr  28435  iscgrglt  28441  tgcgrxfr  28445  lnext  28494  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  legval  28511  legov  28512  legov2  28513  legtrd  28516  legtri3  28517  legso  28526  hlcgrex  28543  hlcgreu  28545  tglnne  28555  tglndim0  28556  tglineeltr  28558  tglinethru  28563  tglnne0  28567  tglnpt2  28568  colline  28576  tglowdim2l  28577  tglowdim2ln  28578  mirreu3  28581  miriso  28597  midexlem  28619  isperp  28639  perpcom  28640  perpneq  28641  isperp2  28642  footexALT  28645  footex  28648  colperpexlem3  28659  opphllem  28662  midex  28664  oppne3  28670  opptgdim2  28672  opphllem2  28675  opphllem3  28676  opphllem5  28678  opphllem6  28679  opphl  28681  outpasch  28682  lnopp2hpgb  28690  colopp  28696  lmieu  28711  trgcopy  28731  trgcopyeu  28733  iscgra1  28737  cgrane1  28739  cgrane2  28740  cgrane3  28741  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  cgrabtwn  28753  cgrahl  28754  dfcgra2  28757  sacgr  28758  acopyeu  28761  inaghl  28772  cgrg3col4  28780  f1otrg  28798  f1otrge  28799  axsegcon  28854  axeuclidlem  28889  upgr1eopALT  29044  usgr1eop  29177  pthdepisspth  29665  wpthswwlks2on  29891  clwwlkf1  29978  clwwlknscsh  29991  2pthfrgr  30213  n4cyclfrgr  30220  frgrwopreglem5  30250  frgrwopreglem5ALT  30251  friendshipgt3  30327  smcnlem  30626  0lno  30719  ubthlem1  30799  ubthlem3  30801  chocunii  31230  occl  31233  5oalem1  31583  3oalem2  31592  nmopub2tALT  31838  nmfnleub2  31855  lnconi  31962  kbass5  32049  mdslmd1lem1  32254  mdslmd1lem2  32255  cdj1i  32362  opreu2reuALT  32406  disjabrex  32511  disjabrexf  32512  2ndresdju  32573  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  fnpreimac  32595  fgreu  32596  suppovss  32604  xrge0infss  32683  xrofsup  32690  elq2  32736  fsumiunle  32754  sgnsub  32762  2exple2exp  32770  s3f1  32868  ccatf1  32870  ccatws1f1o  32873  swrdf1  32878  ressprs  32890  dfmgc2  32922  mgcf1o  32929  chnind  32937  chnso  32940  xrge0addgt0  32958  mndlrinvb  32966  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  mndlactf1o  32971  gsumfs2d  32995  gsumwun  33005  gsumwrd2dccatlem  33006  gsumle  33038  psgnfzto1stlem  33057  fzto1st1  33059  cycpmco2  33090  cycpmrn  33100  cyc3genpm  33109  cycpmconjs  33113  cyc3conja  33114  conjga  33127  submarchi  33140  isarchi3  33141  archiabllem1  33147  archiabllem2a  33148  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  erler  33216  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rloc1r  33223  subrdom  33235  isdrng4  33245  fracfld  33258  suborng  33293  isarchiofld  33295  imaslmod  33324  dvdsruasso  33356  unitprodclb  33360  nsgqusf1olem2  33385  lmhmqusker  33388  intlidl  33391  rhmquskerlem  33396  elrspunidl  33399  elrspunsn  33400  rhmimaidl  33403  prmidl2  33412  isprmidlc  33418  rhmpreimaprmidl  33422  qsidomlem2  33424  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  ssmxidl  33445  opprqusplusg  33460  opprqusmulr  33462  qsdrngilem  33465  qsdrngi  33466  rsprprmprmidl  33493  rsprprmprmidlb  33494  rprmirred  33502  rprmirredb  33503  rprmdvdspow  33504  rprmdvdsprod  33505  1arithidom  33508  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  dfufd2  33521  zringfrac  33525  ply1dg3rt0irred  33551  r1plmhm  33575  r1pquslmic  33576  exsslsb  33592  lindsunlem  33620  lindsun  33621  dimkerim  33623  fedgmullem1  33625  fedgmul  33627  dimlssid  33628  evls1fldgencl  33665  fldextrspunlsplem  33668  minplyirred  33701  fldext2chn  33718  constrmon  33734  constrconj  33735  constrfin  33736  constrelextdg2  33737  constrextdg2lem  33738  constrextdg2  33739  constrext2chnlem  33740  constrfiss  33741  cos9thpiminplylem2  33773  mdetpmtr1  33813  txomap  33824  qtophaus  33826  cmpcref  33840  zarclsun  33860  zarclssn  33863  zarcmplem  33871  pstmxmet  33887  sqsscirc1  33898  ordtrest2NEWlem  33912  ordtconnlem1  33914  pnfneige0  33941  lmxrge0  33942  lmdvg  33943  qqhval2  33972  esumcst  34053  esumrnmpt2  34058  esumfsup  34060  esumcvg  34076  esum2d  34083  esumiun  34084  sigaclfu2  34111  insiga  34127  ldsysgenld  34150  ldgenpisyslem1  34153  fiunelros  34164  measinb  34211  imambfm  34253  oms0  34288  omssubadd  34291  carsgclctunlem3  34311  eulerpartlemgvv  34367  dstrvprob  34463  signstfvneq0  34563  actfunsnrndisj  34596  reprinfz1  34613  breprexp  34624  afsval  34662  derangenlem  35158  sconnpi1  35226  cvmsss2  35261  cvmopnlem  35265  cvmlift3lem7  35312  msrval  35525  ifscgr  36032  cgrxfr  36043  btwnconn1lem13  36087  outsideofeu  36119  neibastop2lem  36348  weiunso  36454  irrdifflemf  37313  irrdiff  37314  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem14  37628  poimirlem22  37636  poimirlem29  37643  broucube  37648  heicant  37649  mblfinlem1  37651  itg2addnclem  37665  ftc1cnnc  37686  ftc1anclem7  37693  sstotbnd2  37768  equivtotbnd  37772  isbnd3  37778  ssbnd  37782  totbndbnd  37783  cntotbnd  37790  heibor1lem  37803  rrncmslem  37826  lssats  39005  lsat0cv  39026  lkrlss  39088  lfl1dim  39114  lfl1dim2N  39115  lkrpssN  39156  hlhgt2  39383  3dim2  39462  2dim  39464  lplncvrlvol  39610  paddasslem11  39824  pmapjat1  39847  2polssN  39909  pclfinclN  39944  pexmidlem8N  39971  lhpexle1lem  40001  4atex  40070  ltrnid  40129  trlator0  40165  cdlemg2cex  40585  tendodi1  40778  tendodi2  40779  diblss  41164  dihopelvalcpre  41242  dihatexv  41332  mapdval4N  41626  fldhmf1  42078  mndmolinv  42083  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij2  42091  primrootspoweq0  42094  aks6d1c2p2  42107  hashscontpow  42110  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5  42127  sticksstones8  42141  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6isolem1  42162  unitscyglem3  42185  aks5  42192  sn-subeu  42415  sn-0tie0  42439  fiabv  42524  frlmsnic  42528  fsuppind  42578  prjspersym  42595  dffltz  42622  nna4b4nsq  42648  mzpindd  42734  mzpsubst  42736  mzpcompact2lem  42739  eldioph2b  42751  irrapxlem3  42812  irrapxlem5  42814  pellex  42823  pell1234qrdich  42849  pell14qrexpcl  42855  congabseq  42963  jm2.26a  42989  jm2.26lem3  42990  rmydioph  43003  lnrfg  43108  hbt  43119  cantnftermord  43309  cantnfresb  43313  cantnf2  43314  oawordex2  43315  omabs2  43321  tfsconcatfv  43330  tfsconcatrev  43337  ofoaass  43349  nadd2rabtr  43373  nadd1suc  43381  naddgeoa  43383  rfovcnvf1od  43993  clsk3nimkb  44029  ntrneiiso  44080  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  4an4132  44489  iunconnlem2  44924  modelaxrep  44971  fnchoice  45023  cncmpmax  45026  ssinc  45081  ssdec  45082  disjf1  45177  supxrge  45334  suplesup  45335  infxr  45363  infleinf  45368  unb2ltle  45411  rexabslelem  45414  uzub  45427  supminfxr  45460  climrec  45601  climsuse  45606  islptre  45617  addlimc  45646  0ellimcdiv  45647  limsuppnfdlem  45699  limsupub  45702  limsuppnflem  45708  limsupubuz  45711  climinf3  45714  limsupmnflem  45718  climxrre  45748  liminfreuzlem  45800  liminflimsupclim  45805  xlimliminflimsup  45860  icccncfext  45885  cncfiooicclem1  45891  fperdvper  45917  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem2  45945  stoweidlem7  46005  stoweidlem34  46032  stoweidlem52  46050  stoweidlem60  46058  wallispilem3  46065  fourierdlem34  46139  fourierdlem38  46143  fourierdlem39  46144  fourierdlem48  46152  fourierdlem50  46154  fourierdlem51  46155  fourierdlem73  46177  fourierdlem76  46180  fourierdlem77  46181  fourierdlem80  46184  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  etransclem32  46264  etransclem33  46265  sge0f1o  46380  sge0pr  46392  sge0isum  46425  iundjiun  46458  meaiininclem  46484  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  smflimlem2  46770  smflimlem4  46772  smfmullem3  46791  smflimmpt  46808  smfinflem  46815  smfpimne2  46838  fsupdm  46840  finfdm  46844  cfsetsnfsetfo  47061  funressnbrafv2  47245  imasetpreimafvbijlemf1  47405  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  isuspgrim  47896  stgrusgra  47958  isubgr3stgrlem6  47970  2zlidl  48228  lindslinindsimp2  48452  snlindsntor  48460  lincresunit2  48467  islindeps2  48472  imaf1co  49144  imasubc3  49145  fucofvalg  49307  fuco21  49325  precofvalALT  49357  lanfval  49602  ranfval  49603