Theorem simpr2 1196

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simpr2

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜒)
2	1	3ad2antr2 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  simpr12  1259  simpr22  1262  simpr32  1265  simp1r2  1271  simp2r2  1277  simp3r2  1283  3anandis  1473  fpr2g  7154  isopolem  7288  fr3nr  7714  sexp3  8092  dif1en  9081  frfi  9179  intrnfi  9310  fisupcl  9364  cnfcomlem  9599  ackbij1lem15  10134  cofsmo  10170  sornom  10178  fpwwe2lem4  10535  dedekindle  11287  supmul1  12101  eluzuzle  12751  xlesubadd  13172  elioc2  13319  elico2  13320  elicc2  13321  fseq1p1m1  13508  fz0fzelfz0  13544  hash7g  14403  swrdsbslen  14582  ccatswrd  14586  swrdswrdlem  14621  wwlktovf1  14874  tanadd  16086  dvds2ln  16210  cshwsidrepsw  17015  ressress  17168  f1ovscpbl  17440  mreexexlem4d  17563  mreexexd  17564  iscatd2  17597  2oppccomf  17641  issubc3  17766  fthmon  17846  fuccocl  17884  fucidcl  17885  invfuc  17894  initoeu2lem0  17930  initoeu2lem1  17931  curf2cl  18147  yonedalem4c  18193  yonedalem3  18196  pospo  18259  latjle12  18366  latjlej1  18369  latnlej2  18375  latlem12  18382  latmlem1  18385  latledi  18393  latjass  18399  latj12  18400  latj32  18401  latj13  18402  latj31  18403  latjrot  18404  latjjdi  18407  latjjdir  18408  latdisdlem  18412  prdssgrpd  18651  prdsmndd  18688  mndissubm  18725  frmdmnd  18777  grpsubrcan  18944  grpsubadd  18951  grpaddsubass  18953  grpsubsub4  18956  grppnpcan2  18957  grpnpncan  18958  mulgnndir  19026  mulgnn0dir  19027  mulgdir  19029  mulgnnass  19032  mulgnn0ass  19033  mulgass  19034  mulgsubdir  19037  pwsmulg  19042  issubg2  19064  eqgval  19099  qusgrp  19108  galcan  19226  gacan  19227  oppgmnd  19276  fvcosymgeq  19351  pmtrprfv  19375  psgnunilem3  19418  cmn32  19722  cmn12  19724  abladdsub  19734  ablsubaddsub  19736  ablsubsub23  19746  mulgdi  19748  mulgsubdi  19751  dprdss  19953  dprdz  19954  dprdf1o  19956  dprdsn  19960  dprd2da  19966  dmdprdsplit  19971  ablfac1b  19994  pgpfac1lem5  20003  prdsrngd  20104  srgdilem  20120  srgbinom  20159  ringdilem  20177  prdsringd  20249  opprrng  20273  mulgass3  20281  dvrass  20336  dvrdir  20340  subrgunit  20515  issubrg2  20517  isdomn4  20641  abvdiv  20754  lsssn0  20891  islss3  20902  prdslmodd  20912  islmhm2  20982  lspsolv  21090  islbs2  21101  islbs3  21102  lbsextlem4  21108  sralmod  21131  rnglidl1  21179  psgndiflemB  21547  ipdir  21586  ipdi  21587  ipsubdir  21589  ipsubdi  21590  ipass  21592  ipassr  21593  ipassr2  21594  isphld  21601  ocvlss  21619  sraassab  21815  sraassaOLD  21817  psrgrpOLD  21904  psrlmod  21907  psrring  21917  psrassa  21920  mamudm  22320  matring  22368  matassa  22369  ofco2  22376  ma1repveval  22496  mdetunilem1  22537  mdetunilem9  22545  chpscmatgsumbin  22769  iinopn  22827  restopnb  23100  subbascn  23179  nrmsep2  23281  isnrm3  23284  regsep2  23301  dnsconst  23303  dfconn2  23344  1stcelcls  23386  dislly  23422  ptuni2  23501  tx1stc  23575  0nelfb  23756  infil  23788  fsubbas  23792  filssufilg  23836  hauspwpwf1  23912  cnextcn  23992  tmdcn2  24014  ustuqtoplem  24164  utopsnneiplem  24172  psmettri  24236  isxmet2d  24252  xmettri  24276  xmetres2  24286  bldisj  24323  blss2ps  24328  blss2  24329  xmstri2  24391  mstri2  24392  xmstri  24393  mstri  24394  xmstri3  24395  mstri3  24396  msrtri  24397  comet  24438  stdbdbl  24442  met2ndci  24447  ngprcan  24535  ngplcan  24536  ngpsubcan  24539  nmtri2  24552  nrgdsdi  24590  nrgdsdir  24591  nlmdsdi  24606  nlmdsdir  24607  blcvx  24723  icoopnst  24873  pi1grplem  24986  clmpm1dir  25040  cmodscmulexp  25059  cvsdiv  25069  cvsdivcl  25070  cphdivcl  25119  cphsubdir  25145  cphsubdi  25146  tcphcph  25174  bcthlem5  25265  volfiniun  25485  volcn  25544  itg1val2  25622  dvconst  25855  dvlip  25935  ftc1a  25981  ulmval  26326  ulmdvlem3  26348  ang180  26761  cvxcl  26932  scvxcvx  26933  sgmmul  27149  dchrabl  27202  gausslemma2dlem1a  27313  nosupbnd1  27663  noinfbnd1lem5  27676  noinfbnd1  27678  ssltss2  27739  addscom  27919  addsbday  27970  motgrp  28531  iscgra1  28798  cgrane1  28800  cgrane3  28802  cgrahl1  28804  cgrahl2  28805  cgracgr  28806  cgratr  28811  cgrabtwn  28814  cgrahl  28815  dfcgra2  28818  sacgr  28819  f1otrge  28860  colinearalglem1  28895  axcgrtr  28904  axeuclidlem  28951  axcontlem3  28955  axcontlem4  28956  axcontlem7  28959  eengtrkg  28975  eengtrkge  28976  edglnl  29132  subgruhgredgd  29273  nbfusgrlevtxm2  29367  lfgriswlk  29676  wwlknbp1  29833  usgrwwlks2on  29947  umgrwwlks2on  29948  rusgrnumwwlks  29966  clwlkclwwlkfo  30000  3spthd  30167  3vfriswmgr  30269  frgr2wwlkeqm  30322  numclwwlk1lem2f  30346  numclwwlk2  30372  numclwwlk3  30376  numclwwlk5  30379  grpomuldivass  30532  ablomuldiv  30543  ablodivdiv4  30545  ablonnncan1  30548  nvmdi  30639  dipassr  30837  archiabllem2c  33175  dvrcan5  33214  rloccring  33248  reofld  33319  eqgvscpbl  33326  qusvsval  33328  quslmod  33334  quslmhm  33335  prmidlc  33424  ssdifidl  33433  ssmxidl  33450  ply1degltlss  33568  r1plmhm  33581  drgextlsp  33617  ccfldsrarelvec  33695  constrconj  33769  constrfin  33770  constrelextdg2  33771  pstmfval  33920  qqhval2lem  34005  qqhvq  34011  measdivcst  34248  measdivcstALTV  34249  carsggect  34342  tgoldbachgtd  34686  bnj1098  34806  bnj149  34898  bnj1118  35007  erdszelem9  35254  resconn  35301  cvmseu  35331  cvmlift2lem10  35367  cvmlift2lem12  35369  ex-sategoelel  35476  elmrsubrn  35575  mclsind  35625  r1peuqusdeg1  35698  cgrid2  36058  segconeu  36066  btwncomim  36068  btwnswapid  36072  trisegint  36083  cgrxfr  36110  brofs2  36132  endofsegid  36140  btwnconn2  36157  seglemin  36168  segletr  36169  btwnsegle  36172  colinbtwnle  36173  broutsideof2  36177  btwnoutside  36180  broutsideof3  36181  outsideoftr  36184  outsidele  36187  fvray  36196  fvline  36199  ellines  36207  weiunpo  36520  broucube  37704  ftc1anc  37751  sdclem1  37793  sstotbnd2  37824  iscringd  38048  lsmsat  39117  lfladdcl  39180  lflnegcl  39184  lflvscl  39186  eqlkr  39208  lshpkrlem4  39222  lshpkrlem6  39224  ldualgrplem  39254  lduallmodlem  39261  latmassOLD  39338  latm12  39339  latm32  39340  latmrot  39341  latmmdiN  39343  latmmdir  39344  omlfh1N  39367  omlfh3N  39368  cvrnbtwn2  39384  cvlexchb1  39439  cvlsupr2  39452  hlatjass  39479  hlatj12  39480  hlatj32  39481  cvrat  39531  cvrat2  39538  atltcvr  39544  atexchltN  39550  cvrat3  39551  cvrat4  39552  atbtwnexOLDN  39556  atbtwnex  39557  3dimlem3  39570  3dimlem3OLDN  39571  3at  39599  2atneat  39624  llncmp  39631  2at0mat0  39634  2atmat0  39635  llncvrlpln  39667  lplncmp  39671  2llnjaN  39675  4atlem11  39718  lplncvrlvol  39725  lvolcmp  39726  2atm2atN  39894  elpaddatriN  39912  paddasslem8  39936  paddass  39947  padd12N  39948  paddssw2  39953  paddss  39954  pmod1i  39957  pmodN  39959  pmapjlln1  39964  atmod1i1  39966  atmod1i2  39968  pexmidlem2N  40080  pl42lem2N  40089  pl42lem3N  40090  pl42lem4N  40091  pl42N  40092  lhpm0atN  40138  lautlt  40200  lautcvr  40201  lautj  40202  lautm  40203  ltrneq2  40257  cdlemd1  40307  cdleme1b  40335  cdleme1  40336  cdleme2  40337  cdleme3e  40341  cdlemefr27cl  40512  cdlemefs27cl  40522  cdleme42ke  40594  cdleme42mN  40596  cdlemf2  40671  cdlemftr2  40675  trljco  40849  tgrpgrplem  40858  tendoplass  40892  tendodi1  40893  tendodi2  40894  cdlemk34  41019  cdlemk36  41022  erngdvlem3-rN  41107  tendospdi1  41129  dialss  41155  dvhvaddass  41206  dvhopvsca  41211  dvhlveclem  41217  diblss  41279  diclss  41302  diclspsn  41303  cdlemn11pre  41319  dihmeetlem12N  41427  dihmeetlem16N  41431  dihmeetlem17N  41432  dihmeetlem18N  41433  dvh4dimN  41556  lpolconN  41596  dochpolN  41599  lclkr  41642  lclkrs  41648  lcfr  41694  aks6d1c1  42219  irrapxlem6  42934  jm2.26lem3  43108  dgrsub2  43242  mpaaroot  43262  mendring  43295  mendlmod  43296  mendassa  43297  relexpmulg  43817  iunrelexpmin2  43819  relexpxpmin  43824  neicvgel1  44226  grumnud  44393  rfcnpre3  45144  fmuldfeq  45697  xlimbr  45939  stoweidlem43  46155  stoweidlem52  46164  stoweidlem53  46165  stoweidlem56  46168  stoweidlem57  46169  stoweidlem60  46172  issmfle  46857  issmfgt  46868  issmfge  46882  smflimlem4  46886  ltsubsubaddltsub  47415  iccpartigtl  47537  iccelpart  47547  prproropf1olem1  47617  fpprel2  47855  cycl3grtrilem  48060  grlimprclnbgr  48110  upgrwlkupwlk  48254  copissgrp  48282  cznrng  48375  funcringcsetcALTV2lem9  48412  funcringcsetclem9ALTV  48435  ldepsprlem  48587  lincresunit3  48596  lincreslvec3  48597  itsclc0yqe  48876  itsclc0yqsol  48879  resipos  49089  topdlat  49118  catprs  49126  endmndlem  49130  idmon  49135  idepi  49136  thincmon  49548  thincepi  49549  functhinclem1  49559  grptcmon  49708  grptcepi  49709