Theorem simpr2 1197

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

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

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 1089

This theorem is referenced by:  simpr12  1260  simpr22  1263  simpr32  1266  simp1r2  1272  simp2r2  1278  simp3r2  1284  3anandis  1474  fpr2g  7166  isopolem  7300  fr3nr  7726  sexp3  8103  dif1en  9096  frfi  9195  intrnfi  9329  fisupcl  9383  cnfcomlem  9620  ackbij1lem15  10155  cofsmo  10191  sornom  10199  fpwwe2lem4  10557  dedekindle  11310  supmul1  12125  eluzuzle  12797  xlesubadd  13215  elioc2  13362  elico2  13363  elicc2  13364  fseq1p1m1  13552  fz0fzelfz0  13588  hash7g  14448  swrdsbslen  14627  ccatswrd  14631  swrdswrdlem  14666  wwlktovf1  14919  tanadd  16134  dvds2ln  16258  cshwsidrepsw  17064  ressress  17217  f1ovscpbl  17490  mreexexlem4d  17613  mreexexd  17614  iscatd2  17647  2oppccomf  17691  issubc3  17816  fthmon  17896  fuccocl  17934  fucidcl  17935  invfuc  17944  initoeu2lem0  17980  initoeu2lem1  17981  curf2cl  18197  yonedalem4c  18243  yonedalem3  18246  pospo  18309  latjle12  18416  latjlej1  18419  latnlej2  18425  latlem12  18432  latmlem1  18435  latledi  18443  latjass  18449  latj12  18450  latj32  18451  latj13  18452  latj31  18453  latjrot  18454  latjjdi  18457  latjjdir  18458  latdisdlem  18462  prdssgrpd  18701  prdsmndd  18738  mndissubm  18775  frmdmnd  18827  grpsubrcan  18997  grpsubadd  19004  grpaddsubass  19006  grpsubsub4  19009  grppnpcan2  19010  grpnpncan  19011  mulgnndir  19079  mulgnn0dir  19080  mulgdir  19082  mulgnnass  19085  mulgnn0ass  19086  mulgass  19087  mulgsubdir  19090  pwsmulg  19095  issubg2  19117  eqgval  19152  qusgrp  19161  galcan  19279  gacan  19280  oppgmnd  19329  fvcosymgeq  19404  pmtrprfv  19428  psgnunilem3  19471  cmn32  19775  cmn12  19777  abladdsub  19787  ablsubaddsub  19789  ablsubsub23  19799  mulgdi  19801  mulgsubdi  19804  dprdss  20006  dprdz  20007  dprdf1o  20009  dprdsn  20013  dprd2da  20019  dmdprdsplit  20024  ablfac1b  20047  pgpfac1lem5  20056  prdsrngd  20157  srgdilem  20173  srgbinom  20212  ringdilem  20230  prdsringd  20300  opprrng  20325  mulgass3  20333  dvrass  20388  dvrdir  20392  subrgunit  20567  issubrg2  20569  isdomn4  20693  abvdiv  20806  lsssn0  20943  islss3  20954  prdslmodd  20964  islmhm2  21033  lspsolv  21141  islbs2  21152  islbs3  21153  lbsextlem4  21159  sralmod  21182  rnglidl1  21230  psgndiflemB  21580  ipdir  21619  ipdi  21620  ipsubdir  21622  ipsubdi  21623  ipass  21625  ipassr  21626  ipassr2  21627  isphld  21634  ocvlss  21652  sraassab  21848  psrlmod  21938  psrring  21948  psrassa  21951  mamudm  22360  matring  22408  matassa  22409  ofco2  22416  ma1repveval  22536  mdetunilem1  22577  mdetunilem9  22585  chpscmatgsumbin  22809  iinopn  22867  restopnb  23140  subbascn  23219  nrmsep2  23321  isnrm3  23324  regsep2  23341  dnsconst  23343  dfconn2  23384  1stcelcls  23426  dislly  23462  ptuni2  23541  tx1stc  23615  0nelfb  23796  infil  23828  fsubbas  23832  filssufilg  23876  hauspwpwf1  23952  cnextcn  24032  tmdcn2  24054  ustuqtoplem  24204  utopsnneiplem  24212  psmettri  24276  isxmet2d  24292  xmettri  24316  xmetres2  24326  bldisj  24363  blss2ps  24368  blss2  24369  xmstri2  24431  mstri2  24432  xmstri  24433  mstri  24434  xmstri3  24435  mstri3  24436  msrtri  24437  comet  24478  stdbdbl  24482  met2ndci  24487  ngprcan  24575  ngplcan  24576  ngpsubcan  24579  nmtri2  24592  nrgdsdi  24630  nrgdsdir  24631  nlmdsdi  24646  nlmdsdir  24647  blcvx  24763  icoopnst  24906  pi1grplem  25016  clmpm1dir  25070  cmodscmulexp  25089  cvsdiv  25099  cvsdivcl  25100  cphdivcl  25149  cphsubdir  25175  cphsubdi  25176  tcphcph  25204  bcthlem5  25295  volfiniun  25514  volcn  25573  itg1val2  25651  dvconst  25884  dvlip  25960  ftc1a  26004  ulmval  26345  ulmdvlem3  26367  ang180  26778  cvxcl  26948  scvxcvx  26949  sgmmul  27164  dchrabl  27217  gausslemma2dlem1a  27328  nosupbnd1  27678  noinfbnd1lem5  27691  noinfbnd1  27693  sltsss2  27758  addscom  27958  addbday  28010  motgrp  28611  iscgra1  28878  cgrane1  28880  cgrane3  28882  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgratr  28891  cgrabtwn  28894  cgrahl  28895  dfcgra2  28898  sacgr  28899  f1otrge  28940  colinearalglem1  28975  axcgrtr  28984  axeuclidlem  29031  axcontlem3  29035  axcontlem4  29036  axcontlem7  29039  eengtrkg  29055  eengtrkge  29056  edglnl  29212  subgruhgredgd  29353  nbfusgrlevtxm2  29447  lfgriswlk  29755  wwlknbp1  29912  usgrwwlks2on  30026  umgrwwlks2on  30027  rusgrnumwwlks  30045  clwlkclwwlkfo  30079  3spthd  30246  3vfriswmgr  30348  frgr2wwlkeqm  30401  numclwwlk1lem2f  30425  numclwwlk2  30451  numclwwlk3  30455  numclwwlk5  30458  grpomuldivass  30612  ablomuldiv  30623  ablodivdiv4  30625  ablonnncan1  30628  nvmdi  30719  dipassr  30917  archiabllem2c  33256  dvrcan5  33297  rloccring  33331  reofld  33403  eqgvscpbl  33410  qusvsval  33412  quslmod  33418  quslmhm  33419  prmidlc  33508  ssdifidl  33517  ssmxidl  33534  ply1degltlss  33656  r1plmhm  33670  drgextlsp  33738  ccfldsrarelvec  33815  constrconj  33889  constrfin  33890  constrelextdg2  33891  pstmfval  34040  qqhval2lem  34125  qqhvq  34131  measdivcst  34368  measdivcstALTV  34369  carsggect  34462  tgoldbachgtd  34806  bnj1098  34926  bnj149  35017  bnj1118  35126  erdszelem9  35381  resconn  35428  cvmseu  35458  cvmlift2lem10  35494  cvmlift2lem12  35496  ex-sategoelel  35603  elmrsubrn  35702  mclsind  35752  r1peuqusdeg1  35825  cgrid2  36185  segconeu  36193  btwncomim  36195  btwnswapid  36199  trisegint  36210  cgrxfr  36237  brofs2  36259  endofsegid  36267  btwnconn2  36284  seglemin  36295  segletr  36296  btwnsegle  36299  colinbtwnle  36300  broutsideof2  36304  btwnoutside  36307  broutsideof3  36308  outsideoftr  36311  outsidele  36314  fvray  36323  fvline  36326  ellines  36334  weiunpo  36647  broucube  37975  ftc1anc  38022  sdclem1  38064  sstotbnd2  38095  iscringd  38319  lsmsat  39454  lfladdcl  39517  lflnegcl  39521  lflvscl  39523  eqlkr  39545  lshpkrlem4  39559  lshpkrlem6  39561  ldualgrplem  39591  lduallmodlem  39598  latmassOLD  39675  latm12  39676  latm32  39677  latmrot  39678  latmmdiN  39680  latmmdir  39681  omlfh1N  39704  omlfh3N  39705  cvrnbtwn2  39721  cvlexchb1  39776  cvlsupr2  39789  hlatjass  39816  hlatj12  39817  hlatj32  39818  cvrat  39868  cvrat2  39875  atltcvr  39881  atexchltN  39887  cvrat3  39888  cvrat4  39889  atbtwnexOLDN  39893  atbtwnex  39894  3dimlem3  39907  3dimlem3OLDN  39908  3at  39936  2atneat  39961  llncmp  39968  2at0mat0  39971  2atmat0  39972  llncvrlpln  40004  lplncmp  40008  2llnjaN  40012  4atlem11  40055  lplncvrlvol  40062  lvolcmp  40063  2atm2atN  40231  elpaddatriN  40249  paddasslem8  40273  paddass  40284  padd12N  40285  paddssw2  40290  paddss  40291  pmod1i  40294  pmodN  40296  pmapjlln1  40301  atmod1i1  40303  atmod1i2  40305  pexmidlem2N  40417  pl42lem2N  40426  pl42lem3N  40427  pl42lem4N  40428  pl42N  40429  lhpm0atN  40475  lautlt  40537  lautcvr  40538  lautj  40539  lautm  40540  ltrneq2  40594  cdlemd1  40644  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3e  40678  cdlemefr27cl  40849  cdlemefs27cl  40859  cdleme42ke  40931  cdleme42mN  40933  cdlemf2  41008  cdlemftr2  41012  trljco  41186  tgrpgrplem  41195  tendoplass  41229  tendodi1  41230  tendodi2  41231  cdlemk34  41356  cdlemk36  41359  erngdvlem3-rN  41444  tendospdi1  41466  dialss  41492  dvhvaddass  41543  dvhopvsca  41548  dvhlveclem  41554  diblss  41616  diclss  41639  diclspsn  41640  cdlemn11pre  41656  dihmeetlem12N  41764  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem18N  41770  dvh4dimN  41893  lpolconN  41933  dochpolN  41936  lclkr  41979  lclkrs  41985  lcfr  42031  aks6d1c1  42555  irrapxlem6  43255  jm2.26lem3  43429  dgrsub2  43563  mpaaroot  43583  mendring  43616  mendlmod  43617  mendassa  43618  relexpmulg  44137  iunrelexpmin2  44139  relexpxpmin  44144  neicvgel1  44546  grumnud  44713  rfcnpre3  45464  fmuldfeq  46013  xlimbr  46255  stoweidlem43  46471  stoweidlem52  46480  stoweidlem53  46481  stoweidlem56  46484  stoweidlem57  46485  stoweidlem60  46488  issmfle  47173  issmfgt  47184  issmfge  47198  smflimlem4  47202  ltsubsubaddltsub  47743  iccpartigtl  47877  iccelpart  47887  prproropf1olem1  47957  fpprel2  48211  cycl3grtrilem  48416  grlimprclnbgr  48466  upgrwlkupwlk  48610  copissgrp  48638  cznrng  48731  funcringcsetcALTV2lem9  48768  funcringcsetclem9ALTV  48791  ldepsprlem  48942  lincresunit3  48951  lincreslvec3  48952  itsclc0yqe  49231  itsclc0yqsol  49234  resipos  49444  topdlat  49473  catprs  49480  endmndlem  49484  idmon  49489  idepi  49490  thincmon  49902  thincepi  49903  functhinclem1  49913  grptcmon  50062  grptcepi  50063