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  7188  isopolem  7323  fr3nr  7751  sexp3  8135  dif1en  9130  frfi  9239  intrnfi  9374  fisupcl  9428  cnfcomlem  9659  ackbij1lem15  10193  cofsmo  10229  sornom  10237  fpwwe2lem4  10594  dedekindle  11345  supmul1  12159  eluzuzle  12809  xlesubadd  13230  elioc2  13377  elico2  13378  elicc2  13379  fseq1p1m1  13566  fz0fzelfz0  13602  hash7g  14458  swrdsbslen  14636  ccatswrd  14640  swrdswrdlem  14676  wwlktovf1  14930  tanadd  16142  dvds2ln  16266  cshwsidrepsw  17071  ressress  17224  f1ovscpbl  17496  mreexexlem4d  17615  mreexexd  17616  iscatd2  17649  2oppccomf  17693  issubc3  17818  fthmon  17898  fuccocl  17936  fucidcl  17937  invfuc  17946  initoeu2lem0  17982  initoeu2lem1  17983  curf2cl  18199  yonedalem4c  18245  yonedalem3  18248  pospo  18311  latjle12  18416  latjlej1  18419  latnlej2  18425  latlem12  18432  latmlem1  18435  latledi  18443  latjass  18449  latj12  18450  latj32  18451  latj13  18452  latj31  18453  latjrot  18454  latjjdi  18457  latjjdir  18458  latdisdlem  18462  prdssgrpd  18667  prdsmndd  18704  mndissubm  18741  frmdmnd  18793  grpsubrcan  18960  grpsubadd  18967  grpaddsubass  18969  grpsubsub4  18972  grppnpcan2  18973  grpnpncan  18974  mulgnndir  19042  mulgnn0dir  19043  mulgdir  19045  mulgnnass  19048  mulgnn0ass  19049  mulgass  19050  mulgsubdir  19053  pwsmulg  19058  issubg2  19080  eqgval  19116  qusgrp  19125  galcan  19243  gacan  19244  oppgmnd  19293  fvcosymgeq  19366  pmtrprfv  19390  psgnunilem3  19433  cmn32  19737  cmn12  19739  abladdsub  19749  ablsubaddsub  19751  ablsubsub23  19761  mulgdi  19763  mulgsubdi  19766  dprdss  19968  dprdz  19969  dprdf1o  19971  dprdsn  19975  dprd2da  19981  dmdprdsplit  19986  ablfac1b  20009  pgpfac1lem5  20018  prdsrngd  20092  srgdilem  20108  srgbinom  20147  ringdilem  20165  prdsringd  20237  opprrng  20261  mulgass3  20269  dvrass  20324  dvrdir  20328  subrgunit  20506  issubrg2  20508  isdomn4  20632  abvdiv  20745  lsssn0  20861  islss3  20872  prdslmodd  20882  islmhm2  20952  lspsolv  21060  islbs2  21071  islbs3  21072  lbsextlem4  21078  sralmod  21101  rnglidl1  21149  psgndiflemB  21516  ipdir  21555  ipdi  21556  ipsubdir  21558  ipsubdi  21559  ipass  21561  ipassr  21562  ipassr2  21563  isphld  21570  ocvlss  21588  sraassab  21784  sraassaOLD  21786  psrgrpOLD  21873  psrlmod  21876  psrring  21886  psrassa  21889  mamudm  22289  matring  22337  matassa  22338  ofco2  22345  ma1repveval  22465  mdetunilem1  22506  mdetunilem9  22514  chpscmatgsumbin  22738  iinopn  22796  restopnb  23069  subbascn  23148  nrmsep2  23250  isnrm3  23253  regsep2  23270  dnsconst  23272  dfconn2  23313  1stcelcls  23355  dislly  23391  ptuni2  23470  tx1stc  23544  0nelfb  23725  infil  23757  fsubbas  23761  filssufilg  23805  hauspwpwf1  23881  cnextcn  23961  tmdcn2  23983  ustuqtoplem  24134  utopsnneiplem  24142  psmettri  24206  isxmet2d  24222  xmettri  24246  xmetres2  24256  bldisj  24293  blss2ps  24298  blss2  24299  xmstri2  24361  mstri2  24362  xmstri  24363  mstri  24364  xmstri3  24365  mstri3  24366  msrtri  24367  comet  24408  stdbdbl  24412  met2ndci  24417  ngprcan  24505  ngplcan  24506  ngpsubcan  24509  nmtri2  24522  nrgdsdi  24560  nrgdsdir  24561  nlmdsdi  24576  nlmdsdir  24577  blcvx  24693  icoopnst  24843  pi1grplem  24956  clmpm1dir  25010  cmodscmulexp  25029  cvsdiv  25039  cvsdivcl  25040  cphdivcl  25089  cphsubdir  25115  cphsubdi  25116  tcphcph  25144  bcthlem5  25235  volfiniun  25455  volcn  25514  itg1val2  25592  dvconst  25825  dvlip  25905  ftc1a  25951  ulmval  26296  ulmdvlem3  26318  ang180  26731  cvxcl  26902  scvxcvx  26903  sgmmul  27119  dchrabl  27172  gausslemma2dlem1a  27283  nosupbnd1  27633  noinfbnd1lem5  27646  noinfbnd1  27648  ssltss2  27708  addscom  27880  addsbday  27931  motgrp  28477  iscgra1  28744  cgrane1  28746  cgrane3  28748  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgratr  28757  cgrabtwn  28760  cgrahl  28761  dfcgra2  28764  sacgr  28765  f1otrge  28806  colinearalglem1  28840  axcgrtr  28849  axeuclidlem  28896  axcontlem3  28900  axcontlem4  28901  axcontlem7  28904  eengtrkg  28920  eengtrkge  28921  edglnl  29077  subgruhgredgd  29218  nbfusgrlevtxm2  29312  lfgriswlk  29623  wwlknbp1  29781  umgrwwlks2on  29894  rusgrnumwwlks  29911  clwlkclwwlkfo  29945  3spthd  30112  3vfriswmgr  30214  frgr2wwlkeqm  30267  numclwwlk1lem2f  30291  numclwwlk2  30317  numclwwlk3  30321  numclwwlk5  30324  grpomuldivass  30477  ablomuldiv  30488  ablodivdiv4  30490  ablonnncan1  30493  nvmdi  30584  dipassr  30782  archiabllem2c  33156  dvrcan5  33194  rloccring  33228  reofld  33322  eqgvscpbl  33328  qusvsval  33330  quslmod  33336  quslmhm  33337  prmidlc  33426  ssdifidl  33435  ssmxidl  33452  ply1degltlss  33569  r1plmhm  33582  drgextlsp  33596  ccfldsrarelvec  33673  constrconj  33742  constrfin  33743  constrelextdg2  33744  pstmfval  33893  qqhval2lem  33978  qqhvq  33984  measdivcst  34221  measdivcstALTV  34222  carsggect  34316  tgoldbachgtd  34660  bnj1098  34780  bnj149  34872  bnj1118  34981  erdszelem9  35193  resconn  35240  cvmseu  35270  cvmlift2lem10  35306  cvmlift2lem12  35308  ex-sategoelel  35415  elmrsubrn  35514  mclsind  35564  r1peuqusdeg1  35637  cgrid2  35998  segconeu  36006  btwncomim  36008  btwnswapid  36012  trisegint  36023  cgrxfr  36050  brofs2  36072  endofsegid  36080  btwnconn2  36097  seglemin  36108  segletr  36109  btwnsegle  36112  colinbtwnle  36113  broutsideof2  36117  btwnoutside  36120  broutsideof3  36121  outsideoftr  36124  outsidele  36127  fvray  36136  fvline  36139  ellines  36147  weiunpo  36460  broucube  37655  ftc1anc  37702  sdclem1  37744  sstotbnd2  37775  iscringd  37999  lsmsat  39008  lfladdcl  39071  lflnegcl  39075  lflvscl  39077  eqlkr  39099  lshpkrlem4  39113  lshpkrlem6  39115  ldualgrplem  39145  lduallmodlem  39152  latmassOLD  39229  latm12  39230  latm32  39231  latmrot  39232  latmmdiN  39234  latmmdir  39235  omlfh1N  39258  omlfh3N  39259  cvrnbtwn2  39275  cvlexchb1  39330  cvlsupr2  39343  hlatjass  39370  hlatj12  39371  hlatj32  39372  cvrat  39423  cvrat2  39430  atltcvr  39436  atexchltN  39442  cvrat3  39443  cvrat4  39444  atbtwnexOLDN  39448  atbtwnex  39449  3dimlem3  39462  3dimlem3OLDN  39463  3at  39491  2atneat  39516  llncmp  39523  2at0mat0  39526  2atmat0  39527  llncvrlpln  39559  lplncmp  39563  2llnjaN  39567  4atlem11  39610  lplncvrlvol  39617  lvolcmp  39618  2atm2atN  39786  elpaddatriN  39804  paddasslem8  39828  paddass  39839  padd12N  39840  paddssw2  39845  paddss  39846  pmod1i  39849  pmodN  39851  pmapjlln1  39856  atmod1i1  39858  atmod1i2  39860  pexmidlem2N  39972  pl42lem2N  39981  pl42lem3N  39982  pl42lem4N  39983  pl42N  39984  lhpm0atN  40030  lautlt  40092  lautcvr  40093  lautj  40094  lautm  40095  ltrneq2  40149  cdlemd1  40199  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3e  40233  cdlemefr27cl  40404  cdlemefs27cl  40414  cdleme42ke  40486  cdleme42mN  40488  cdlemf2  40563  cdlemftr2  40567  trljco  40741  tgrpgrplem  40750  tendoplass  40784  tendodi1  40785  tendodi2  40786  cdlemk34  40911  cdlemk36  40914  erngdvlem3-rN  40999  tendospdi1  41021  dialss  41047  dvhvaddass  41098  dvhopvsca  41103  dvhlveclem  41109  diblss  41171  diclss  41194  diclspsn  41195  cdlemn11pre  41211  dihmeetlem12N  41319  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem18N  41325  dvh4dimN  41448  lpolconN  41488  dochpolN  41491  lclkr  41534  lclkrs  41540  lcfr  41586  aks6d1c1  42111  irrapxlem6  42822  jm2.26lem3  42997  dgrsub2  43131  mpaaroot  43151  mendring  43184  mendlmod  43185  mendassa  43186  relexpmulg  43706  iunrelexpmin2  43708  relexpxpmin  43713  neicvgel1  44115  grumnud  44282  rfcnpre3  45034  fmuldfeq  45588  xlimbr  45832  stoweidlem43  46048  stoweidlem52  46057  stoweidlem53  46058  stoweidlem56  46061  stoweidlem57  46062  stoweidlem60  46065  issmfle  46750  issmfgt  46761  issmfge  46775  smflimlem4  46779  ltsubsubaddltsub  47306  iccpartigtl  47428  iccelpart  47438  prproropf1olem1  47508  fpprel2  47746  cycl3grtrilem  47949  grlimgrtrilem1  47997  upgrwlkupwlk  48132  copissgrp  48160  cznrng  48253  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  ldepsprlem  48465  lincresunit3  48474  lincreslvec3  48475  itsclc0yqe  48754  itsclc0yqsol  48757  resipos  48967  topdlat  48996  catprs  49004  endmndlem  49008  idmon  49013  idepi  49014  thincmon  49426  thincepi  49427  functhinclem1  49437  grptcmon  49586  grptcepi  49587