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  7203  isopolem  7338  fr3nr  7766  sexp3  8152  dif1en  9174  frfi  9293  intrnfi  9428  fisupcl  9482  cnfcomlem  9713  ackbij1lem15  10247  cofsmo  10283  sornom  10291  fpwwe2lem4  10648  dedekindle  11399  supmul1  12211  eluzuzle  12861  xlesubadd  13279  elioc2  13426  elico2  13427  elicc2  13428  fseq1p1m1  13615  fz0fzelfz0  13651  hash7g  14504  swrdsbslen  14682  ccatswrd  14686  swrdswrdlem  14722  wwlktovf1  14976  tanadd  16185  dvds2ln  16308  cshwsidrepsw  17113  ressress  17268  f1ovscpbl  17540  mreexexlem4d  17659  mreexexd  17660  iscatd2  17693  2oppccomf  17737  issubc3  17862  fthmon  17942  fuccocl  17980  fucidcl  17981  invfuc  17990  initoeu2lem0  18026  initoeu2lem1  18027  curf2cl  18243  yonedalem4c  18289  yonedalem3  18292  pospo  18355  latjle12  18460  latjlej1  18463  latnlej2  18469  latlem12  18476  latmlem1  18479  latledi  18487  latjass  18493  latj12  18494  latj32  18495  latj13  18496  latj31  18497  latjrot  18498  latjjdi  18501  latjjdir  18502  latdisdlem  18506  prdssgrpd  18711  prdsmndd  18748  mndissubm  18785  frmdmnd  18837  grpsubrcan  19004  grpsubadd  19011  grpaddsubass  19013  grpsubsub4  19016  grppnpcan2  19017  grpnpncan  19018  mulgnndir  19086  mulgnn0dir  19087  mulgdir  19089  mulgnnass  19092  mulgnn0ass  19093  mulgass  19094  mulgsubdir  19097  pwsmulg  19102  issubg2  19124  eqgval  19160  qusgrp  19169  galcan  19287  gacan  19288  oppgmnd  19337  fvcosymgeq  19410  pmtrprfv  19434  psgnunilem3  19477  cmn32  19781  cmn12  19783  abladdsub  19793  ablsubaddsub  19795  ablsubsub23  19805  mulgdi  19807  mulgsubdi  19810  dprdss  20012  dprdz  20013  dprdf1o  20015  dprdsn  20019  dprd2da  20025  dmdprdsplit  20030  ablfac1b  20053  pgpfac1lem5  20062  prdsrngd  20136  srgdilem  20152  srgbinom  20191  ringdilem  20209  prdsringd  20281  opprrng  20305  mulgass3  20313  dvrass  20368  dvrdir  20372  subrgunit  20550  issubrg2  20552  isdomn4  20676  abvdiv  20789  lsssn0  20905  islss3  20916  prdslmodd  20926  islmhm2  20996  lspsolv  21104  islbs2  21115  islbs3  21116  lbsextlem4  21122  sralmod  21145  rnglidl1  21193  psgndiflemB  21560  ipdir  21599  ipdi  21600  ipsubdir  21602  ipsubdi  21603  ipass  21605  ipassr  21606  ipassr2  21607  isphld  21614  ocvlss  21632  sraassab  21828  sraassaOLD  21830  psrgrpOLD  21917  psrlmod  21920  psrring  21930  psrassa  21933  mamudm  22333  matring  22381  matassa  22382  ofco2  22389  ma1repveval  22509  mdetunilem1  22550  mdetunilem9  22558  chpscmatgsumbin  22782  iinopn  22840  restopnb  23113  subbascn  23192  nrmsep2  23294  isnrm3  23297  regsep2  23314  dnsconst  23316  dfconn2  23357  1stcelcls  23399  dislly  23435  ptuni2  23514  tx1stc  23588  0nelfb  23769  infil  23801  fsubbas  23805  filssufilg  23849  hauspwpwf1  23925  cnextcn  24005  tmdcn2  24027  ustuqtoplem  24178  utopsnneiplem  24186  psmettri  24250  isxmet2d  24266  xmettri  24290  xmetres2  24300  bldisj  24337  blss2ps  24342  blss2  24343  xmstri2  24405  mstri2  24406  xmstri  24407  mstri  24408  xmstri3  24409  mstri3  24410  msrtri  24411  comet  24452  stdbdbl  24456  met2ndci  24461  ngprcan  24549  ngplcan  24550  ngpsubcan  24553  nmtri2  24566  nrgdsdi  24604  nrgdsdir  24605  nlmdsdi  24620  nlmdsdir  24621  blcvx  24737  icoopnst  24887  pi1grplem  25000  clmpm1dir  25054  cmodscmulexp  25073  cvsdiv  25083  cvsdivcl  25084  cphdivcl  25134  cphsubdir  25160  cphsubdi  25161  tcphcph  25189  bcthlem5  25280  volfiniun  25500  volcn  25559  itg1val2  25637  dvconst  25870  dvlip  25950  ftc1a  25996  ulmval  26341  ulmdvlem3  26363  ang180  26776  cvxcl  26947  scvxcvx  26948  sgmmul  27164  dchrabl  27217  gausslemma2dlem1a  27328  nosupbnd1  27678  noinfbnd1lem5  27691  noinfbnd1  27693  ssltss2  27753  addscom  27925  addsbday  27976  motgrp  28522  iscgra1  28789  cgrane1  28791  cgrane3  28793  cgrahl1  28795  cgrahl2  28796  cgracgr  28797  cgratr  28802  cgrabtwn  28805  cgrahl  28806  dfcgra2  28809  sacgr  28810  f1otrge  28851  colinearalglem1  28885  axcgrtr  28894  axeuclidlem  28941  axcontlem3  28945  axcontlem4  28946  axcontlem7  28949  eengtrkg  28965  eengtrkge  28966  edglnl  29122  subgruhgredgd  29263  nbfusgrlevtxm2  29357  lfgriswlk  29668  wwlknbp1  29826  umgrwwlks2on  29939  rusgrnumwwlks  29956  clwlkclwwlkfo  29990  3spthd  30157  3vfriswmgr  30259  frgr2wwlkeqm  30312  numclwwlk1lem2f  30336  numclwwlk2  30362  numclwwlk3  30366  numclwwlk5  30369  grpomuldivass  30522  ablomuldiv  30533  ablodivdiv4  30535  ablonnncan1  30538  nvmdi  30629  dipassr  30827  archiabllem2c  33193  dvrcan5  33231  rloccring  33265  reofld  33359  eqgvscpbl  33365  qusvsval  33367  quslmod  33373  quslmhm  33374  prmidlc  33463  ssdifidl  33472  ssmxidl  33489  ply1degltlss  33606  r1plmhm  33619  drgextlsp  33633  ccfldsrarelvec  33712  constrconj  33779  constrfin  33780  constrelextdg2  33781  pstmfval  33927  qqhval2lem  34012  qqhvq  34018  measdivcst  34255  measdivcstALTV  34256  carsggect  34350  tgoldbachgtd  34694  bnj1098  34814  bnj149  34906  bnj1118  35015  erdszelem9  35221  resconn  35268  cvmseu  35298  cvmlift2lem10  35334  cvmlift2lem12  35336  ex-sategoelel  35443  elmrsubrn  35542  mclsind  35592  r1peuqusdeg1  35665  cgrid2  36021  segconeu  36029  btwncomim  36031  btwnswapid  36035  trisegint  36046  cgrxfr  36073  brofs2  36095  endofsegid  36103  btwnconn2  36120  seglemin  36131  segletr  36132  btwnsegle  36135  colinbtwnle  36136  broutsideof2  36140  btwnoutside  36143  broutsideof3  36144  outsideoftr  36147  outsidele  36150  fvray  36159  fvline  36162  ellines  36170  weiunpo  36483  broucube  37678  ftc1anc  37725  sdclem1  37767  sstotbnd2  37798  iscringd  38022  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  39441  cvrat2  39448  atltcvr  39454  atexchltN  39460  cvrat3  39461  cvrat4  39462  atbtwnexOLDN  39466  atbtwnex  39467  3dimlem3  39480  3dimlem3OLDN  39481  3at  39509  2atneat  39534  llncmp  39541  2at0mat0  39544  2atmat0  39545  llncvrlpln  39577  lplncmp  39581  2llnjaN  39585  4atlem11  39628  lplncvrlvol  39635  lvolcmp  39636  2atm2atN  39804  elpaddatriN  39822  paddasslem8  39846  paddass  39857  padd12N  39858  paddssw2  39863  paddss  39864  pmod1i  39867  pmodN  39869  pmapjlln1  39874  atmod1i1  39876  atmod1i2  39878  pexmidlem2N  39990  pl42lem2N  39999  pl42lem3N  40000  pl42lem4N  40001  pl42N  40002  lhpm0atN  40048  lautlt  40110  lautcvr  40111  lautj  40112  lautm  40113  ltrneq2  40167  cdlemd1  40217  cdleme1b  40245  cdleme1  40246  cdleme2  40247  cdleme3e  40251  cdlemefr27cl  40422  cdlemefs27cl  40432  cdleme42ke  40504  cdleme42mN  40506  cdlemf2  40581  cdlemftr2  40585  trljco  40759  tgrpgrplem  40768  tendoplass  40802  tendodi1  40803  tendodi2  40804  cdlemk34  40929  cdlemk36  40932  erngdvlem3-rN  41017  tendospdi1  41039  dialss  41065  dvhvaddass  41116  dvhopvsca  41121  dvhlveclem  41127  diblss  41189  diclss  41212  diclspsn  41213  cdlemn11pre  41229  dihmeetlem12N  41337  dihmeetlem16N  41341  dihmeetlem17N  41342  dihmeetlem18N  41343  dvh4dimN  41466  lpolconN  41506  dochpolN  41509  lclkr  41552  lclkrs  41558  lcfr  41604  aks6d1c1  42129  irrapxlem6  42850  jm2.26lem3  43025  dgrsub2  43159  mpaaroot  43179  mendring  43212  mendlmod  43213  mendassa  43214  relexpmulg  43734  iunrelexpmin2  43736  relexpxpmin  43741  neicvgel1  44143  grumnud  44310  rfcnpre3  45057  fmuldfeq  45612  xlimbr  45856  stoweidlem43  46072  stoweidlem52  46081  stoweidlem53  46082  stoweidlem56  46085  stoweidlem57  46086  stoweidlem60  46089  issmfle  46774  issmfgt  46785  issmfge  46799  smflimlem4  46803  ltsubsubaddltsub  47330  iccpartigtl  47437  iccelpart  47447  prproropf1olem1  47517  fpprel2  47755  cycl3grtrilem  47958  grlimgrtrilem1  48006  upgrwlkupwlk  48115  copissgrp  48143  cznrng  48236  funcringcsetcALTV2lem9  48273  funcringcsetclem9ALTV  48296  ldepsprlem  48448  lincresunit3  48457  lincreslvec3  48458  itsclc0yqe  48741  itsclc0yqsol  48744  resipos  48949  topdlat  48978  catprs  48986  endmndlem  48990  idmon  48995  idepi  48996  thincmon  49319  thincepi  49320  functhinclem1  49330  grptcmon  49470  grptcepi  49471