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  7208  isopolem  7343  fr3nr  7771  sexp3  8157  dif1en  9179  frfi  9298  intrnfi  9433  fisupcl  9487  cnfcomlem  9718  ackbij1lem15  10252  cofsmo  10288  sornom  10296  fpwwe2lem4  10653  dedekindle  11404  supmul1  12216  eluzuzle  12866  xlesubadd  13284  elioc2  13431  elico2  13432  elicc2  13433  fseq1p1m1  13620  fz0fzelfz0  13656  hash7g  14509  swrdsbslen  14687  ccatswrd  14691  swrdswrdlem  14727  wwlktovf1  14981  tanadd  16190  dvds2ln  16313  cshwsidrepsw  17118  ressress  17273  f1ovscpbl  17545  mreexexlem4d  17664  mreexexd  17665  iscatd2  17698  2oppccomf  17742  issubc3  17867  fthmon  17947  fuccocl  17985  fucidcl  17986  invfuc  17995  initoeu2lem0  18031  initoeu2lem1  18032  curf2cl  18248  yonedalem4c  18294  yonedalem3  18297  pospo  18360  latjle12  18465  latjlej1  18468  latnlej2  18474  latlem12  18481  latmlem1  18484  latledi  18492  latjass  18498  latj12  18499  latj32  18500  latj13  18501  latj31  18502  latjrot  18503  latjjdi  18506  latjjdir  18507  latdisdlem  18511  prdssgrpd  18716  prdsmndd  18753  mndissubm  18790  frmdmnd  18842  grpsubrcan  19009  grpsubadd  19016  grpaddsubass  19018  grpsubsub4  19021  grppnpcan2  19022  grpnpncan  19023  mulgnndir  19091  mulgnn0dir  19092  mulgdir  19094  mulgnnass  19097  mulgnn0ass  19098  mulgass  19099  mulgsubdir  19102  pwsmulg  19107  issubg2  19129  eqgval  19165  qusgrp  19174  galcan  19292  gacan  19293  oppgmnd  19342  fvcosymgeq  19415  pmtrprfv  19439  psgnunilem3  19482  cmn32  19786  cmn12  19788  abladdsub  19798  ablsubaddsub  19800  ablsubsub23  19810  mulgdi  19812  mulgsubdi  19815  dprdss  20017  dprdz  20018  dprdf1o  20020  dprdsn  20024  dprd2da  20030  dmdprdsplit  20035  ablfac1b  20058  pgpfac1lem5  20067  prdsrngd  20141  srgdilem  20157  srgbinom  20196  ringdilem  20214  prdsringd  20286  opprrng  20310  mulgass3  20318  dvrass  20373  dvrdir  20377  subrgunit  20555  issubrg2  20557  isdomn4  20681  abvdiv  20794  lsssn0  20910  islss3  20921  prdslmodd  20931  islmhm2  21001  lspsolv  21109  islbs2  21120  islbs3  21121  lbsextlem4  21127  sralmod  21150  rnglidl1  21198  psgndiflemB  21565  ipdir  21604  ipdi  21605  ipsubdir  21607  ipsubdi  21608  ipass  21610  ipassr  21611  ipassr2  21612  isphld  21619  ocvlss  21637  sraassab  21833  sraassaOLD  21835  psrgrpOLD  21922  psrlmod  21925  psrring  21935  psrassa  21938  mamudm  22338  matring  22386  matassa  22387  ofco2  22394  ma1repveval  22514  mdetunilem1  22555  mdetunilem9  22563  chpscmatgsumbin  22787  iinopn  22845  restopnb  23118  subbascn  23197  nrmsep2  23299  isnrm3  23302  regsep2  23319  dnsconst  23321  dfconn2  23362  1stcelcls  23404  dislly  23440  ptuni2  23519  tx1stc  23593  0nelfb  23774  infil  23806  fsubbas  23810  filssufilg  23854  hauspwpwf1  23930  cnextcn  24010  tmdcn2  24032  ustuqtoplem  24183  utopsnneiplem  24191  psmettri  24255  isxmet2d  24271  xmettri  24295  xmetres2  24305  bldisj  24342  blss2ps  24347  blss2  24348  xmstri2  24410  mstri2  24411  xmstri  24412  mstri  24413  xmstri3  24414  mstri3  24415  msrtri  24416  comet  24457  stdbdbl  24461  met2ndci  24466  ngprcan  24554  ngplcan  24555  ngpsubcan  24558  nmtri2  24571  nrgdsdi  24609  nrgdsdir  24610  nlmdsdi  24625  nlmdsdir  24626  blcvx  24742  icoopnst  24892  pi1grplem  25005  clmpm1dir  25059  cmodscmulexp  25078  cvsdiv  25088  cvsdivcl  25089  cphdivcl  25139  cphsubdir  25165  cphsubdi  25166  tcphcph  25194  bcthlem5  25285  volfiniun  25505  volcn  25564  itg1val2  25642  dvconst  25875  dvlip  25955  ftc1a  26001  ulmval  26346  ulmdvlem3  26368  ang180  26781  cvxcl  26952  scvxcvx  26953  sgmmul  27169  dchrabl  27222  gausslemma2dlem1a  27333  nosupbnd1  27683  noinfbnd1lem5  27696  noinfbnd1  27698  ssltss2  27758  addscom  27930  addsbday  27981  motgrp  28527  iscgra1  28794  cgrane1  28796  cgrane3  28798  cgrahl1  28800  cgrahl2  28801  cgracgr  28802  cgratr  28807  cgrabtwn  28810  cgrahl  28811  dfcgra2  28814  sacgr  28815  f1otrge  28856  colinearalglem1  28890  axcgrtr  28899  axeuclidlem  28946  axcontlem3  28950  axcontlem4  28951  axcontlem7  28954  eengtrkg  28970  eengtrkge  28971  edglnl  29127  subgruhgredgd  29268  nbfusgrlevtxm2  29362  lfgriswlk  29673  wwlknbp1  29831  umgrwwlks2on  29944  rusgrnumwwlks  29961  clwlkclwwlkfo  29995  3spthd  30162  3vfriswmgr  30264  frgr2wwlkeqm  30317  numclwwlk1lem2f  30341  numclwwlk2  30367  numclwwlk3  30371  numclwwlk5  30374  grpomuldivass  30527  ablomuldiv  30538  ablodivdiv4  30540  ablonnncan1  30543  nvmdi  30634  dipassr  30832  archiabllem2c  33198  dvrcan5  33236  rloccring  33270  reofld  33364  eqgvscpbl  33370  qusvsval  33372  quslmod  33378  quslmhm  33379  prmidlc  33468  ssdifidl  33477  ssmxidl  33494  ply1degltlss  33611  r1plmhm  33624  drgextlsp  33638  ccfldsrarelvec  33717  constrconj  33784  constrfin  33785  constrelextdg2  33786  pstmfval  33932  qqhval2lem  34017  qqhvq  34023  measdivcst  34260  measdivcstALTV  34261  carsggect  34355  tgoldbachgtd  34699  bnj1098  34819  bnj149  34911  bnj1118  35020  erdszelem9  35226  resconn  35273  cvmseu  35303  cvmlift2lem10  35339  cvmlift2lem12  35341  ex-sategoelel  35448  elmrsubrn  35547  mclsind  35597  r1peuqusdeg1  35670  cgrid2  36026  segconeu  36034  btwncomim  36036  btwnswapid  36040  trisegint  36051  cgrxfr  36078  brofs2  36100  endofsegid  36108  btwnconn2  36125  seglemin  36136  segletr  36137  btwnsegle  36140  colinbtwnle  36141  broutsideof2  36145  btwnoutside  36148  broutsideof3  36149  outsideoftr  36152  outsidele  36155  fvray  36164  fvline  36167  ellines  36175  weiunpo  36488  broucube  37683  ftc1anc  37730  sdclem1  37772  sstotbnd2  37803  iscringd  38027  lsmsat  39031  lfladdcl  39094  lflnegcl  39098  lflvscl  39100  eqlkr  39122  lshpkrlem4  39136  lshpkrlem6  39138  ldualgrplem  39168  lduallmodlem  39175  latmassOLD  39252  latm12  39253  latm32  39254  latmrot  39255  latmmdiN  39257  latmmdir  39258  omlfh1N  39281  omlfh3N  39282  cvrnbtwn2  39298  cvlexchb1  39353  cvlsupr2  39366  hlatjass  39393  hlatj12  39394  hlatj32  39395  cvrat  39446  cvrat2  39453  atltcvr  39459  atexchltN  39465  cvrat3  39466  cvrat4  39467  atbtwnexOLDN  39471  atbtwnex  39472  3dimlem3  39485  3dimlem3OLDN  39486  3at  39514  2atneat  39539  llncmp  39546  2at0mat0  39549  2atmat0  39550  llncvrlpln  39582  lplncmp  39586  2llnjaN  39590  4atlem11  39633  lplncvrlvol  39640  lvolcmp  39641  2atm2atN  39809  elpaddatriN  39827  paddasslem8  39851  paddass  39862  padd12N  39863  paddssw2  39868  paddss  39869  pmod1i  39872  pmodN  39874  pmapjlln1  39879  atmod1i1  39881  atmod1i2  39883  pexmidlem2N  39995  pl42lem2N  40004  pl42lem3N  40005  pl42lem4N  40006  pl42N  40007  lhpm0atN  40053  lautlt  40115  lautcvr  40116  lautj  40117  lautm  40118  ltrneq2  40172  cdlemd1  40222  cdleme1b  40250  cdleme1  40251  cdleme2  40252  cdleme3e  40256  cdlemefr27cl  40427  cdlemefs27cl  40437  cdleme42ke  40509  cdleme42mN  40511  cdlemf2  40586  cdlemftr2  40590  trljco  40764  tgrpgrplem  40773  tendoplass  40807  tendodi1  40808  tendodi2  40809  cdlemk34  40934  cdlemk36  40937  erngdvlem3-rN  41022  tendospdi1  41044  dialss  41070  dvhvaddass  41121  dvhopvsca  41126  dvhlveclem  41132  diblss  41194  diclss  41217  diclspsn  41218  cdlemn11pre  41234  dihmeetlem12N  41342  dihmeetlem16N  41346  dihmeetlem17N  41347  dihmeetlem18N  41348  dvh4dimN  41471  lpolconN  41511  dochpolN  41514  lclkr  41557  lclkrs  41563  lcfr  41609  aks6d1c1  42134  irrapxlem6  42825  jm2.26lem3  43000  dgrsub2  43134  mpaaroot  43154  mendring  43187  mendlmod  43188  mendassa  43189  relexpmulg  43709  iunrelexpmin2  43711  relexpxpmin  43716  neicvgel1  44118  grumnud  44285  rfcnpre3  45037  fmuldfeq  45592  xlimbr  45836  stoweidlem43  46052  stoweidlem52  46061  stoweidlem53  46062  stoweidlem56  46065  stoweidlem57  46066  stoweidlem60  46069  issmfle  46754  issmfgt  46765  issmfge  46779  smflimlem4  46783  ltsubsubaddltsub  47310  iccpartigtl  47417  iccelpart  47427  prproropf1olem1  47497  fpprel2  47735  cycl3grtrilem  47938  grlimgrtrilem1  47986  upgrwlkupwlk  48095  copissgrp  48123  cznrng  48216  funcringcsetcALTV2lem9  48253  funcringcsetclem9ALTV  48276  ldepsprlem  48428  lincresunit3  48437  lincreslvec3  48438  itsclc0yqe  48721  itsclc0yqsol  48724  resipos  48929  topdlat  48958  catprs  48966  endmndlem  48970  idmon  48975  idepi  48976  thincmon  49299  thincepi  49300  functhinclem1  49310  grptcmon  49450  grptcepi  49451