Theorem simpr2 1208

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpr12  1271  simpr22  1274  simpr32  1277  simp1r2  1283  simp2r2  1289  simp3r2  1295  3anandis  1491  fpr2g  7189  isopolem  7323  fr3nr  7749  sexp3  8126  dif1en  9124  frfi  9223  intrnfi  9357  fisupcl  9411  cnfcomlem  9649  ackbij1lem15  10184  cofsmo  10221  sornom  10229  fpwwe2lem4  10587  dedekindle  11342  supmul1  12156  eluzuzle  12843  xlesubadd  13261  elioc2  13408  elico2  13409  elicc2  13410  fseq1p1m1  13598  fz0fzelfz0  13634  hash7g  14494  swrdsbslen  14673  ccatswrd  14677  swrdswrdlem  14712  wwlktovf1  14965  tanadd  16180  dvds2ln  16304  cshwsidrepsw  17110  ressress  17264  f1ovscpbl  17537  mreexexlem4d  17660  mreexexd  17661  iscatd2  17694  2oppccomf  17738  issubc3  17863  fthmon  17943  fuccocl  17981  fucidcl  17982  invfuc  17991  initoeu2lem0  18027  initoeu2lem1  18028  curf2cl  18244  yonedalem4c  18290  yonedalem3  18293  pospo  18356  latjle12  18463  latjlej1  18466  latnlej2  18472  latlem12  18479  latmlem1  18482  latledi  18490  latjass  18496  latj12  18497  latj32  18498  latj13  18499  latj31  18500  latjrot  18501  latjjdi  18504  latjjdir  18505  latdisdlem  18509  prdssgrpd  18748  prdsmndd  18785  mndissubm  18822  frmdmnd  18874  grpsubrcan  19044  grpsubadd  19051  grpaddsubass  19053  grpsubsub4  19056  grppnpcan2  19057  grpnpncan  19058  mulgnndir  19126  mulgnn0dir  19127  mulgdir  19129  mulgnnass  19132  mulgnn0ass  19133  mulgass  19134  mulgsubdir  19137  pwsmulg  19142  issubg2  19164  eqgval  19199  qusgrp  19208  galcan  19325  gacan  19326  oppgmnd  19375  fvcosymgeq  19450  pmtrprfv  19474  psgnunilem3  19517  cmn32  19821  cmn12  19823  abladdsub  19833  ablsubaddsub  19835  ablsubsub23  19845  mulgdi  19847  mulgsubdi  19850  dprdss  20052  dprdz  20053  dprdf1o  20055  dprdsn  20059  dprd2da  20065  dmdprdsplit  20070  ablfac1b  20093  pgpfac1lem5  20102  prdsrngd  20203  srgdilem  20219  srgbinom  20258  ringdilem  20276  prdsringd  20346  opprrng  20371  mulgass3  20379  dvrass  20434  dvrdir  20438  subrgunit  20617  issubrg2  20619  isdomn4  20743  abvdiv  20856  lsssn0  20993  islss3  21004  prdslmodd  21014  islmhm2  21083  lspsolv  21191  islbs2  21202  islbs3  21203  lbsextlem4  21209  sralmod  21232  rnglidl1  21280  psgndiflemB  21630  ipdir  21669  ipdi  21670  ipsubdir  21672  ipsubdi  21673  ipass  21675  ipassr  21676  ipassr2  21677  isphld  21684  ocvlss  21702  sraassab  21898  psrlmod  21989  psrring  21999  psrassa  22002  mamudm  22433  matring  22481  matassa  22482  ofco2  22489  ma1repveval  22609  mdetunilem1  22650  mdetunilem9  22658  chpscmatgsumbin  22882  iinopn  22940  restopnb  23213  subbascn  23292  nrmsep2  23394  isnrm3  23397  regsep2  23414  dnsconst  23416  dfconn2  23457  1stcelcls  23499  dislly  23535  ptuni2  23614  tx1stc  23688  0nelfb  23869  infil  23901  fsubbas  23905  filssufilg  23949  hauspwpwf1  24025  cnextcn  24105  tmdcn2  24127  ustuqtoplem  24277  utopsnneiplem  24285  psmettri  24349  isxmet2d  24365  xmettri  24389  xmetres2  24399  bldisj  24436  blss2ps  24441  blss2  24442  xmstri2  24504  mstri2  24505  xmstri  24506  mstri  24507  xmstri3  24508  mstri3  24509  msrtri  24510  comet  24551  stdbdbl  24555  met2ndci  24560  ngprcan  24648  ngplcan  24649  ngpsubcan  24652  nmtri2  24665  nrgdsdi  24703  nrgdsdir  24704  nlmdsdi  24719  nlmdsdir  24720  blcvx  24836  icoopnst  24979  pi1grplem  25089  clmpm1dir  25143  cmodscmulexp  25162  cvsdiv  25172  cvsdivcl  25173  cphdivcl  25222  cphsubdir  25248  cphsubdi  25249  tcphcph  25277  bcthlem5  25368  volfiniun  25587  volcn  25646  itg1val2  25724  dvconst  25957  dvlip  26033  ftc1a  26077  ulmval  26418  ulmdvlem3  26440  ang180  26854  cvxcl  27024  scvxcvx  27025  sgmmul  27240  dchrabl  27293  gausslemma2dlem1a  27404  nosupbnd1  27753  noinfbnd1lem5  27766  noinfbnd1  27768  sltsss2  27834  addscom  28034  addbday  28086  motgrp  28687  iscgra1  28954  cgrane1  28956  cgrane3  28958  cgrahl1  28960  cgrahl2  28961  cgracgr  28962  cgratr  28967  cgrabtwn  28970  cgrahl  28971  dfcgra2  28974  sacgr  28975  f1otrge  29016  colinearalglem1  29051  axcgrtr  29060  axeuclidlem  29107  axcontlem3  29111  axcontlem4  29112  axcontlem7  29115  eengtrkg  29131  eengtrkge  29132  edglnl  29288  subgruhgredgd  29429  nbfusgrlevtxm2  29523  lfgriswlk  29831  wwlknbp1  29988  usgrwwlks2on  30102  umgrwwlks2on  30103  rusgrnumwwlks  30121  clwlkclwwlkfo  30155  3spthd  30322  3vfriswmgr  30424  frgr2wwlkeqm  30477  numclwwlk1lem2f  30501  numclwwlk2  30527  numclwwlk3  30531  numclwwlk5  30534  grpomuldivass  30688  ablomuldiv  30699  ablodivdiv4  30701  ablonnncan1  30704  nvmdi  30795  dipassr  30993  archiabllem2c  33334  dvrcan5  33375  rloccring  33411  reofld  33488  eqgvscpbl  33495  qusvsval  33497  quslmod  33503  quslmhm  33504  prmidlc  33593  ssdifidl  33603  ssmxidl  33621  ply1degltlss  33751  r1plmhm  33765  drgextlsp  33850  ccfldsrarelvec  33927  constrconj  34001  constrfin  34002  constrelextdg2  34003  pstmfval  34152  qqhval2lem  34237  qqhvq  34243  measdivcst  34480  measdivcstALTV  34481  carsggect  34574  tgoldbachgtd  34918  bnj1098  35041  bnj149  35132  bnj1118  35241  erdszelem9  35502  resconn  35549  cvmseu  35579  cvmlift2lem10  35615  cvmlift2lem12  35617  ex-sategoelel  35724  elmrsubrn  35823  mclsind  35873  r1peuqusdeg1  35946  cgrid2  36306  segconeu  36314  btwncomim  36316  btwnswapid  36320  trisegint  36331  cgrxfr  36358  brofs2  36380  endofsegid  36388  btwnconn2  36405  seglemin  36416  segletr  36417  btwnsegle  36420  colinbtwnle  36421  broutsideof2  36425  btwnoutside  36428  broutsideof3  36429  outsideoftr  36432  outsidele  36435  fvray  36444  fvline  36447  ellines  36455  nmulprop  36493  weiunpo  36778  broucube  38106  ftc1anc  38153  sdclem1  38195  sstotbnd2  38226  iscringd  38450  lsmsat  39585  lfladdcl  39648  lflnegcl  39652  lflvscl  39654  eqlkr  39676  lshpkrlem4  39690  lshpkrlem6  39692  ldualgrplem  39722  lduallmodlem  39729  latmassOLD  39806  latm12  39807  latm32  39808  latmrot  39809  latmmdiN  39811  latmmdir  39812  omlfh1N  39835  omlfh3N  39836  cvrnbtwn2  39852  cvlexchb1  39907  cvlsupr2  39920  hlatjass  39947  hlatj12  39948  hlatj32  39949  cvrat  39999  cvrat2  40006  atltcvr  40012  atexchltN  40018  cvrat3  40019  cvrat4  40020  atbtwnexOLDN  40024  atbtwnex  40025  3dimlem3  40038  3dimlem3OLDN  40039  3at  40067  2atneat  40092  llncmp  40099  2at0mat0  40102  2atmat0  40103  llncvrlpln  40135  lplncmp  40139  2llnjaN  40143  4atlem11  40186  lplncvrlvol  40193  lvolcmp  40194  2atm2atN  40362  elpaddatriN  40380  paddasslem8  40404  paddass  40415  padd12N  40416  paddssw2  40421  paddss  40422  pmod1i  40425  pmodN  40427  pmapjlln1  40432  atmod1i1  40434  atmod1i2  40436  pexmidlem2N  40548  pl42lem2N  40557  pl42lem3N  40558  pl42lem4N  40559  pl42N  40560  lhpm0atN  40606  lautlt  40668  lautcvr  40669  lautj  40670  lautm  40671  ltrneq2  40725  cdlemd1  40775  cdleme1b  40803  cdleme1  40804  cdleme2  40805  cdleme3e  40809  cdlemefr27cl  40980  cdlemefs27cl  40990  cdleme42ke  41062  cdleme42mN  41064  cdlemf2  41139  cdlemftr2  41143  trljco  41317  tgrpgrplem  41326  tendoplass  41360  tendodi1  41361  tendodi2  41362  cdlemk34  41487  cdlemk36  41490  erngdvlem3-rN  41575  tendospdi1  41597  dialss  41623  dvhvaddass  41674  dvhopvsca  41679  dvhlveclem  41685  diblss  41747  diclss  41770  diclspsn  41771  cdlemn11pre  41787  dihmeetlem12N  41895  dihmeetlem16N  41899  dihmeetlem17N  41900  dihmeetlem18N  41901  dvh4dimN  42024  lpolconN  42064  dochpolN  42067  lclkr  42110  lclkrs  42116  lcfr  42162  aks6d1c1  42686  irrapxlem6  43357  jm2.26lem3  43531  dgrsub2  43665  mpaaroot  43685  mendring  43718  mendlmod  43719  mendassa  43720  relexpmulg  44239  iunrelexpmin2  44241  relexpxpmin  44246  neicvgel1  44648  grumnud  44815  rfcnpre3  45566  fmuldfeq  46112  xlimbr  46354  stoweidlem43  46570  stoweidlem52  46579  stoweidlem53  46580  stoweidlem56  46583  stoweidlem57  46584  stoweidlem60  46587  issmfle  47272  issmfgt  47283  issmfge  47297  smflimlem4  47301  ltsubsubaddltsub  47848  iccpartigtl  47982  iccelpart  47992  prproropf1olem1  48062  fpprel2  48316  cycl3grtrilem  48521  grlimprclnbgr  48571  upgrwlkupwlk  48715  copissgrp  48743  cznrng  48836  funcringcsetcALTV2lem9  48873  funcringcsetclem9ALTV  48896  ldepsprlem  49047  lincresunit3  49056  lincreslvec3  49057  itsclc0yqe  49336  itsclc0yqsol  49339  resipos  49549  topdlat  49578  catprs  49585  endmndlem  49589  idmon  49594  idepi  49595  thincmon  50007  thincepi  50008  functhinclem1  50018  grptcmon  50167  grptcepi  50168