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  7157  isopolem  7291  fr3nr  7717  sexp3  8094  dif1en  9087  frfi  9186  intrnfi  9320  fisupcl  9374  cnfcomlem  9609  ackbij1lem15  10144  cofsmo  10180  sornom  10188  fpwwe2lem4  10546  dedekindle  11299  supmul1  12114  eluzuzle  12786  xlesubadd  13204  elioc2  13351  elico2  13352  elicc2  13353  fseq1p1m1  13541  fz0fzelfz0  13577  hash7g  14437  swrdsbslen  14616  ccatswrd  14620  swrdswrdlem  14655  wwlktovf1  14908  tanadd  16123  dvds2ln  16247  cshwsidrepsw  17053  ressress  17206  f1ovscpbl  17479  mreexexlem4d  17602  mreexexd  17603  iscatd2  17636  2oppccomf  17680  issubc3  17805  fthmon  17885  fuccocl  17923  fucidcl  17924  invfuc  17933  initoeu2lem0  17969  initoeu2lem1  17970  curf2cl  18186  yonedalem4c  18232  yonedalem3  18235  pospo  18298  latjle12  18405  latjlej1  18408  latnlej2  18414  latlem12  18421  latmlem1  18424  latledi  18432  latjass  18438  latj12  18439  latj32  18440  latj13  18441  latj31  18442  latjrot  18443  latjjdi  18446  latjjdir  18447  latdisdlem  18451  prdssgrpd  18690  prdsmndd  18727  mndissubm  18764  frmdmnd  18816  grpsubrcan  18986  grpsubadd  18993  grpaddsubass  18995  grpsubsub4  18998  grppnpcan2  18999  grpnpncan  19000  mulgnndir  19068  mulgnn0dir  19069  mulgdir  19071  mulgnnass  19074  mulgnn0ass  19075  mulgass  19076  mulgsubdir  19079  pwsmulg  19084  issubg2  19106  eqgval  19141  qusgrp  19150  galcan  19268  gacan  19269  oppgmnd  19318  fvcosymgeq  19393  pmtrprfv  19417  psgnunilem3  19460  cmn32  19764  cmn12  19766  abladdsub  19776  ablsubaddsub  19778  ablsubsub23  19788  mulgdi  19790  mulgsubdi  19793  dprdss  19995  dprdz  19996  dprdf1o  19998  dprdsn  20002  dprd2da  20008  dmdprdsplit  20013  ablfac1b  20036  pgpfac1lem5  20045  prdsrngd  20146  srgdilem  20162  srgbinom  20201  ringdilem  20219  prdsringd  20289  opprrng  20314  mulgass3  20322  dvrass  20377  dvrdir  20381  subrgunit  20556  issubrg2  20558  isdomn4  20682  abvdiv  20795  lsssn0  20932  islss3  20943  prdslmodd  20953  islmhm2  21023  lspsolv  21131  islbs2  21142  islbs3  21143  lbsextlem4  21149  sralmod  21172  rnglidl1  21220  psgndiflemB  21588  ipdir  21627  ipdi  21628  ipsubdir  21630  ipsubdi  21631  ipass  21633  ipassr  21634  ipassr2  21635  isphld  21642  ocvlss  21660  sraassab  21856  psrlmod  21947  psrring  21957  psrassa  21960  mamudm  22369  matring  22417  matassa  22418  ofco2  22425  ma1repveval  22545  mdetunilem1  22586  mdetunilem9  22594  chpscmatgsumbin  22818  iinopn  22876  restopnb  23149  subbascn  23228  nrmsep2  23330  isnrm3  23333  regsep2  23350  dnsconst  23352  dfconn2  23393  1stcelcls  23435  dislly  23471  ptuni2  23550  tx1stc  23624  0nelfb  23805  infil  23837  fsubbas  23841  filssufilg  23885  hauspwpwf1  23961  cnextcn  24041  tmdcn2  24063  ustuqtoplem  24213  utopsnneiplem  24221  psmettri  24285  isxmet2d  24301  xmettri  24325  xmetres2  24335  bldisj  24372  blss2ps  24377  blss2  24378  xmstri2  24440  mstri2  24441  xmstri  24442  mstri  24443  xmstri3  24444  mstri3  24445  msrtri  24446  comet  24487  stdbdbl  24491  met2ndci  24496  ngprcan  24584  ngplcan  24585  ngpsubcan  24588  nmtri2  24601  nrgdsdi  24639  nrgdsdir  24640  nlmdsdi  24655  nlmdsdir  24656  blcvx  24772  icoopnst  24915  pi1grplem  25025  clmpm1dir  25079  cmodscmulexp  25098  cvsdiv  25108  cvsdivcl  25109  cphdivcl  25158  cphsubdir  25184  cphsubdi  25185  tcphcph  25213  bcthlem5  25304  volfiniun  25523  volcn  25582  itg1val2  25660  dvconst  25893  dvlip  25970  ftc1a  26016  ulmval  26360  ulmdvlem3  26382  ang180  26795  cvxcl  26966  scvxcvx  26967  sgmmul  27183  dchrabl  27236  gausslemma2dlem1a  27347  nosupbnd1  27697  noinfbnd1lem5  27710  noinfbnd1  27712  sltsss2  27777  addscom  27977  addbday  28029  motgrp  28630  iscgra1  28897  cgrane1  28899  cgrane3  28901  cgrahl1  28903  cgrahl2  28904  cgracgr  28905  cgratr  28910  cgrabtwn  28913  cgrahl  28914  dfcgra2  28917  sacgr  28918  f1otrge  28959  colinearalglem1  28994  axcgrtr  29003  axeuclidlem  29050  axcontlem3  29054  axcontlem4  29055  axcontlem7  29058  eengtrkg  29074  eengtrkge  29075  edglnl  29231  subgruhgredgd  29372  nbfusgrlevtxm2  29466  lfgriswlk  29775  wwlknbp1  29932  usgrwwlks2on  30046  umgrwwlks2on  30047  rusgrnumwwlks  30065  clwlkclwwlkfo  30099  3spthd  30266  3vfriswmgr  30368  frgr2wwlkeqm  30421  numclwwlk1lem2f  30445  numclwwlk2  30471  numclwwlk3  30475  numclwwlk5  30478  grpomuldivass  30632  ablomuldiv  30643  ablodivdiv4  30645  ablonnncan1  30648  nvmdi  30739  dipassr  30937  archiabllem2c  33276  dvrcan5  33317  rloccring  33351  reofld  33423  eqgvscpbl  33430  qusvsval  33432  quslmod  33438  quslmhm  33439  prmidlc  33528  ssdifidl  33537  ssmxidl  33554  ply1degltlss  33676  r1plmhm  33690  drgextlsp  33758  ccfldsrarelvec  33836  constrconj  33910  constrfin  33911  constrelextdg2  33912  pstmfval  34061  qqhval2lem  34146  qqhvq  34152  measdivcst  34389  measdivcstALTV  34390  carsggect  34483  tgoldbachgtd  34827  bnj1098  34947  bnj149  35038  bnj1118  35147  erdszelem9  35402  resconn  35449  cvmseu  35479  cvmlift2lem10  35515  cvmlift2lem12  35517  ex-sategoelel  35624  elmrsubrn  35723  mclsind  35773  r1peuqusdeg1  35846  cgrid2  36206  segconeu  36214  btwncomim  36216  btwnswapid  36220  trisegint  36231  cgrxfr  36258  brofs2  36280  endofsegid  36288  btwnconn2  36305  seglemin  36316  segletr  36317  btwnsegle  36320  colinbtwnle  36321  broutsideof2  36325  btwnoutside  36328  broutsideof3  36329  outsideoftr  36332  outsidele  36335  fvray  36344  fvline  36347  ellines  36355  weiunpo  36668  broucube  37986  ftc1anc  38033  sdclem1  38075  sstotbnd2  38106  iscringd  38330  lsmsat  39465  lfladdcl  39528  lflnegcl  39532  lflvscl  39534  eqlkr  39556  lshpkrlem4  39570  lshpkrlem6  39572  ldualgrplem  39602  lduallmodlem  39609  latmassOLD  39686  latm12  39687  latm32  39688  latmrot  39689  latmmdiN  39691  latmmdir  39692  omlfh1N  39715  omlfh3N  39716  cvrnbtwn2  39732  cvlexchb1  39787  cvlsupr2  39800  hlatjass  39827  hlatj12  39828  hlatj32  39829  cvrat  39879  cvrat2  39886  atltcvr  39892  atexchltN  39898  cvrat3  39899  cvrat4  39900  atbtwnexOLDN  39904  atbtwnex  39905  3dimlem3  39918  3dimlem3OLDN  39919  3at  39947  2atneat  39972  llncmp  39979  2at0mat0  39982  2atmat0  39983  llncvrlpln  40015  lplncmp  40019  2llnjaN  40023  4atlem11  40066  lplncvrlvol  40073  lvolcmp  40074  2atm2atN  40242  elpaddatriN  40260  paddasslem8  40284  paddass  40295  padd12N  40296  paddssw2  40301  paddss  40302  pmod1i  40305  pmodN  40307  pmapjlln1  40312  atmod1i1  40314  atmod1i2  40316  pexmidlem2N  40428  pl42lem2N  40437  pl42lem3N  40438  pl42lem4N  40439  pl42N  40440  lhpm0atN  40486  lautlt  40548  lautcvr  40549  lautj  40550  lautm  40551  ltrneq2  40605  cdlemd1  40655  cdleme1b  40683  cdleme1  40684  cdleme2  40685  cdleme3e  40689  cdlemefr27cl  40860  cdlemefs27cl  40870  cdleme42ke  40942  cdleme42mN  40944  cdlemf2  41019  cdlemftr2  41023  trljco  41197  tgrpgrplem  41206  tendoplass  41240  tendodi1  41241  tendodi2  41242  cdlemk34  41367  cdlemk36  41370  erngdvlem3-rN  41455  tendospdi1  41477  dialss  41503  dvhvaddass  41554  dvhopvsca  41559  dvhlveclem  41565  diblss  41627  diclss  41650  diclspsn  41651  cdlemn11pre  41667  dihmeetlem12N  41775  dihmeetlem16N  41779  dihmeetlem17N  41780  dihmeetlem18N  41781  dvh4dimN  41904  lpolconN  41944  dochpolN  41947  lclkr  41990  lclkrs  41996  lcfr  42042  aks6d1c1  42566  irrapxlem6  43270  jm2.26lem3  43444  dgrsub2  43578  mpaaroot  43598  mendring  43631  mendlmod  43632  mendassa  43633  relexpmulg  44152  iunrelexpmin2  44154  relexpxpmin  44159  neicvgel1  44561  grumnud  44728  rfcnpre3  45479  fmuldfeq  46028  xlimbr  46270  stoweidlem43  46486  stoweidlem52  46495  stoweidlem53  46496  stoweidlem56  46499  stoweidlem57  46500  stoweidlem60  46503  issmfle  47188  issmfgt  47199  issmfge  47213  smflimlem4  47217  ltsubsubaddltsub  47746  iccpartigtl  47880  iccelpart  47890  prproropf1olem1  47960  fpprel2  48214  cycl3grtrilem  48419  grlimprclnbgr  48469  upgrwlkupwlk  48613  copissgrp  48641  cznrng  48734  funcringcsetcALTV2lem9  48771  funcringcsetclem9ALTV  48794  ldepsprlem  48945  lincresunit3  48954  lincreslvec3  48955  itsclc0yqe  49234  itsclc0yqsol  49237  resipos  49447  topdlat  49476  catprs  49483  endmndlem  49487  idmon  49492  idepi  49493  thincmon  49905  thincepi  49906  functhinclem1  49916  grptcmon  50065  grptcepi  50066