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  7140  isopolem  7274  fr3nr  7700  sexp3  8078  dif1en  9066  frfi  9164  intrnfi  9295  fisupcl  9349  cnfcomlem  9584  ackbij1lem15  10116  cofsmo  10152  sornom  10160  fpwwe2lem4  10517  dedekindle  11269  supmul1  12083  eluzuzle  12733  xlesubadd  13154  elioc2  13301  elico2  13302  elicc2  13303  fseq1p1m1  13490  fz0fzelfz0  13526  hash7g  14385  swrdsbslen  14564  ccatswrd  14568  swrdswrdlem  14603  wwlktovf1  14856  tanadd  16068  dvds2ln  16192  cshwsidrepsw  16997  ressress  17150  f1ovscpbl  17422  mreexexlem4d  17545  mreexexd  17546  iscatd2  17579  2oppccomf  17623  issubc3  17748  fthmon  17828  fuccocl  17866  fucidcl  17867  invfuc  17876  initoeu2lem0  17912  initoeu2lem1  17913  curf2cl  18129  yonedalem4c  18175  yonedalem3  18178  pospo  18241  latjle12  18348  latjlej1  18351  latnlej2  18357  latlem12  18364  latmlem1  18367  latledi  18375  latjass  18381  latj12  18382  latj32  18383  latj13  18384  latj31  18385  latjrot  18386  latjjdi  18389  latjjdir  18390  latdisdlem  18394  prdssgrpd  18633  prdsmndd  18670  mndissubm  18707  frmdmnd  18759  grpsubrcan  18926  grpsubadd  18933  grpaddsubass  18935  grpsubsub4  18938  grppnpcan2  18939  grpnpncan  18940  mulgnndir  19008  mulgnn0dir  19009  mulgdir  19011  mulgnnass  19014  mulgnn0ass  19015  mulgass  19016  mulgsubdir  19019  pwsmulg  19024  issubg2  19046  eqgval  19082  qusgrp  19091  galcan  19209  gacan  19210  oppgmnd  19259  fvcosymgeq  19334  pmtrprfv  19358  psgnunilem3  19401  cmn32  19705  cmn12  19707  abladdsub  19717  ablsubaddsub  19719  ablsubsub23  19729  mulgdi  19731  mulgsubdi  19734  dprdss  19936  dprdz  19937  dprdf1o  19939  dprdsn  19943  dprd2da  19949  dmdprdsplit  19954  ablfac1b  19977  pgpfac1lem5  19986  prdsrngd  20087  srgdilem  20103  srgbinom  20142  ringdilem  20160  prdsringd  20232  opprrng  20256  mulgass3  20264  dvrass  20319  dvrdir  20323  subrgunit  20498  issubrg2  20500  isdomn4  20624  abvdiv  20737  lsssn0  20874  islss3  20885  prdslmodd  20895  islmhm2  20965  lspsolv  21073  islbs2  21084  islbs3  21085  lbsextlem4  21091  sralmod  21114  rnglidl1  21162  psgndiflemB  21530  ipdir  21569  ipdi  21570  ipsubdir  21572  ipsubdi  21573  ipass  21575  ipassr  21576  ipassr2  21577  isphld  21584  ocvlss  21602  sraassab  21798  sraassaOLD  21800  psrgrpOLD  21887  psrlmod  21890  psrring  21900  psrassa  21903  mamudm  22303  matring  22351  matassa  22352  ofco2  22359  ma1repveval  22479  mdetunilem1  22520  mdetunilem9  22528  chpscmatgsumbin  22752  iinopn  22810  restopnb  23083  subbascn  23162  nrmsep2  23264  isnrm3  23267  regsep2  23284  dnsconst  23286  dfconn2  23327  1stcelcls  23369  dislly  23405  ptuni2  23484  tx1stc  23558  0nelfb  23739  infil  23771  fsubbas  23775  filssufilg  23819  hauspwpwf1  23895  cnextcn  23975  tmdcn2  23997  ustuqtoplem  24147  utopsnneiplem  24155  psmettri  24219  isxmet2d  24235  xmettri  24259  xmetres2  24269  bldisj  24306  blss2ps  24311  blss2  24312  xmstri2  24374  mstri2  24375  xmstri  24376  mstri  24377  xmstri3  24378  mstri3  24379  msrtri  24380  comet  24421  stdbdbl  24425  met2ndci  24430  ngprcan  24518  ngplcan  24519  ngpsubcan  24522  nmtri2  24535  nrgdsdi  24573  nrgdsdir  24574  nlmdsdi  24589  nlmdsdir  24590  blcvx  24706  icoopnst  24856  pi1grplem  24969  clmpm1dir  25023  cmodscmulexp  25042  cvsdiv  25052  cvsdivcl  25053  cphdivcl  25102  cphsubdir  25128  cphsubdi  25129  tcphcph  25157  bcthlem5  25248  volfiniun  25468  volcn  25527  itg1val2  25605  dvconst  25838  dvlip  25918  ftc1a  25964  ulmval  26309  ulmdvlem3  26331  ang180  26744  cvxcl  26915  scvxcvx  26916  sgmmul  27132  dchrabl  27185  gausslemma2dlem1a  27296  nosupbnd1  27646  noinfbnd1lem5  27659  noinfbnd1  27661  ssltss2  27722  addscom  27902  addsbday  27953  motgrp  28514  iscgra1  28781  cgrane1  28783  cgrane3  28785  cgrahl1  28787  cgrahl2  28788  cgracgr  28789  cgratr  28794  cgrabtwn  28797  cgrahl  28798  dfcgra2  28801  sacgr  28802  f1otrge  28843  colinearalglem1  28877  axcgrtr  28886  axeuclidlem  28933  axcontlem3  28937  axcontlem4  28938  axcontlem7  28941  eengtrkg  28957  eengtrkge  28958  edglnl  29114  subgruhgredgd  29255  nbfusgrlevtxm2  29349  lfgriswlk  29658  wwlknbp1  29815  umgrwwlks2on  29928  rusgrnumwwlks  29945  clwlkclwwlkfo  29979  3spthd  30146  3vfriswmgr  30248  frgr2wwlkeqm  30301  numclwwlk1lem2f  30325  numclwwlk2  30351  numclwwlk3  30355  numclwwlk5  30358  grpomuldivass  30511  ablomuldiv  30522  ablodivdiv4  30524  ablonnncan1  30527  nvmdi  30618  dipassr  30816  archiabllem2c  33154  dvrcan5  33193  rloccring  33227  reofld  33298  eqgvscpbl  33305  qusvsval  33307  quslmod  33313  quslmhm  33314  prmidlc  33403  ssdifidl  33412  ssmxidl  33429  ply1degltlss  33547  r1plmhm  33560  drgextlsp  33596  ccfldsrarelvec  33674  constrconj  33748  constrfin  33749  constrelextdg2  33750  pstmfval  33899  qqhval2lem  33984  qqhvq  33990  measdivcst  34227  measdivcstALTV  34228  carsggect  34321  tgoldbachgtd  34665  bnj1098  34785  bnj149  34877  bnj1118  34986  erdszelem9  35211  resconn  35258  cvmseu  35288  cvmlift2lem10  35324  cvmlift2lem12  35326  ex-sategoelel  35433  elmrsubrn  35532  mclsind  35582  r1peuqusdeg1  35655  cgrid2  36016  segconeu  36024  btwncomim  36026  btwnswapid  36030  trisegint  36041  cgrxfr  36068  brofs2  36090  endofsegid  36098  btwnconn2  36115  seglemin  36126  segletr  36127  btwnsegle  36130  colinbtwnle  36131  broutsideof2  36135  btwnoutside  36138  broutsideof3  36139  outsideoftr  36142  outsidele  36145  fvray  36154  fvline  36157  ellines  36165  weiunpo  36478  broucube  37673  ftc1anc  37720  sdclem1  37762  sstotbnd2  37793  iscringd  38017  lsmsat  39026  lfladdcl  39089  lflnegcl  39093  lflvscl  39095  eqlkr  39117  lshpkrlem4  39131  lshpkrlem6  39133  ldualgrplem  39163  lduallmodlem  39170  latmassOLD  39247  latm12  39248  latm32  39249  latmrot  39250  latmmdiN  39252  latmmdir  39253  omlfh1N  39276  omlfh3N  39277  cvrnbtwn2  39293  cvlexchb1  39348  cvlsupr2  39361  hlatjass  39388  hlatj12  39389  hlatj32  39390  cvrat  39440  cvrat2  39447  atltcvr  39453  atexchltN  39459  cvrat3  39460  cvrat4  39461  atbtwnexOLDN  39465  atbtwnex  39466  3dimlem3  39479  3dimlem3OLDN  39480  3at  39508  2atneat  39533  llncmp  39540  2at0mat0  39543  2atmat0  39544  llncvrlpln  39576  lplncmp  39580  2llnjaN  39584  4atlem11  39627  lplncvrlvol  39634  lvolcmp  39635  2atm2atN  39803  elpaddatriN  39821  paddasslem8  39845  paddass  39856  padd12N  39857  paddssw2  39862  paddss  39863  pmod1i  39866  pmodN  39868  pmapjlln1  39873  atmod1i1  39875  atmod1i2  39877  pexmidlem2N  39989  pl42lem2N  39998  pl42lem3N  39999  pl42lem4N  40000  pl42N  40001  lhpm0atN  40047  lautlt  40109  lautcvr  40110  lautj  40111  lautm  40112  ltrneq2  40166  cdlemd1  40216  cdleme1b  40244  cdleme1  40245  cdleme2  40246  cdleme3e  40250  cdlemefr27cl  40421  cdlemefs27cl  40431  cdleme42ke  40503  cdleme42mN  40505  cdlemf2  40580  cdlemftr2  40584  trljco  40758  tgrpgrplem  40767  tendoplass  40801  tendodi1  40802  tendodi2  40803  cdlemk34  40928  cdlemk36  40931  erngdvlem3-rN  41016  tendospdi1  41038  dialss  41064  dvhvaddass  41115  dvhopvsca  41120  dvhlveclem  41126  diblss  41188  diclss  41211  diclspsn  41212  cdlemn11pre  41228  dihmeetlem12N  41336  dihmeetlem16N  41340  dihmeetlem17N  41341  dihmeetlem18N  41342  dvh4dimN  41465  lpolconN  41505  dochpolN  41508  lclkr  41551  lclkrs  41557  lcfr  41603  aks6d1c1  42128  irrapxlem6  42839  jm2.26lem3  43013  dgrsub2  43147  mpaaroot  43167  mendring  43200  mendlmod  43201  mendassa  43202  relexpmulg  43722  iunrelexpmin2  43724  relexpxpmin  43729  neicvgel1  44131  grumnud  44298  rfcnpre3  45049  fmuldfeq  45602  xlimbr  45844  stoweidlem43  46060  stoweidlem52  46069  stoweidlem53  46070  stoweidlem56  46073  stoweidlem57  46074  stoweidlem60  46077  issmfle  46762  issmfgt  46773  issmfge  46787  smflimlem4  46791  ltsubsubaddltsub  47311  iccpartigtl  47433  iccelpart  47443  prproropf1olem1  47513  fpprel2  47751  cycl3grtrilem  47956  grlimprclnbgr  48006  upgrwlkupwlk  48150  copissgrp  48178  cznrng  48271  funcringcsetcALTV2lem9  48308  funcringcsetclem9ALTV  48331  ldepsprlem  48483  lincresunit3  48492  lincreslvec3  48493  itsclc0yqe  48772  itsclc0yqsol  48775  resipos  48985  topdlat  49014  catprs  49022  endmndlem  49026  idmon  49031  idepi  49032  thincmon  49444  thincepi  49445  functhinclem1  49455  grptcmon  49604  grptcepi  49605