Theorem simpr2 1212

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpr12  1275  simpr22  1278  simpr32  1281  simp1r2  1287  simp2r2  1293  simp3r2  1299  3anandis  1495  fpr2g  7199  isopolem  7333  fr3nr  7759  sexp3  8137  dif1en  9134  frfi  9233  intrnfi  9364  fisupcl  9418  cnfcomlem  9656  ackbij1lem15  10204  cofsmo  10241  sornom  10249  fpwwe2lem4  10607  dedekindle  11362  supmul1  12175  eluzuzle  12862  xlesubadd  13280  elioc2  13427  elico2  13428  elicc2  13429  fseq1p1m1  13617  fz0fzelfz0  13653  hash7g  14513  swrdsbslen  14692  ccatswrd  14696  swrdswrdlem  14731  wwlktovf1  14984  tanadd  16213  dvds2ln  16337  cshwsidrepsw  17143  ressress  17297  f1ovscpbl  17570  mreexexlem4d  17693  mreexexd  17694  iscatd2  17727  2oppccomf  17771  issubc3  17896  fthmon  17976  fuccocl  18014  fucidcl  18015  invfuc  18024  initoeu2lem0  18060  initoeu2lem1  18061  curf2cl  18277  yonedalem4c  18323  yonedalem3  18326  pospo  18389  latjle12  18496  latjlej1  18499  latnlej2  18505  latlem12  18512  latmlem1  18515  latledi  18523  latjass  18529  latj12  18530  latj32  18531  latj13  18532  latj31  18533  latjrot  18534  latjjdi  18537  latjjdir  18538  latdisdlem  18542  prdssgrpd  18781  prdsmndd  18818  mndissubm  18855  frmdmnd  18908  grpsubrcan  19078  grpsubadd  19085  grpaddsubass  19087  grpsubsub4  19090  grppnpcan2  19091  grpnpncan  19092  mulgnndir  19160  mulgnn0dir  19161  mulgdir  19163  mulgnnass  19166  mulgnn0ass  19167  mulgass  19168  mulgsubdir  19171  pwsmulg  19176  issubg2  19199  eqgval  19236  qusgrp  19248  galcan  19365  gacan  19366  oppgmnd  19415  fvcosymgeq  19490  pmtrprfv  19514  psgnunilem3  19557  cmn32  19861  cmn12  19863  abladdsub  19873  ablsubaddsub  19875  ablsubsub23  19885  mulgdi  19887  mulgsubdi  19890  dprdss  20092  dprdz  20093  dprdf1o  20095  dprdsn  20099  dprd2da  20105  dmdprdsplit  20110  ablfac1b  20133  pgpfac1lem5  20142  prdsrngd  20245  srgdilem  20265  srgbinom  20304  ringdilem  20322  prdsringd  20393  opprrng  20418  mulgass3  20426  dvrass  20481  dvrdir  20485  subrgunit  20666  issubrg2  20668  isdomn4  20791  abvdiv  20901  lsssn0  21038  islss3  21049  prdslmodd  21059  islmhm2  21128  lspsolv  21236  islbs2  21247  islbs3  21248  lbsextlem4  21254  sralmod  21277  rnglidl1  21327  prmidlc  21435  ssdifidl  21445  psgndiflemB  21710  ipdir  21749  ipdi  21750  ipsubdir  21752  ipsubdi  21753  ipass  21755  ipassr  21756  ipassr2  21757  isphld  21764  ocvlss  21782  sraassab  21978  psrlmod  22069  psrring  22079  psrassa  22082  mamudm  22513  matring  22561  matassa  22562  ofco2  22569  ma1repveval  22689  mdetunilem1  22730  mdetunilem9  22738  chpscmatgsumbin  22962  iinopn  23020  restopnb  23293  subbascn  23372  nrmsep2  23474  isnrm3  23477  regsep2  23494  dnsconst  23496  dfconn2  23537  1stcelcls  23579  dislly  23615  ptuni2  23694  tx1stc  23768  0nelfb  23949  infil  23981  fsubbas  23985  filssufilg  24029  hauspwpwf1  24105  cnextcn  24185  tmdcn2  24207  ustuqtoplem  24357  utopsnneiplem  24365  psmettri  24429  isxmet2d  24445  xmettri  24469  xmetres2  24479  bldisj  24516  blss2ps  24521  blss2  24522  xmstri2  24584  mstri2  24585  xmstri  24586  mstri  24587  xmstri3  24588  mstri3  24589  msrtri  24590  comet  24631  stdbdbl  24635  met2ndci  24640  ngprcan  24728  ngplcan  24729  ngpsubcan  24732  nmtri2  24745  nrgdsdi  24783  nrgdsdir  24784  nlmdsdi  24799  nlmdsdir  24800  blcvx  24916  icoopnst  25059  pi1grplem  25169  clmpm1dir  25223  cmodscmulexp  25242  cvsdiv  25252  cvsdivcl  25253  cphdivcl  25302  cphsubdir  25328  cphsubdi  25329  tcphcph  25357  bcthlem5  25448  volfiniun  25667  volcn  25726  itg1val2  25804  dvconst  26037  dvlip  26113  ftc1a  26157  ulmval  26501  ulmdvlem3  26523  ang180  26937  cvxcl  27107  scvxcvx  27108  sgmmul  27323  dchrabl  27376  gausslemma2dlem1a  27487  nosupbnd1  27836  noinfbnd1lem5  27849  noinfbnd1  27851  sltsss2  27917  addscom  28117  addbday  28169  motgrp  28770  iscgra1  29062  cgrane1  29064  cgrane3  29066  cgrahl1  29068  cgrahl2  29069  cgracgr  29070  cgratr  29075  cgrabtwn  29078  cgrahl  29079  dfcgra2  29082  sacgr  29083  f1otrge  29130  colinearalglem1  29165  axcgrtr  29174  axeuclidlem  29221  axcontlem3  29225  axcontlem4  29226  axcontlem7  29229  eengtrkg  29245  eengtrkge  29246  edglnl  29402  subgruhgredgd  29543  nbfusgrlevtxm2  29637  lfgriswlk  29945  wwlknbp1  30102  usgrwwlks2on  30216  umgrwwlks2on  30217  rusgrnumwwlks  30235  clwlkclwwlkfo  30269  3spthd  30436  3vfriswmgr  30538  frgr2wwlkeqm  30591  numclwwlk1lem2f  30615  numclwwlk2  30641  numclwwlk3  30645  numclwwlk5  30648  grpomuldivass  30802  ablomuldiv  30813  ablodivdiv4  30815  ablonnncan1  30818  nvmdi  30909  dipassr  31107  archiabllem2c  33428  dvrcan5  33468  rloccring  33504  reofld  33578  eqgvscpbl  33585  qusvsval  33587  quslmod  33593  quslmhm  33594  ssmxidl  33674  ply1degltlss  33803  r1plmhm  33816  drgextlsp  33901  ccfldsrarelvec  33978  constrconj  34052  constrfin  34053  constrelextdg2  34054  pstmfval  34203  qqhval2lem  34288  qqhvq  34294  measdivcst  34531  measdivcstALTV  34532  carsggect  34625  tgoldbachgtd  34966  bnj1098  35089  bnj149  35180  bnj1118  35289  erdszelem9  35562  resconn  35609  cvmseu  35639  cvmlift2lem10  35675  cvmlift2lem12  35677  ex-sategoelel  35784  elmrsubrn  35883  mclsind  35933  r1peuqusdeg1  36006  cgrid2  36366  segconeu  36374  btwncomim  36376  btwnswapid  36380  trisegint  36391  cgrxfr  36418  brofs2  36440  endofsegid  36448  btwnconn2  36465  seglemin  36476  segletr  36477  btwnsegle  36480  colinbtwnle  36481  broutsideof2  36485  btwnoutside  36488  broutsideof3  36489  outsideoftr  36492  outsidele  36495  fvray  36504  fvline  36507  ellines  36515  nmulprop  36553  weiunpo  36838  broucube  38165  ftc1anc  38212  sdclem1  38254  sstotbnd2  38285  iscringd  38509  lsmsat  39644  lfladdcl  39707  lflnegcl  39711  lflvscl  39713  eqlkr  39735  lshpkrlem4  39749  lshpkrlem6  39751  ldualgrplem  39781  lduallmodlem  39788  latmassOLD  39865  latm12  39866  latm32  39867  latmrot  39868  latmmdiN  39870  latmmdir  39871  omlfh1N  39894  omlfh3N  39895  cvrnbtwn2  39911  cvlexchb1  39966  cvlsupr2  39979  hlatjass  40006  hlatj12  40007  hlatj32  40008  cvrat  40058  cvrat2  40065  atltcvr  40071  atexchltN  40077  cvrat3  40078  cvrat4  40079  atbtwnexOLDN  40083  atbtwnex  40084  3dimlem3  40097  3dimlem3OLDN  40098  3at  40126  2atneat  40151  llncmp  40158  2at0mat0  40161  2atmat0  40162  llncvrlpln  40194  lplncmp  40198  2llnjaN  40202  4atlem11  40245  lplncvrlvol  40252  lvolcmp  40253  2atm2atN  40421  elpaddatriN  40439  paddasslem8  40463  paddass  40474  padd12N  40475  paddssw2  40480  paddss  40481  pmod1i  40484  pmodN  40486  pmapjlln1  40491  atmod1i1  40493  atmod1i2  40495  pexmidlem2N  40607  pl42lem2N  40616  pl42lem3N  40617  pl42lem4N  40618  pl42N  40619  lhpm0atN  40665  lautlt  40727  lautcvr  40728  lautj  40729  lautm  40730  ltrneq2  40784  cdlemd1  40834  cdleme1b  40862  cdleme1  40863  cdleme2  40864  cdleme3e  40868  cdlemefr27cl  41039  cdlemefs27cl  41049  cdleme42ke  41121  cdleme42mN  41123  cdlemf2  41198  cdlemftr2  41202  trljco  41376  tgrpgrplem  41385  tendoplass  41419  tendodi1  41420  tendodi2  41421  cdlemk34  41546  cdlemk36  41549  erngdvlem3-rN  41634  tendospdi1  41656  dialss  41682  dvhvaddass  41733  dvhopvsca  41738  dvhlveclem  41744  diblss  41806  diclss  41829  diclspsn  41830  cdlemn11pre  41846  dihmeetlem12N  41954  dihmeetlem16N  41958  dihmeetlem17N  41959  dihmeetlem18N  41960  dvh4dimN  42083  lpolconN  42123  dochpolN  42126  lclkr  42169  lclkrs  42175  lcfr  42221  aks6d1c1  42745  irrapxlem6  43416  jm2.26lem3  43590  dgrsub2  43724  mpaaroot  43744  mendring  43777  mendlmod  43778  mendassa  43779  relexpmulg  44298  iunrelexpmin2  44300  relexpxpmin  44305  neicvgel1  44707  grumnud  44860  rfcnpre3  45611  fmuldfeq  46157  xlimbr  46399  stoweidlem43  46615  stoweidlem52  46624  stoweidlem53  46625  stoweidlem56  46628  stoweidlem57  46629  stoweidlem60  46632  issmfle  47317  issmfgt  47328  issmfge  47342  smflimlem4  47346  ltsubsubaddltsub  47893  iccpartigtl  48027  iccelpart  48037  prproropf1olem1  48107  fpprel2  48361  cycl3grtrilem  48566  grlimprclnbgr  48616  upgrwlkupwlk  48760  copissgrp  48788  cznrng  48881  funcringcsetcALTV2lem9  48918  funcringcsetclem9ALTV  48941  ldepsprlem  49103  lincresunit3  49112  lincreslvec3  49113  itsclc0yqe  49392  itsclc0yqsol  49395  resipos  49604  topdlat  49633  catprs  49640  endmndlem  49644  idmon  49649  idepi  49650  thincmon  50062  thincepi  50063  functhinclem1  50073  grptcmon  50222  grptcepi  50223