Theorem simpr2 1194

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpr12  1257  simpr22  1260  simpr32  1263  simp1r2  1269  simp2r2  1275  simp3r2  1281  3anandis  1470  fpr2g  7096  isopolem  7225  fr3nr  7631  frfi  9068  intrnfi  9184  fisupcl  9237  cnfcomlem  9466  ackbij1lem15  9999  cofsmo  10034  sornom  10042  fpwwe2lem4  10399  dedekindle  11148  supmul1  11953  eluzuzle  12600  xlesubadd  13006  elioc2  13151  elico2  13152  elicc2  13153  fseq1p1m1  13339  fz0fzelfz0  13371  swrdsbslen  14386  ccatswrd  14390  swrdswrdlem  14426  wwlktovf1  14681  tanadd  15885  dvds2ln  16007  cshwsidrepsw  16804  ressress  16967  f1ovscpbl  17246  mreexexlem4d  17365  mreexexd  17366  iscatd2  17399  2oppccomf  17445  issubc3  17573  fthmon  17652  fuccocl  17691  fucidcl  17692  invfuc  17701  initoeu2lem0  17737  initoeu2lem1  17738  curf2cl  17958  yonedalem4c  18004  yonedalem3  18007  pospo  18072  latjle12  18177  latjlej1  18180  latnlej2  18186  latlem12  18193  latmlem1  18196  latledi  18204  latjass  18210  latj12  18211  latj32  18212  latj13  18213  latj31  18214  latjrot  18215  latjjdi  18218  latjjdir  18219  latdisdlem  18223  prdsmndd  18427  mndissubm  18455  frmdmnd  18507  grpsubrcan  18665  grpsubadd  18672  grpaddsubass  18674  grpsubsub4  18677  grppnpcan2  18678  grpnpncan  18679  mulgnndir  18741  mulgnn0dir  18742  mulgdir  18744  mulgnnass  18747  mulgnn0ass  18748  mulgass  18749  mulgsubdir  18752  pwsmulg  18757  issubg2  18779  eqgval  18814  qusgrp  18820  galcan  18919  gacan  18920  oppgmnd  18970  fvcosymgeq  19046  pmtrprfv  19070  psgnunilem3  19113  cmn32  19414  cmn12  19416  abladdsub  19425  ablsubsub23  19435  mulgdi  19437  mulgsubdi  19440  dprdss  19641  dprdz  19642  dprdf1o  19644  dprdsn  19648  dprd2da  19654  dmdprdsplit  19659  ablfac1b  19682  pgpfac1lem5  19691  srgi  19756  srgbinom  19790  ringi  19808  prdsringd  19860  opprring  19882  mulgass3  19888  dvrass  19941  subrgunit  20051  issubrg2  20053  abvdiv  20106  lsssn0  20218  islss3  20230  prdslmodd  20240  islmhm2  20309  lspsolv  20414  islbs2  20425  islbs3  20426  lbsextlem4  20432  sralmod  20466  psgndiflemB  20814  ipdir  20853  ipdi  20854  ipsubdir  20856  ipsubdi  20857  ipass  20859  ipassr  20860  ipassr2  20861  isphld  20868  ocvlss  20886  sraassa  21083  psrbaglesuppOLD  21137  psrbagleclOLD  21139  psrbagconOLD  21143  psrgrp  21176  psrlmod  21179  psrring  21189  psrassa  21192  mamudm  21546  matring  21601  matassa  21602  ofco2  21609  ma1repveval  21729  mdetunilem1  21770  mdetunilem9  21778  chpscmatgsumbin  22002  iinopn  22060  restopnb  22335  subbascn  22414  nrmsep2  22516  isnrm3  22519  regsep2  22536  dnsconst  22538  dfconn2  22579  1stcelcls  22621  dislly  22657  ptuni2  22736  tx1stc  22810  0nelfb  22991  infil  23023  fsubbas  23027  filssufilg  23071  hauspwpwf1  23147  cnextcn  23227  tmdcn2  23249  ustuqtoplem  23400  utopsnneiplem  23408  psmettri  23473  isxmet2d  23489  xmettri  23513  xmetres2  23523  bldisj  23560  blss2ps  23565  blss2  23566  xmstri2  23628  mstri2  23629  xmstri  23630  mstri  23631  xmstri3  23632  mstri3  23633  msrtri  23634  comet  23678  stdbdbl  23682  met2ndci  23687  ngprcan  23775  ngplcan  23776  ngpsubcan  23779  nmtri2  23792  nrgdsdi  23838  nrgdsdir  23839  nlmdsdi  23854  nlmdsdir  23855  blcvx  23970  icoopnst  24111  pi1grplem  24221  clmpm1dir  24275  cmodscmulexp  24294  cvsdiv  24304  cvsdivcl  24305  cphdivcl  24355  cphsubdir  24381  cphsubdi  24382  tcphcph  24410  bcthlem5  24501  volfiniun  24720  volcn  24779  itg1val2  24857  dvconst  25090  dvlip  25166  ftc1a  25210  ulmval  25548  ulmdvlem3  25570  ang180  25973  cvxcl  26143  scvxcvx  26144  sgmmul  26358  dchrabl  26411  gausslemma2dlem1a  26522  motgrp  26913  iscgra1  27180  cgrane1  27182  cgrane3  27184  cgrahl1  27186  cgrahl2  27187  cgracgr  27188  cgratr  27193  cgrabtwn  27196  cgrahl  27197  dfcgra2  27200  sacgr  27201  f1otrge  27242  colinearalglem1  27283  axcgrtr  27292  axeuclidlem  27339  axcontlem3  27343  axcontlem4  27344  axcontlem7  27347  eengtrkg  27363  eengtrkge  27364  edglnl  27522  subgruhgredgd  27660  nbfusgrlevtxm2  27754  lfgriswlk  28065  wwlknbp1  28218  umgrwwlks2on  28331  rusgrnumwwlks  28348  clwlkclwwlkfo  28382  3spthd  28549  3vfriswmgr  28651  frgr2wwlkeqm  28704  numclwwlk1lem2f  28728  numclwwlk2  28754  numclwwlk3  28758  numclwwlk5  28761  grpomuldivass  28912  ablomuldiv  28923  ablodivdiv4  28925  ablonnncan1  28928  nvmdi  29019  dipassr  29217  archiabllem2c  31458  dvrdir  31496  dvrcan5  31499  reofld  31553  eqgvscpbl  31559  qusscaval  31561  quslmod  31563  quslmhm  31564  prmidlc  31633  ssmxidl  31651  drgextlsp  31690  ccfldsrarelvec  31750  pstmfval  31855  qqhval2lem  31940  qqhvq  31946  measdivcst  32201  measdivcstALTV  32202  carsggect  32294  tgoldbachgtd  32651  bnj1098  32772  bnj149  32864  bnj1118  32973  erdszelem9  33170  resconn  33217  cvmseu  33247  cvmlift2lem10  33283  cvmlift2lem12  33285  ex-sategoelel  33392  elmrsubrn  33491  mclsind  33541  xpord3pred  33807  sexp3  33808  nosupbnd1  33926  noinfbnd1lem5  33939  noinfbnd1  33941  ssltss2  33993  addscom  34138  cgrid2  34314  segconeu  34322  btwncomim  34324  btwnswapid  34328  trisegint  34339  cgrxfr  34366  brofs2  34388  endofsegid  34396  btwnconn2  34413  seglemin  34424  segletr  34425  btwnsegle  34428  colinbtwnle  34429  broutsideof2  34433  btwnoutside  34436  broutsideof3  34437  outsideoftr  34440  outsidele  34443  fvray  34452  fvline  34455  ellines  34463  broucube  35820  ftc1anc  35867  sdclem1  35910  sstotbnd2  35941  iscringd  36165  lsmsat  37029  lfladdcl  37092  lflnegcl  37096  lflvscl  37098  eqlkr  37120  lshpkrlem4  37134  lshpkrlem6  37136  ldualgrplem  37166  lduallmodlem  37173  latmassOLD  37250  latm12  37251  latm32  37252  latmrot  37253  latmmdiN  37255  latmmdir  37256  omlfh1N  37279  omlfh3N  37280  cvrnbtwn2  37296  cvlexchb1  37351  cvlsupr2  37364  hlatjass  37391  hlatj12  37392  hlatj32  37393  cvrat  37443  cvrat2  37450  atltcvr  37456  atexchltN  37462  cvrat3  37463  cvrat4  37464  atbtwnexOLDN  37468  atbtwnex  37469  3dimlem3  37482  3dimlem3OLDN  37483  3at  37511  2atneat  37536  llncmp  37543  2at0mat0  37546  2atmat0  37547  llncvrlpln  37579  lplncmp  37583  2llnjaN  37587  4atlem11  37630  lplncvrlvol  37637  lvolcmp  37638  2atm2atN  37806  elpaddatriN  37824  paddasslem8  37848  paddass  37859  padd12N  37860  paddssw2  37865  paddss  37866  pmod1i  37869  pmodN  37871  pmapjlln1  37876  atmod1i1  37878  atmod1i2  37880  pexmidlem2N  37992  pl42lem2N  38001  pl42lem3N  38002  pl42lem4N  38003  pl42N  38004  lhpm0atN  38050  lautlt  38112  lautcvr  38113  lautj  38114  lautm  38115  ltrneq2  38169  cdlemd1  38219  cdleme1b  38247  cdleme1  38248  cdleme2  38249  cdleme3e  38253  cdlemefr27cl  38424  cdlemefs27cl  38434  cdleme42ke  38506  cdleme42mN  38508  cdlemf2  38583  cdlemftr2  38587  trljco  38761  tgrpgrplem  38770  tendoplass  38804  tendodi1  38805  tendodi2  38806  cdlemk34  38931  cdlemk36  38934  erngdvlem3-rN  39019  tendospdi1  39041  dialss  39067  dvhvaddass  39118  dvhopvsca  39123  dvhlveclem  39129  diblss  39191  diclss  39214  diclspsn  39215  cdlemn11pre  39231  dihmeetlem12N  39339  dihmeetlem16N  39343  dihmeetlem17N  39344  dihmeetlem18N  39345  dvh4dimN  39468  lpolconN  39508  dochpolN  39511  lclkr  39554  lclkrs  39560  lcfr  39606  isdomn4  40179  irrapxlem6  40656  jm2.26lem3  40830  dgrsub2  40967  mpaaroot  40987  mendring  41024  mendlmod  41025  mendassa  41026  relexpmulg  41325  iunrelexpmin2  41327  relexpxpmin  41332  neicvgel1  41736  grumnud  41911  rfcnpre3  42583  fmuldfeq  43131  xlimbr  43375  stoweidlem43  43591  stoweidlem52  43600  stoweidlem53  43601  stoweidlem56  43604  stoweidlem57  43605  stoweidlem60  43608  issmfle  44290  issmfgt  44301  issmfge  44315  smflimlem4  44319  ltsubsubaddltsub  44804  iccpartigtl  44886  iccelpart  44896  prproropf1olem1  44966  fpprel2  45204  upgrwlkupwlk  45313  copissgrp  45373  cznrng  45524  funcringcsetcALTV2lem9  45613  funcringcsetclem9ALTV  45636  ldepsprlem  45824  lincresunit3  45833  lincreslvec3  45834  itsclc0yqe  46118  itsclc0yqsol  46121  topdlat  46301  catprs  46303  endmndlem  46307  idmon  46308  idepi  46309  thincmon  46326  thincepi  46327  functhinclem1  46333  grptcmon  46388  grptcepi  46389