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 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  1258  simpr22  1261  simpr32  1264  simp1r2  1270  simp2r2  1276  simp3r2  1282  3anandis  1472  fpr2g  7214  isopolem  7348  fr3nr  7775  sexp3  8161  dif1en  9183  frfi  9304  intrnfi  9439  fisupcl  9492  cnfcomlem  9722  ackbij1lem15  10256  cofsmo  10292  sornom  10300  fpwwe2lem4  10657  dedekindle  11408  supmul1  12220  eluzuzle  12870  xlesubadd  13288  elioc2  13433  elico2  13434  elicc2  13435  fseq1p1m1  13621  fz0fzelfz0  13657  hash7g  14508  swrdsbslen  14685  ccatswrd  14689  swrdswrdlem  14725  wwlktovf1  14979  tanadd  16186  dvds2ln  16309  cshwsidrepsw  17114  ressress  17274  f1ovscpbl  17547  mreexexlem4d  17666  mreexexd  17667  iscatd2  17700  2oppccomf  17744  issubc3  17870  fthmon  17950  fuccocl  17988  fucidcl  17989  invfuc  17998  initoeu2lem0  18034  initoeu2lem1  18035  curf2cl  18251  yonedalem4c  18297  yonedalem3  18300  pospo  18364  latjle12  18469  latjlej1  18472  latnlej2  18478  latlem12  18485  latmlem1  18488  latledi  18496  latjass  18502  latj12  18503  latj32  18504  latj13  18505  latj31  18506  latjrot  18507  latjjdi  18510  latjjdir  18511  latdisdlem  18515  prdssgrpd  18720  prdsmndd  18757  mndissubm  18794  frmdmnd  18846  grpsubrcan  19013  grpsubadd  19020  grpaddsubass  19022  grpsubsub4  19025  grppnpcan2  19026  grpnpncan  19027  mulgnndir  19095  mulgnn0dir  19096  mulgdir  19098  mulgnnass  19101  mulgnn0ass  19102  mulgass  19103  mulgsubdir  19106  pwsmulg  19111  issubg2  19133  eqgval  19169  qusgrp  19178  galcan  19296  gacan  19297  oppgmnd  19346  fvcosymgeq  19420  pmtrprfv  19444  psgnunilem3  19487  cmn32  19791  cmn12  19793  abladdsub  19803  ablsubaddsub  19805  ablsubsub23  19815  mulgdi  19817  mulgsubdi  19820  dprdss  20022  dprdz  20023  dprdf1o  20025  dprdsn  20029  dprd2da  20035  dmdprdsplit  20040  ablfac1b  20063  pgpfac1lem5  20072  prdsrngd  20146  srgdilem  20162  srgbinom  20201  ringdilem  20219  prdsringd  20291  opprrng  20318  mulgass3  20326  dvrass  20381  dvrdir  20385  subrgunit  20563  issubrg2  20565  isdomn4  20689  abvdiv  20803  lsssn0  20919  islss3  20930  prdslmodd  20940  islmhm2  21010  lspsolv  21118  islbs2  21129  islbs3  21130  lbsextlem4  21136  sralmod  21161  rnglidl1  21209  psgndiflemB  21585  ipdir  21624  ipdi  21625  ipsubdir  21627  ipsubdi  21628  ipass  21630  ipassr  21631  ipassr2  21632  isphld  21639  ocvlss  21657  sraassab  21855  sraassaOLD  21857  psrgrpOLD  21944  psrlmod  21947  psrring  21957  psrassa  21960  mamudm  22366  matring  22416  matassa  22417  ofco2  22424  ma1repveval  22544  mdetunilem1  22585  mdetunilem9  22593  chpscmatgsumbin  22817  iinopn  22875  restopnb  23148  subbascn  23227  nrmsep2  23329  isnrm3  23332  regsep2  23349  dnsconst  23351  dfconn2  23392  1stcelcls  23434  dislly  23470  ptuni2  23549  tx1stc  23623  0nelfb  23804  infil  23836  fsubbas  23840  filssufilg  23884  hauspwpwf1  23960  cnextcn  24040  tmdcn2  24062  ustuqtoplem  24213  utopsnneiplem  24221  psmettri  24285  isxmet2d  24301  xmettri  24325  xmetres2  24335  bldisj  24372  blss2ps  24377  blss2  24378  xmstri2  24440  mstri2  24441  xmstri  24442  mstri  24443  xmstri3  24444  mstri3  24445  msrtri  24446  comet  24489  stdbdbl  24493  met2ndci  24498  ngprcan  24586  ngplcan  24587  ngpsubcan  24590  nmtri2  24603  nrgdsdi  24641  nrgdsdir  24642  nlmdsdi  24657  nlmdsdir  24658  blcvx  24774  icoopnst  24924  pi1grplem  25037  clmpm1dir  25091  cmodscmulexp  25110  cvsdiv  25120  cvsdivcl  25121  cphdivcl  25171  cphsubdir  25197  cphsubdi  25198  tcphcph  25226  bcthlem5  25317  volfiniun  25537  volcn  25596  itg1val2  25674  dvconst  25907  dvlip  25987  ftc1a  26033  ulmval  26378  ulmdvlem3  26400  ang180  26812  cvxcl  26983  scvxcvx  26984  sgmmul  27200  dchrabl  27253  gausslemma2dlem1a  27364  nosupbnd1  27714  noinfbnd1lem5  27727  noinfbnd1  27729  ssltss2  27789  addscom  27954  addsbday  28005  motgrp  28506  iscgra1  28773  cgrane1  28775  cgrane3  28777  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgratr  28786  cgrabtwn  28789  cgrahl  28790  dfcgra2  28793  sacgr  28794  f1otrge  28835  colinearalglem1  28870  axcgrtr  28879  axeuclidlem  28926  axcontlem3  28930  axcontlem4  28931  axcontlem7  28934  eengtrkg  28950  eengtrkge  28951  edglnl  29107  subgruhgredgd  29248  nbfusgrlevtxm2  29342  lfgriswlk  29653  wwlknbp1  29811  umgrwwlks2on  29924  rusgrnumwwlks  29941  clwlkclwwlkfo  29975  3spthd  30142  3vfriswmgr  30244  frgr2wwlkeqm  30297  numclwwlk1lem2f  30321  numclwwlk2  30347  numclwwlk3  30351  numclwwlk5  30354  grpomuldivass  30507  ablomuldiv  30518  ablodivdiv4  30520  ablonnncan1  30523  nvmdi  30614  dipassr  30812  archiabllem2c  33148  dvrcan5  33186  rloccring  33220  reofld  33313  eqgvscpbl  33319  qusvsval  33321  quslmod  33327  quslmhm  33328  prmidlc  33417  ssdifidl  33426  ssmxidl  33443  ply1degltlss  33558  r1plmhm  33571  drgextlsp  33585  ccfldsrarelvec  33662  constrconj  33727  constrfin  33728  constrelextdg2  33729  pstmfval  33836  qqhval2lem  33923  qqhvq  33929  measdivcst  34166  measdivcstALTV  34167  carsggect  34261  tgoldbachgtd  34618  bnj1098  34738  bnj149  34830  bnj1118  34939  erdszelem9  35145  resconn  35192  cvmseu  35222  cvmlift2lem10  35258  cvmlift2lem12  35260  ex-sategoelel  35367  elmrsubrn  35466  mclsind  35516  r1peuqusdeg1  35589  cgrid2  35945  segconeu  35953  btwncomim  35955  btwnswapid  35959  trisegint  35970  cgrxfr  35997  brofs2  36019  endofsegid  36027  btwnconn2  36044  seglemin  36055  segletr  36056  btwnsegle  36059  colinbtwnle  36060  broutsideof2  36064  btwnoutside  36067  broutsideof3  36068  outsideoftr  36071  outsidele  36074  fvray  36083  fvline  36086  ellines  36094  weiunpo  36407  broucube  37602  ftc1anc  37649  sdclem1  37691  sstotbnd2  37722  iscringd  37946  lsmsat  38950  lfladdcl  39013  lflnegcl  39017  lflvscl  39019  eqlkr  39041  lshpkrlem4  39055  lshpkrlem6  39057  ldualgrplem  39087  lduallmodlem  39094  latmassOLD  39171  latm12  39172  latm32  39173  latmrot  39174  latmmdiN  39176  latmmdir  39177  omlfh1N  39200  omlfh3N  39201  cvrnbtwn2  39217  cvlexchb1  39272  cvlsupr2  39285  hlatjass  39312  hlatj12  39313  hlatj32  39314  cvrat  39365  cvrat2  39372  atltcvr  39378  atexchltN  39384  cvrat3  39385  cvrat4  39386  atbtwnexOLDN  39390  atbtwnex  39391  3dimlem3  39404  3dimlem3OLDN  39405  3at  39433  2atneat  39458  llncmp  39465  2at0mat0  39468  2atmat0  39469  llncvrlpln  39501  lplncmp  39505  2llnjaN  39509  4atlem11  39552  lplncvrlvol  39559  lvolcmp  39560  2atm2atN  39728  elpaddatriN  39746  paddasslem8  39770  paddass  39781  padd12N  39782  paddssw2  39787  paddss  39788  pmod1i  39791  pmodN  39793  pmapjlln1  39798  atmod1i1  39800  atmod1i2  39802  pexmidlem2N  39914  pl42lem2N  39923  pl42lem3N  39924  pl42lem4N  39925  pl42N  39926  lhpm0atN  39972  lautlt  40034  lautcvr  40035  lautj  40036  lautm  40037  ltrneq2  40091  cdlemd1  40141  cdleme1b  40169  cdleme1  40170  cdleme2  40171  cdleme3e  40175  cdlemefr27cl  40346  cdlemefs27cl  40356  cdleme42ke  40428  cdleme42mN  40430  cdlemf2  40505  cdlemftr2  40509  trljco  40683  tgrpgrplem  40692  tendoplass  40726  tendodi1  40727  tendodi2  40728  cdlemk34  40853  cdlemk36  40856  erngdvlem3-rN  40941  tendospdi1  40963  dialss  40989  dvhvaddass  41040  dvhopvsca  41045  dvhlveclem  41051  diblss  41113  diclss  41136  diclspsn  41137  cdlemn11pre  41153  dihmeetlem12N  41261  dihmeetlem16N  41265  dihmeetlem17N  41266  dihmeetlem18N  41267  dvh4dimN  41390  lpolconN  41430  dochpolN  41433  lclkr  41476  lclkrs  41482  lcfr  41528  aks6d1c1  42058  irrapxlem6  42783  jm2.26lem3  42958  dgrsub2  43092  mpaaroot  43112  mendring  43145  mendlmod  43146  mendassa  43147  relexpmulg  43668  iunrelexpmin2  43670  relexpxpmin  43675  neicvgel1  44077  grumnud  44250  rfcnpre3  44983  fmuldfeq  45543  xlimbr  45787  stoweidlem43  46003  stoweidlem52  46012  stoweidlem53  46013  stoweidlem56  46016  stoweidlem57  46017  stoweidlem60  46020  issmfle  46705  issmfgt  46716  issmfge  46730  smflimlem4  46734  ltsubsubaddltsub  47259  iccpartigtl  47356  iccelpart  47366  prproropf1olem1  47436  fpprel2  47674  cycl3grtrilem  47859  grlimgrtrilem1  47907  upgrwlkupwlk  48002  copissgrp  48030  cznrng  48123  funcringcsetcALTV2lem9  48160  funcringcsetclem9ALTV  48183  ldepsprlem  48335  lincresunit3  48344  lincreslvec3  48345  itsclc0yqe  48628  itsclc0yqsol  48631  resipos  48820  topdlat  48849  catprs  48856  endmndlem  48860  idmon  48864  idepi  48865  thincmon  49048  thincepi  49049  functhinclem1  49059  grptcmon  49186  grptcepi  49187