Theorem simpllr 781

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 737	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  frpomin  6298  fsnex  7234  soisoi  7279  f1o2ndf1  8068  fimaproj  8082  fprlem2  8248  tz7.49  8381  omabs  8584  cofon1  8605  naddssim  8618  omxpenlem  9013  fopwdom  9020  findcard3  9190  frfi  9192  finsschain  9266  marypha1lem  9343  wemappo  9461  wdomtr  9487  cantnfp1  9600  ttrcltr  9635  harcard  9900  numacn  9969  infunsdom1  10132  sornom  10197  ssfin4  10230  fin1a2lem11  10330  fin1a2lem13  10332  fpwwe2lem12  10563  pwfseq  10585  mulcmpblnr  10992  00id  11319  addrid  11324  cnegex  11325  negeu  11381  add20  11660  ltmul12a  12009  lediv12a  12047  cru  12149  qextltlem  13152  xleadd1a  13203  xmullem  13214  xlemul1a  13238  ixxss12  13316  ioodisj  13433  fvf1tp  13746  fsuppmapnn0fz  13956  seqf1o  14003  mulexpz  14062  leexp1a  14135  faclbnd  14250  swrdswrdlem  14664  abs3lem  15299  rexico  15314  cau3lem  15315  rlim3  15458  ello12  15476  lo1bdd2  15484  elo12  15487  rlimconst  15504  isercoll  15628  climcau  15631  climbdd  15632  summolem2  15676  fsumconst  15750  o1fsum  15774  incexclem  15799  fprodconst  15941  bitsfzo  16402  dvdsmulgcd  16523  pc2dvds  16848  pcz  16850  pcadd  16858  pcfac  16868  vdwmc2  16948  vdwlem2  16951  vdwlem10  16959  vdw  16963  ramcl  16998  sbcie3s  17130  firest  17393  prdsval  17416  mreexd  17606  mreexexlemd  17608  iscat  17636  cidfval  17640  iscatd2  17645  catcocl  17649  catass  17650  catpropd  17673  cidpropd  17674  moni  17701  monpropd  17702  issubc  17800  subccocl  17810  funcco  17836  funcpropd  17867  fullpropd  17887  nati  17923  natpropd  17944  fucpropd  17945  xpcpropd  18172  curfuncf  18202  curf2ndf  18211  yonffthlem  18246  acsfiindd  18517  chnind  18585  chnso  18588  mgmhmeql  18682  sgrppropd  18697  mndpropd  18725  mhmeql  18792  smndex1mgm  18876  isgrpinv  18967  dfgrp3lem  19012  mhmmnd  19038  cycsubm  19175  cycsubmcom  19177  conjnmzb  19226  ghmqusnsg  19255  ghmquskerlem3  19259  ghmqusker  19260  gass  19274  symgextf  19390  dfod2  19537  gexdvds  19557  sylow3lem2  19601  efgredlem  19720  efgredeu  19725  ghmcmn  19804  oddvdssubg  19828  dprdfcntz  19990  pgpfaclem3  20058  gsumle  20118  isrng  20133  issrg  20167  isring  20216  dvdsrmul1  20347  issubdrg  20759  suborng  20855  islmhm2  21035  lmhmeql  21052  lssacsex  21144  rhmpreimaidl  21277  rhmqusnsg  21285  isphl  21610  uvcf1  21774  lindfmm  21809  sraassab  21850  issubassa2  21874  opsrval  22029  psdmul  22161  scmatmats  22501  smatvscl  22514  mdetunilem7  22608  gsummatr01lem4  22648  m2cpmfo  22746  pmatcollpw3fi1lem1  22776  pm2mpf1lem  22784  pm2mpf1  22789  mp2pm2mplem4  22799  pm2mpghm  22806  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  cctop  22996  neiptoptop  23121  neiptopreu  23123  tgrest  23149  ordtrest2lem  23193  cnss1  23266  cncnp  23270  isnrm3  23349  uncmp  23393  cmpfi  23398  iunconn  23418  1stcrest  23443  subislly  23471  islly2  23474  cldllycmp  23485  lly1stc  23486  llycmpkgen2  23540  kgencn  23546  xkoccn  23609  ptcnplem  23611  pthaus  23628  txhaus  23637  txkgen  23642  xkohaus  23643  xkococnlem  23649  txconn  23679  regr1lem2  23730  kqreglem1  23731  reghmph  23783  nrmhmph  23784  trfil2  23877  ufileu  23909  flimopn  23965  flimcf  23972  fclscf  24015  ufilcmp  24022  cnpfcf  24031  cnextfun  24054  tgpmulg  24083  symgtgp  24096  tgpt0  24109  qustgplem  24111  ustex2sym  24207  ustex3sym  24208  trust  24219  restutop  24227  restutopopn  24228  ustuqtop4  24234  utop3cls  24241  utopreg  24242  cstucnd  24273  ucncn  24274  trcfilu  24283  neipcfilu  24285  ismet2  24323  metequiv2  24500  metcnp  24531  metcnp2  24532  metcnpi3  24536  txmetcnp  24537  metustto  24543  metustsym  24545  metust  24548  cfilucfil  24549  metuel2  24555  psmetutop  24557  restmetu  24560  metucn  24561  ngptgp  24626  tngngp  24644  nmoleub  24721  icccmp  24816  reconnlem2  24818  reconn  24819  xmetdcn2  24828  metdseq0  24845  metdscn  24847  elcncf2  24882  cncfmet  24901  cnheibor  24947  nmoleub2lem2  25108  nmoleub3  25111  cvsi  25122  iscfil2  25258  iscfil3  25265  cfilfcls  25266  equivcfil  25291  caubl  25300  bcthlem5  25320  pmltpc  25442  ovollb2  25481  ovoliunnul  25499  ovolicc2lem4  25512  volsup  25548  ioorf  25565  dyadss  25586  dyaddisjlem  25587  mbfposr  25644  cncombf  25650  mbflimsup  25658  i1fmulclem  25694  mbfi1fseqlem4  25710  iblss2  25798  ellimc2  25869  ellimc3  25871  dvnadd  25921  dvmptfsum  25967  dvferm1  25977  dvferm2  25979  fta1g  26160  plyeq0lem  26200  plydivex  26288  fta1  26299  aalioulem2  26324  aalioulem3  26325  ulmuni  26382  ulmbdd  26388  ulmdvlem3  26392  mtest  26394  abelthlem8  26429  efopn  26647  cxpmul2z  26680  cxpcn3lem  26736  jensen  26977  lgambdd  27025  lgamucov  27026  isppw2  27103  mersenne  27215  dchrelbas3  27226  dchrptlem1  27252  dchrpt  27255  lgsval2lem  27295  lgsdchrval  27342  lgsquad3  27375  2sqb  27420  2sqmo  27425  pntrsumbnd2  27555  pntpbnd  27576  pntibnd  27581  nosupno  27692  noinfno  27707  noetasuplem4  27725  noetalem1  27730  madebday  27917  cofcutr  27941  negsprop  28052  mulscom  28156  absmuls  28261  addonbday  28296  bdayfinbndlem1  28484  z12sge0  28500  remulscl  28519  tgjustr  28567  tglowdim1i  28594  tgbtwndiff  28599  tgifscgr  28601  iscgrglt  28607  tgcgrxfr  28611  lnext  28660  tgbtwnconn1lem3  28667  tgbtwnconn1  28668  legval  28677  legov  28678  legov2  28679  legtrd  28682  legtri3  28683  legso  28692  hlcgrex  28709  hlcgreu  28711  tglnne  28721  tglndim0  28722  tglineeltr  28724  tglinethru  28729  tglnne0  28733  tglnpt2  28734  colline  28742  tglowdim2l  28743  tglowdim2ln  28744  mirreu3  28747  miriso  28763  midexlem  28785  isperp  28805  perpcom  28806  perpneq  28807  isperp2  28808  footexALT  28811  footex  28814  colperpexlem3  28825  opphllem  28828  midex  28830  oppne3  28836  opptgdim2  28838  opphllem2  28841  opphllem3  28842  opphllem5  28844  opphllem6  28845  opphl  28847  outpasch  28848  lnopp2hpgb  28856  colopp  28862  lmieu  28877  trgcopy  28897  trgcopyeu  28899  iscgra1  28903  cgrane1  28905  cgrane2  28906  cgrane3  28907  cgrahl1  28909  cgrahl2  28910  cgracgr  28911  cgraswap  28913  cgracom  28915  cgratr  28916  flatcgra  28917  cgrabtwn  28919  cgrahl  28920  dfcgra2  28923  sacgr  28924  acopyeu  28927  inaghl  28938  cgrg3col4  28946  f1otrg  28964  f1otrge  28965  axsegcon  29021  axeuclidlem  29056  upgr1eopALT  29211  usgr1eop  29344  pthdepisspth  29828  wpthswwlks2on  30057  clwwlkf1  30144  clwwlknscsh  30157  2pthfrgr  30379  n4cyclfrgr  30386  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  friendshipgt3  30493  smcnlem  30793  0lno  30886  ubthlem1  30966  ubthlem3  30968  chocunii  31397  occl  31400  5oalem1  31750  3oalem2  31759  nmopub2tALT  32005  nmfnleub2  32022  lnconi  32129  kbass5  32216  mdslmd1lem1  32421  mdslmd1lem2  32422  cdj1i  32529  opreu2reuALT  32571  disjabrex  32678  disjabrexf  32679  2ndresdju  32748  acunirnmpt  32758  acunirnmpt2  32759  acunirnmpt2f  32760  aciunf1lem  32761  fnpreimac  32769  fgreu  32770  suppovss  32780  xrge0infss  32859  xrofsup  32866  elq2  32911  fsumiunle  32928  sgnsub  32936  2exple2exp  32944  s3f1  33033  ccatf1  33035  ccatws1f1o  33037  swrdf1  33042  ressprs  33052  dfmgc2  33082  mgcf1o  33089  xrge0addgt0  33103  mndlrinvb  33111  mndlactf1  33112  mndlactfo  33113  mndractf1  33114  mndractfo  33115  mndlactf1o  33116  gsumfs2d  33149  suppgsumssiun  33160  gsumwun  33164  gsumwrd2dccatlem  33165  psgnfzto1stlem  33188  fzto1st1  33190  cycpmco2  33221  cycpmrn  33231  cyc3genpm  33240  cycpmconjs  33244  cyc3conja  33245  conjga  33258  fxpsubrg  33262  submarchi  33274  isarchi3  33275  archiabllem1  33281  archiabllem2a  33282  isarchiofld  33287  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem2  33336  erler  33353  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rloc1r  33360  subrdom  33373  ricdomn1  33377  isdrng4  33386  fracfld  33399  imaslmod  33443  dvdsruasso  33475  unitprodclb  33479  nsgqusf1olem2  33504  lmhmqusker  33507  intlidl  33510  rhmquskerlem  33515  elrspunidl  33518  elrspunsn  33519  rhmimaidl  33522  prmidl2  33531  isprmidlc  33537  rhmpreimaprmidl  33541  qsidomlem2  33543  ssdifidllem  33546  ssdifidlprm  33548  mxidlprm  33560  ssmxidl  33564  opprqusplusg  33579  opprqusmulr  33581  qsdrngilem  33584  qsdrngi  33585  rsprprmprmidl  33612  rsprprmprmidlb  33613  rprmirred  33621  rprmirredb  33622  rprmdvdspow  33623  rprmdvdsprod  33624  1arithidom  33627  1arithufdlem2  33635  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  dfufd2  33640  zringfrac  33644  deg1prod  33673  ply1dg3rt0irred  33674  r1plmhm  33700  r1pquslmic  33701  0mplrim  33705  mplidomlem  33718  extvfvcl  33727  mplmulmvr  33730  mplvrpmga  33736  psrgsum  33739  psrmonprod  33743  esplyfval3  33763  esplyfval1  33764  esplyfvaln  33765  esplyind  33766  exsslsb  33788  lindsunlem  33815  lindsun  33816  dimkerim  33818  fedgmullem1  33820  fedgmul  33822  dimlssid  33823  evls1fldgencl  33861  fldextrspunlsplem  33864  extdgfialg  33885  minplyirred  33902  fldext2chn  33919  constrmon  33935  constrconj  33936  constrfin  33937  constrelextdg2  33938  constrextdg2lem  33939  constrextdg2  33940  constrext2chnlem  33941  constrfiss  33942  cos9thpiminplylem2  33974  mdetpmtr1  34014  txomap  34025  qtophaus  34027  cmpcref  34041  zarclsun  34061  zarclssn  34064  zarcmplem  34072  pstmxmet  34088  sqsscirc1  34099  ordtrest2NEWlem  34113  ordtconnlem1  34115  pnfneige0  34142  lmxrge0  34143  lmdvg  34144  qqhval2  34173  esumcst  34254  esumrnmpt2  34259  esumfsup  34261  esumcvg  34277  esum2d  34284  esumiun  34285  sigaclfu2  34312  insiga  34328  ldsysgenld  34351  ldgenpisyslem1  34354  fiunelros  34365  measinb  34412  imambfm  34453  oms0  34488  omssubadd  34491  carsgclctunlem3  34511  eulerpartlemgvv  34567  dstrvprob  34663  signstfvneq0  34763  actfunsnrndisj  34796  reprinfz1  34813  breprexp  34824  afsval  34862  derangenlem  35406  sconnpi1  35474  cvmsss2  35509  cvmopnlem  35513  cvmlift3lem7  35560  msrval  35773  ifscgr  36279  cgrxfr  36290  btwnconn1lem13  36334  outsideofeu  36366  neibastop2lem  36595  weiunso  36701  irrdifflemf  37692  irrdiff  37693  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem14  38008  poimirlem22  38016  poimirlem29  38023  broucube  38028  heicant  38029  mblfinlem1  38031  itg2addnclem  38045  ftc1cnnc  38066  ftc1anclem7  38073  sstotbnd2  38148  equivtotbnd  38152  isbnd3  38158  ssbnd  38162  totbndbnd  38163  cntotbnd  38170  heibor1lem  38183  rrncmslem  38206  lssats  39511  lsat0cv  39532  lkrlss  39594  lfl1dim  39620  lfl1dim2N  39621  lkrpssN  39662  hlhgt2  39888  3dim2  39967  2dim  39969  lplncvrlvol  40115  paddasslem11  40329  pmapjat1  40352  2polssN  40414  pclfinclN  40449  pexmidlem8N  40476  lhpexle1lem  40506  4atex  40575  ltrnid  40634  trlator0  40670  cdlemg2cex  41090  tendodi1  41283  tendodi2  41284  diblss  41669  dihopelvalcpre  41747  dihatexv  41837  mapdval4N  42131  fldhmf1  42582  mndmolinv  42587  primrootscoprmpow  42591  posbezout  42592  primrootscoprbij2  42595  primrootspoweq0  42598  aks6d1c2p2  42611  hashscontpow  42614  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c5  42631  sticksstones8  42645  sticksstones12  42650  sticksstones22  42660  aks6d1c6lem3  42664  aks6d1c6isolem1  42666  unitscyglem3  42689  aks5  42696  sn-subeu  42911  sn-0tie0  42948  fiabv  43029  frlmsnic  43033  fsuppind  43047  prjspersym  43064  dffltz  43091  nna4b4nsq  43117  mzpindd  43202  mzpsubst  43204  mzpcompact2lem  43207  eldioph2b  43219  irrapxlem3  43276  irrapxlem5  43278  pellex  43287  pell1234qrdich  43313  pell14qrexpcl  43319  congabseq  43426  jm2.26a  43452  jm2.26lem3  43453  rmydioph  43466  lnrfg  43571  hbt  43582  cantnftermord  43772  cantnfresb  43776  cantnf2  43777  oawordex2  43778  omabs2  43784  tfsconcatfv  43793  tfsconcatrev  43800  ofoaass  43812  nadd2rabtr  43836  nadd1suc  43844  naddgeoa  43846  rfovcnvf1od  44455  clsk3nimkb  44491  ntrneiiso  44542  ntrneikb  44545  ntrneixb  44546  ntrneik3  44547  ntrneix3  44548  ntrneik13  44549  ntrneix13  44550  4an4132  44950  iunconnlem2  45385  modelaxrep  45432  fnchoice  45484  cncmpmax  45487  ssinc  45541  ssdec  45542  disjf1  45637  supxrge  45790  suplesup  45791  infxr  45818  infleinf  45823  unb2ltle  45865  rexabslelem  45868  uzub  45881  supminfxr  45914  climrec  46055  climsuse  46060  islptre  46071  addlimc  46098  0ellimcdiv  46099  limsuppnfdlem  46151  limsupub  46154  limsuppnflem  46160  limsupubuz  46163  climinf3  46166  limsupmnflem  46170  climxrre  46200  liminfreuzlem  46252  liminflimsupclim  46257  xlimliminflimsup  46312  icccncfext  46337  cncfiooicclem1  46343  fperdvper  46369  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvmptfprodlem  46394  dvmptfprod  46395  dvnprodlem2  46397  stoweidlem7  46457  stoweidlem34  46484  stoweidlem52  46502  stoweidlem60  46510  wallispilem3  46517  fourierdlem34  46591  fourierdlem38  46595  fourierdlem39  46596  fourierdlem48  46604  fourierdlem50  46606  fourierdlem51  46607  fourierdlem73  46629  fourierdlem76  46632  fourierdlem77  46633  fourierdlem80  46636  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  etransclem32  46716  etransclem33  46717  sge0f1o  46832  sge0pr  46844  sge0isum  46877  iundjiun  46910  meaiininclem  46936  hoicvr  46998  pimdecfgtioo  47167  pimincfltioo  47168  preimageiingt  47170  preimaleiinlt  47171  smflimlem2  47222  smflimlem4  47224  smfmullem3  47243  smflimmpt  47260  smfinflem  47267  smfpimne2  47290  fsupdm  47292  finfdm  47296  cfsetsnfsetfo  47530  funressnbrafv2  47714  imasetpreimafvbijlemf1  47886  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbnd  48307  isuspgrim  48394  stgrusgra  48457  isubgr3stgrlem6  48469  2zlidl  48738  lindslinindsimp2  48961  snlindsntor  48969  lincresunit2  48976  islindeps2  48981  imaf1co  49652  imasubc3  49653  fucofvalg  49815  fuco21  49833  precofvalALT  49865  lanfval  50110  ranfval  50111