Theorem simpr2 1205

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 487	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜒)
2	1	3ad2antr2 1199	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  simpr12  1268  simpr22  1271  simpr32  1274  simp1r2  1280  simp2r2  1286  simp3r2  1292  3anandis  1482  fpr2g  7180  isopolem  7314  fr3nr  7740  sexp3  8117  dif1en  9115  frfi  9214  intrnfi  9348  fisupcl  9402  cnfcomlem  9640  ackbij1lem15  10175  cofsmo  10212  sornom  10220  fpwwe2lem4  10578  dedekindle  11333  supmul1  12147  eluzuzle  12834  xlesubadd  13252  elioc2  13399  elico2  13400  elicc2  13401  fseq1p1m1  13589  fz0fzelfz0  13625  hash7g  14485  swrdsbslen  14664  ccatswrd  14668  swrdswrdlem  14703  wwlktovf1  14956  tanadd  16171  dvds2ln  16295  cshwsidrepsw  17101  ressress  17255  f1ovscpbl  17528  mreexexlem4d  17651  mreexexd  17652  iscatd2  17685  2oppccomf  17729  issubc3  17854  fthmon  17934  fuccocl  17972  fucidcl  17973  invfuc  17982  initoeu2lem0  18018  initoeu2lem1  18019  curf2cl  18235  yonedalem4c  18281  yonedalem3  18284  pospo  18347  latjle12  18454  latjlej1  18457  latnlej2  18463  latlem12  18470  latmlem1  18473  latledi  18481  latjass  18487  latj12  18488  latj32  18489  latj13  18490  latj31  18491  latjrot  18492  latjjdi  18495  latjjdir  18496  latdisdlem  18500  prdssgrpd  18739  prdsmndd  18776  mndissubm  18813  frmdmnd  18865  grpsubrcan  19035  grpsubadd  19042  grpaddsubass  19044  grpsubsub4  19047  grppnpcan2  19048  grpnpncan  19049  mulgnndir  19117  mulgnn0dir  19118  mulgdir  19120  mulgnnass  19123  mulgnn0ass  19124  mulgass  19125  mulgsubdir  19128  pwsmulg  19133  issubg2  19155  eqgval  19190  qusgrp  19199  galcan  19316  gacan  19317  oppgmnd  19366  fvcosymgeq  19441  pmtrprfv  19465  psgnunilem3  19508  cmn32  19812  cmn12  19814  abladdsub  19824  ablsubaddsub  19826  ablsubsub23  19836  mulgdi  19838  mulgsubdi  19841  dprdss  20043  dprdz  20044  dprdf1o  20046  dprdsn  20050  dprd2da  20056  dmdprdsplit  20061  ablfac1b  20084  pgpfac1lem5  20093  prdsrngd  20194  srgdilem  20210  srgbinom  20249  ringdilem  20267  prdsringd  20337  opprrng  20362  mulgass3  20370  dvrass  20425  dvrdir  20429  subrgunit  20608  issubrg2  20610  isdomn4  20734  abvdiv  20847  lsssn0  20984  islss3  20995  prdslmodd  21005  islmhm2  21074  lspsolv  21182  islbs2  21193  islbs3  21194  lbsextlem4  21200  sralmod  21223  rnglidl1  21271  psgndiflemB  21621  ipdir  21660  ipdi  21661  ipsubdir  21663  ipsubdi  21664  ipass  21666  ipassr  21667  ipassr2  21668  isphld  21675  ocvlss  21693  sraassab  21889  psrlmod  21980  psrring  21990  psrassa  21993  mamudm  22424  matring  22472  matassa  22473  ofco2  22480  ma1repveval  22600  mdetunilem1  22641  mdetunilem9  22649  chpscmatgsumbin  22873  iinopn  22931  restopnb  23204  subbascn  23283  nrmsep2  23385  isnrm3  23388  regsep2  23405  dnsconst  23407  dfconn2  23448  1stcelcls  23490  dislly  23526  ptuni2  23605  tx1stc  23679  0nelfb  23860  infil  23892  fsubbas  23896  filssufilg  23940  hauspwpwf1  24016  cnextcn  24096  tmdcn2  24118  ustuqtoplem  24268  utopsnneiplem  24276  psmettri  24340  isxmet2d  24356  xmettri  24380  xmetres2  24390  bldisj  24427  blss2ps  24432  blss2  24433  xmstri2  24495  mstri2  24496  xmstri  24497  mstri  24498  xmstri3  24499  mstri3  24500  msrtri  24501  comet  24542  stdbdbl  24546  met2ndci  24551  ngprcan  24639  ngplcan  24640  ngpsubcan  24643  nmtri2  24656  nrgdsdi  24694  nrgdsdir  24695  nlmdsdi  24710  nlmdsdir  24711  blcvx  24827  icoopnst  24970  pi1grplem  25080  clmpm1dir  25134  cmodscmulexp  25153  cvsdiv  25163  cvsdivcl  25164  cphdivcl  25213  cphsubdir  25239  cphsubdi  25240  tcphcph  25268  bcthlem5  25359  volfiniun  25578  volcn  25637  itg1val2  25715  dvconst  25948  dvlip  26024  ftc1a  26068  ulmval  26409  ulmdvlem3  26431  ang180  26845  cvxcl  27015  scvxcvx  27016  sgmmul  27231  dchrabl  27284  gausslemma2dlem1a  27395  nosupbnd1  27744  noinfbnd1lem5  27757  noinfbnd1  27759  sltsss2  27825  addscom  28025  addbday  28077  motgrp  28678  iscgra1  28945  cgrane1  28947  cgrane3  28949  cgrahl1  28951  cgrahl2  28952  cgracgr  28953  cgratr  28958  cgrabtwn  28961  cgrahl  28962  dfcgra2  28965  sacgr  28966  f1otrge  29007  colinearalglem1  29042  axcgrtr  29051  axeuclidlem  29098  axcontlem3  29102  axcontlem4  29103  axcontlem7  29106  eengtrkg  29122  eengtrkge  29123  edglnl  29279  subgruhgredgd  29420  nbfusgrlevtxm2  29514  lfgriswlk  29822  wwlknbp1  29979  usgrwwlks2on  30093  umgrwwlks2on  30094  rusgrnumwwlks  30112  clwlkclwwlkfo  30146  3spthd  30313  3vfriswmgr  30415  frgr2wwlkeqm  30468  numclwwlk1lem2f  30492  numclwwlk2  30518  numclwwlk3  30522  numclwwlk5  30525  grpomuldivass  30679  ablomuldiv  30690  ablodivdiv4  30692  ablonnncan1  30695  nvmdi  30786  dipassr  30984  archiabllem2c  33325  dvrcan5  33366  rloccring  33400  reofld  33475  eqgvscpbl  33482  qusvsval  33484  quslmod  33490  quslmhm  33491  prmidlc  33580  ssdifidl  33589  ssmxidl  33606  ply1degltlss  33736  r1plmhm  33750  drgextlsp  33835  ccfldsrarelvec  33912  constrconj  33986  constrfin  33987  constrelextdg2  33988  pstmfval  34137  qqhval2lem  34222  qqhvq  34228  measdivcst  34465  measdivcstALTV  34466  carsggect  34559  tgoldbachgtd  34903  bnj1098  35026  bnj149  35117  bnj1118  35226  erdszelem9  35487  resconn  35534  cvmseu  35564  cvmlift2lem10  35600  cvmlift2lem12  35602  ex-sategoelel  35709  elmrsubrn  35808  mclsind  35858  r1peuqusdeg1  35931  cgrid2  36291  segconeu  36299  btwncomim  36301  btwnswapid  36305  trisegint  36316  cgrxfr  36343  brofs2  36365  endofsegid  36373  btwnconn2  36390  seglemin  36401  segletr  36402  btwnsegle  36405  colinbtwnle  36406  broutsideof2  36410  btwnoutside  36413  broutsideof3  36414  outsideoftr  36417  outsidele  36420  fvray  36429  fvline  36432  ellines  36440  nmulprop  36478  weiunpo  36763  broucube  38091  ftc1anc  38138  sdclem1  38180  sstotbnd2  38211  iscringd  38435  lsmsat  39570  lfladdcl  39633  lflnegcl  39637  lflvscl  39639  eqlkr  39661  lshpkrlem4  39675  lshpkrlem6  39677  ldualgrplem  39707  lduallmodlem  39714  latmassOLD  39791  latm12  39792  latm32  39793  latmrot  39794  latmmdiN  39796  latmmdir  39797  omlfh1N  39820  omlfh3N  39821  cvrnbtwn2  39837  cvlexchb1  39892  cvlsupr2  39905  hlatjass  39932  hlatj12  39933  hlatj32  39934  cvrat  39984  cvrat2  39991  atltcvr  39997  atexchltN  40003  cvrat3  40004  cvrat4  40005  atbtwnexOLDN  40009  atbtwnex  40010  3dimlem3  40023  3dimlem3OLDN  40024  3at  40052  2atneat  40077  llncmp  40084  2at0mat0  40087  2atmat0  40088  llncvrlpln  40120  lplncmp  40124  2llnjaN  40128  4atlem11  40171  lplncvrlvol  40178  lvolcmp  40179  2atm2atN  40347  elpaddatriN  40365  paddasslem8  40389  paddass  40400  padd12N  40401  paddssw2  40406  paddss  40407  pmod1i  40410  pmodN  40412  pmapjlln1  40417  atmod1i1  40419  atmod1i2  40421  pexmidlem2N  40533  pl42lem2N  40542  pl42lem3N  40543  pl42lem4N  40544  pl42N  40545  lhpm0atN  40591  lautlt  40653  lautcvr  40654  lautj  40655  lautm  40656  ltrneq2  40710  cdlemd1  40760  cdleme1b  40788  cdleme1  40789  cdleme2  40790  cdleme3e  40794  cdlemefr27cl  40965  cdlemefs27cl  40975  cdleme42ke  41047  cdleme42mN  41049  cdlemf2  41124  cdlemftr2  41128  trljco  41302  tgrpgrplem  41311  tendoplass  41345  tendodi1  41346  tendodi2  41347  cdlemk34  41472  cdlemk36  41475  erngdvlem3-rN  41560  tendospdi1  41582  dialss  41608  dvhvaddass  41659  dvhopvsca  41664  dvhlveclem  41670  diblss  41732  diclss  41755  diclspsn  41756  cdlemn11pre  41772  dihmeetlem12N  41880  dihmeetlem16N  41884  dihmeetlem17N  41885  dihmeetlem18N  41886  dvh4dimN  42009  lpolconN  42049  dochpolN  42052  lclkr  42095  lclkrs  42101  lcfr  42147  aks6d1c1  42671  irrapxlem6  43342  jm2.26lem3  43516  dgrsub2  43650  mpaaroot  43670  mendring  43703  mendlmod  43704  mendassa  43705  relexpmulg  44224  iunrelexpmin2  44226  relexpxpmin  44231  neicvgel1  44633  grumnud  44800  rfcnpre3  45551  fmuldfeq  46097  xlimbr  46339  stoweidlem43  46555  stoweidlem52  46564  stoweidlem53  46565  stoweidlem56  46568  stoweidlem57  46569  stoweidlem60  46572  issmfle  47257  issmfgt  47268  issmfge  47282  smflimlem4  47286  ltsubsubaddltsub  47833  iccpartigtl  47967  iccelpart  47977  prproropf1olem1  48047  fpprel2  48301  cycl3grtrilem  48506  grlimprclnbgr  48556  upgrwlkupwlk  48700  copissgrp  48728  cznrng  48821  funcringcsetcALTV2lem9  48858  funcringcsetclem9ALTV  48881  ldepsprlem  49032  lincresunit3  49041  lincreslvec3  49042  itsclc0yqe  49321  itsclc0yqsol  49324  resipos  49534  topdlat  49563  catprs  49570  endmndlem  49574  idmon  49579  idepi  49580  thincmon  49992  thincepi  49993  functhinclem1  50003  grptcmon  50152  grptcepi  50153