Theorem simpr2 1195

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 1189	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  1258  simpr22  1261  simpr32  1264  simp1r2  1270  simp2r2  1276  simp3r2  1282  3anandis  1471  fpr2g  7248  isopolem  7381  fr3nr  7807  sexp3  8194  dif1en  9226  frfi  9349  intrnfi  9485  fisupcl  9538  cnfcomlem  9768  ackbij1lem15  10302  cofsmo  10338  sornom  10346  fpwwe2lem4  10703  dedekindle  11454  supmul1  12264  eluzuzle  12912  xlesubadd  13325  elioc2  13470  elico2  13471  elicc2  13472  fseq1p1m1  13658  fz0fzelfz0  13691  hash7g  14535  swrdsbslen  14712  ccatswrd  14716  swrdswrdlem  14752  wwlktovf1  15006  tanadd  16215  dvds2ln  16337  cshwsidrepsw  17141  ressress  17307  f1ovscpbl  17586  mreexexlem4d  17705  mreexexd  17706  iscatd2  17739  2oppccomf  17785  issubc3  17913  fthmon  17994  fuccocl  18034  fucidcl  18035  invfuc  18044  initoeu2lem0  18080  initoeu2lem1  18081  curf2cl  18301  yonedalem4c  18347  yonedalem3  18350  pospo  18415  latjle12  18520  latjlej1  18523  latnlej2  18529  latlem12  18536  latmlem1  18539  latledi  18547  latjass  18553  latj12  18554  latj32  18555  latj13  18556  latj31  18557  latjrot  18558  latjjdi  18561  latjjdir  18562  latdisdlem  18566  prdssgrpd  18771  prdsmndd  18805  mndissubm  18842  frmdmnd  18894  grpsubrcan  19061  grpsubadd  19068  grpaddsubass  19070  grpsubsub4  19073  grppnpcan2  19074  grpnpncan  19075  mulgnndir  19143  mulgnn0dir  19144  mulgdir  19146  mulgnnass  19149  mulgnn0ass  19150  mulgass  19151  mulgsubdir  19154  pwsmulg  19159  issubg2  19181  eqgval  19217  qusgrp  19226  galcan  19344  gacan  19345  oppgmnd  19397  fvcosymgeq  19471  pmtrprfv  19495  psgnunilem3  19538  cmn32  19842  cmn12  19844  abladdsub  19854  ablsubaddsub  19856  ablsubsub23  19866  mulgdi  19868  mulgsubdi  19871  dprdss  20073  dprdz  20074  dprdf1o  20076  dprdsn  20080  dprd2da  20086  dmdprdsplit  20091  ablfac1b  20114  pgpfac1lem5  20123  prdsrngd  20203  srgdilem  20219  srgbinom  20258  ringdilem  20276  prdsringd  20344  opprrng  20371  mulgass3  20379  dvrass  20434  dvrdir  20438  subrgunit  20618  issubrg2  20620  isdomn4  20738  abvdiv  20852  lsssn0  20969  islss3  20980  prdslmodd  20990  islmhm2  21060  lspsolv  21168  islbs2  21179  islbs3  21180  lbsextlem4  21186  sralmod  21217  rnglidl1  21265  psgndiflemB  21641  ipdir  21680  ipdi  21681  ipsubdir  21683  ipsubdi  21684  ipass  21686  ipassr  21687  ipassr2  21688  isphld  21695  ocvlss  21713  sraassab  21911  sraassaOLD  21913  psrgrpOLD  22000  psrlmod  22003  psrring  22013  psrassa  22016  mamudm  22420  matring  22470  matassa  22471  ofco2  22478  ma1repveval  22598  mdetunilem1  22639  mdetunilem9  22647  chpscmatgsumbin  22871  iinopn  22929  restopnb  23204  subbascn  23283  nrmsep2  23385  isnrm3  23388  regsep2  23405  dnsconst  23407  dfconn2  23448  1stcelcls  23490  dislly  23526  ptuni2  23605  tx1stc  23679  0nelfb  23860  infil  23892  fsubbas  23896  filssufilg  23940  hauspwpwf1  24016  cnextcn  24096  tmdcn2  24118  ustuqtoplem  24269  utopsnneiplem  24277  psmettri  24342  isxmet2d  24358  xmettri  24382  xmetres2  24392  bldisj  24429  blss2ps  24434  blss2  24435  xmstri2  24497  mstri2  24498  xmstri  24499  mstri  24500  xmstri3  24501  mstri3  24502  msrtri  24503  comet  24547  stdbdbl  24551  met2ndci  24556  ngprcan  24644  ngplcan  24645  ngpsubcan  24648  nmtri2  24661  nrgdsdi  24707  nrgdsdir  24708  nlmdsdi  24723  nlmdsdir  24724  blcvx  24839  icoopnst  24988  pi1grplem  25101  clmpm1dir  25155  cmodscmulexp  25174  cvsdiv  25184  cvsdivcl  25185  cphdivcl  25235  cphsubdir  25261  cphsubdi  25262  tcphcph  25290  bcthlem5  25381  volfiniun  25601  volcn  25660  itg1val2  25738  dvconst  25972  dvlip  26052  ftc1a  26098  ulmval  26441  ulmdvlem3  26463  ang180  26875  cvxcl  27046  scvxcvx  27047  sgmmul  27263  dchrabl  27316  gausslemma2dlem1a  27427  nosupbnd1  27777  noinfbnd1lem5  27790  noinfbnd1  27792  ssltss2  27852  addscom  28017  addsbday  28068  motgrp  28569  iscgra1  28836  cgrane1  28838  cgrane3  28840  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgratr  28849  cgrabtwn  28852  cgrahl  28853  dfcgra2  28856  sacgr  28857  f1otrge  28898  colinearalglem1  28939  axcgrtr  28948  axeuclidlem  28995  axcontlem3  28999  axcontlem4  29000  axcontlem7  29003  eengtrkg  29019  eengtrkge  29020  edglnl  29178  subgruhgredgd  29319  nbfusgrlevtxm2  29413  lfgriswlk  29724  wwlknbp1  29877  umgrwwlks2on  29990  rusgrnumwwlks  30007  clwlkclwwlkfo  30041  3spthd  30208  3vfriswmgr  30310  frgr2wwlkeqm  30363  numclwwlk1lem2f  30387  numclwwlk2  30413  numclwwlk3  30417  numclwwlk5  30420  grpomuldivass  30573  ablomuldiv  30584  ablodivdiv4  30586  ablonnncan1  30589  nvmdi  30680  dipassr  30878  archiabllem2c  33175  dvrcan5  33216  rloccring  33242  reofld  33337  eqgvscpbl  33343  qusvsval  33345  quslmod  33351  quslmhm  33352  prmidlc  33441  ssdifidl  33450  ssmxidl  33467  ply1degltlss  33582  r1plmhm  33595  drgextlsp  33608  ccfldsrarelvec  33681  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33842  qqhval2lem  33927  qqhvq  33933  measdivcst  34188  measdivcstALTV  34189  carsggect  34283  tgoldbachgtd  34639  bnj1098  34759  bnj149  34851  bnj1118  34960  erdszelem9  35167  resconn  35214  cvmseu  35244  cvmlift2lem10  35280  cvmlift2lem12  35282  ex-sategoelel  35389  elmrsubrn  35488  mclsind  35538  r1peuqusdeg1  35611  cgrid2  35967  segconeu  35975  btwncomim  35977  btwnswapid  35981  trisegint  35992  cgrxfr  36019  brofs2  36041  endofsegid  36049  btwnconn2  36066  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  broutsideof2  36086  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsidele  36096  fvray  36105  fvline  36108  ellines  36116  weiunpo  36431  broucube  37614  ftc1anc  37661  sdclem1  37703  sstotbnd2  37734  iscringd  37958  lsmsat  38964  lfladdcl  39027  lflnegcl  39031  lflvscl  39033  eqlkr  39055  lshpkrlem4  39069  lshpkrlem6  39071  ldualgrplem  39101  lduallmodlem  39108  latmassOLD  39185  latm12  39186  latm32  39187  latmrot  39188  latmmdiN  39190  latmmdir  39191  omlfh1N  39214  omlfh3N  39215  cvrnbtwn2  39231  cvlexchb1  39286  cvlsupr2  39299  hlatjass  39326  hlatj12  39327  hlatj32  39328  cvrat  39379  cvrat2  39386  atltcvr  39392  atexchltN  39398  cvrat3  39399  cvrat4  39400  atbtwnexOLDN  39404  atbtwnex  39405  3dimlem3  39418  3dimlem3OLDN  39419  3at  39447  2atneat  39472  llncmp  39479  2at0mat0  39482  2atmat0  39483  llncvrlpln  39515  lplncmp  39519  2llnjaN  39523  4atlem11  39566  lplncvrlvol  39573  lvolcmp  39574  2atm2atN  39742  elpaddatriN  39760  paddasslem8  39784  paddass  39795  padd12N  39796  paddssw2  39801  paddss  39802  pmod1i  39805  pmodN  39807  pmapjlln1  39812  atmod1i1  39814  atmod1i2  39816  pexmidlem2N  39928  pl42lem2N  39937  pl42lem3N  39938  pl42lem4N  39939  pl42N  39940  lhpm0atN  39986  lautlt  40048  lautcvr  40049  lautj  40050  lautm  40051  ltrneq2  40105  cdlemd1  40155  cdleme1b  40183  cdleme1  40184  cdleme2  40185  cdleme3e  40189  cdlemefr27cl  40360  cdlemefs27cl  40370  cdleme42ke  40442  cdleme42mN  40444  cdlemf2  40519  cdlemftr2  40523  trljco  40697  tgrpgrplem  40706  tendoplass  40740  tendodi1  40741  tendodi2  40742  cdlemk34  40867  cdlemk36  40870  erngdvlem3-rN  40955  tendospdi1  40977  dialss  41003  dvhvaddass  41054  dvhopvsca  41059  dvhlveclem  41065  diblss  41127  diclss  41150  diclspsn  41151  cdlemn11pre  41167  dihmeetlem12N  41275  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem18N  41281  dvh4dimN  41404  lpolconN  41444  dochpolN  41447  lclkr  41490  lclkrs  41496  lcfr  41542  aks6d1c1  42073  irrapxlem6  42783  jm2.26lem3  42958  dgrsub2  43092  mpaaroot  43112  mendring  43149  mendlmod  43150  mendassa  43151  relexpmulg  43672  iunrelexpmin2  43674  relexpxpmin  43679  neicvgel1  44081  grumnud  44255  rfcnpre3  44933  fmuldfeq  45504  xlimbr  45748  stoweidlem43  45964  stoweidlem52  45973  stoweidlem53  45974  stoweidlem56  45977  stoweidlem57  45978  stoweidlem60  45981  issmfle  46666  issmfgt  46677  issmfge  46691  smflimlem4  46695  ltsubsubaddltsub  47216  iccpartigtl  47297  iccelpart  47307  prproropf1olem1  47377  fpprel2  47615  grlimgrtrilem1  47818  upgrwlkupwlk  47863  copissgrp  47891  cznrng  47984  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  ldepsprlem  48201  lincresunit3  48210  lincreslvec3  48211  itsclc0yqe  48495  itsclc0yqsol  48498  topdlat  48676  catprs  48678  endmndlem  48682  idmon  48683  idepi  48684  thincmon  48701  thincepi  48702  functhinclem1  48708  grptcmon  48763  grptcepi  48764