Theorem simpr2 1214

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr12  1277  simpr22  1280  simpr32  1283  simp1r2  1289  simp2r2  1295  simp3r2  1301  3anandis  1501  fpr2g  7240  isopolem  7376  fr3nr  7810  sexp3  8197  dif1en  9205  frfi  9304  intrnfi  9435  fisupcl  9489  cnfcomlem  9727  ackbij1lem15  10338  cofsmo  10374  sornom  10382  fpwwe2lem4  10746  dedekindle  11501  supmul1  12313  eluzuzle  13001  xlesubadd  13420  elioc2  13567  elico2  13568  elicc2  13569  fseq1p1m1  13759  fz0fzelfz0  13795  hash7g  14658  swrdsbslen  14842  ccatswrd  14846  swrdswrdlem  14881  wwlktovf1  15139  tanadd  16364  dvds2ln  16488  cshwsidrepsw  17300  ressress  17454  f1ovscpbl  17727  mreexexlem4d  17850  mreexexd  17851  iscatd2  17884  2oppccomf  17928  issubc3  18053  fthmon  18133  fuccocl  18171  fucidcl  18172  invfuc  18181  initoeu2lem0  18217  initoeu2lem1  18218  curf2cl  18434  yonedalem4c  18480  yonedalem3  18483  pospo  18546  latjle12  18653  latjlej1  18656  latnlej2  18662  latlem12  18669  latmlem1  18672  latledi  18680  latjass  18686  latj12  18687  latj32  18688  latj13  18689  latj31  18690  latjrot  18691  latjjdi  18694  latjjdir  18695  latdisdlem  18699  prdssgrpd  18951  prdsmndd  18993  mndissubm  19031  frmdmnd  19084  grpsubrcan  19260  grpsubadd  19267  grpaddsubass  19269  grpsubsub4  19272  grppnpcan2  19273  grpnpncan  19274  mulgnndir  19342  mulgnn0dir  19343  mulgdir  19345  mulgnnass  19348  mulgnn0ass  19349  mulgass  19350  mulgsubdir  19353  pwsmulg  19358  issubg2  19381  eqgval  19418  qusgrp  19430  galcan  19548  gacan  19549  oppgmnd  19598  fvcosymgeq  19673  pmtrprfv  19697  psgnunilem3  19740  cmn32  20044  cmn12  20046  abladdsub  20056  ablsubaddsub  20058  ablsubsub23  20068  mulgdi  20070  mulgsubdi  20073  dprdss  20275  dprdz  20276  dprdf1o  20278  dprdsn  20282  dprd2da  20288  dmdprdsplit  20293  ablfac1b  20316  pgpfac1lem5  20325  prdsrngd  20428  srgdilem  20448  srgbinom  20487  ringdilem  20506  prdsringd  20580  opprrng  20605  mulgass3  20613  dvrass  20668  dvrdir  20672  subrgunit  20872  issubrg2  20874  isdomn4  20997  abvdiv  21116  lsssn0  21253  islss3  21264  prdslmodd  21274  islmhm2  21343  lspsolv  21451  islbs2  21462  islbs3  21463  lbsextlem4  21469  sralmod  21492  rnglidl1  21542  prmidlc  21659  ssdifidl  21671  psgndiflemB  21936  ipdir  21975  ipdi  21976  ipsubdir  21978  ipsubdi  21979  ipass  21981  ipassr  21982  ipassr2  21983  isphld  21990  ocvlss  22008  sraassab  22206  psrlmod  22297  psrring  22307  psrassa  22310  mamudm  22740  matring  22788  matassa  22789  ofco2  22796  ma1repveval  22916  mdetunilem1  22957  mdetunilem9  22965  chpscmatgsumbin  23192  iinopn  23250  restopnb  23523  subbascn  23602  nrmsep2  23704  isnrm3  23707  regsep2  23724  dnsconst  23726  dfconn2  23767  1stcelcls  23810  dislly  23846  ptuni2  23925  tx1stc  23999  0nelfb  24180  infil  24212  fsubbas  24216  filssufilg  24260  hauspwpwf1  24336  cnextcn  24416  tmdcn2  24438  ustuqtoplem  24588  utopsnneiplem  24596  psmettri  24660  isxmet2d  24676  xmettri  24700  xmetres2  24710  bldisj  24747  blss2ps  24752  blss2  24753  xmstri2  24815  mstri2  24816  xmstri  24817  mstri  24818  xmstri3  24819  mstri3  24820  msrtri  24821  comet  24862  stdbdbl  24866  met2ndci  24871  ngprcan  24959  ngplcan  24960  ngpsubcan  24963  nmtri2  24976  nrgdsdi  25014  nrgdsdir  25015  nlmdsdi  25030  nlmdsdir  25031  blcvx  25147  icoopnst  25290  pi1grplem  25400  clmpm1dir  25454  cmodscmulexp  25473  cvsdiv  25483  cvsdivcl  25484  cphdivcl  25533  cphsubdir  25559  cphsubdi  25560  tcphcph  25588  bcthlem5  25679  volfiniun  25898  volcn  25957  itg1val2  26035  dvconst  26267  dvlip  26343  ftc1a  26387  ulmval  26737  ulmdvlem3  26759  ang180  27172  cvxcl  27342  scvxcvx  27343  sgmmul  27558  dchrabl  27611  gausslemma2dlem1a  27722  nosupbnd1  28101  noinfbnd1lem5  28114  noinfbnd1  28116  sltsss2  28182  addscom  28382  addbday  28434  motgrp  29036  iscgra1  29347  cgrane1  29349  cgrane3  29351  cgrahl1  29353  cgrahl2  29354  cgracgr  29355  cgratr  29360  cgrabtwn  29364  cgrahl  29365  dfcgra2  29368  sacgr  29369  angmgmaddcl  29421  f1otrge  29479  colinearalglem1  29514  axcgrtr  29523  axeuclidlem  29570  axcontlem3  29574  axcontlem4  29575  axcontlem7  29578  eengtrkg  29594  eengtrkge  29595  edglnl  29751  subgruhgredgd  29895  nbfusgrlevtxm2  29989  lfgriswlk  30301  wwlknbp1  30463  usgrwwlks2on  30577  umgrwwlks2on  30578  rusgrnumwwlks  30596  clwlkclwwlkfo  30630  3spthd  30807  3vfriswmgr  30909  frgr2wwlkeqm  30962  numclwwlk1lem2f  30986  numclwwlk2  31012  numclwwlk3  31016  numclwwlk5  31019  grpomuldivass  31173  ablomuldiv  31184  ablodivdiv4  31186  ablonnncan1  31189  nvmdi  31280  dipassr  31478  archiabllem2c  33826  dvrcan5  33866  rloccring  33902  reofld  33974  eqgvscpbl  33981  qusvsval  33983  quslmod  33989  quslmhm  33990  ssmxidl  34069  ply1degltlss  34198  r1plmhm  34211  drgextlsp  34296  ccfldsrarelvec  34373  constrconj  34447  constrfin  34448  constrelextdg2  34449  pstmfval  34598  qqhval2lem  34683  qqhvq  34689  measdivcst  34927  measdivcstALTV  34928  carsggect  35020  tgoldbachgtd  35361  bnj1098  35484  bnj149  35575  bnj1118  35684  erdszelem9  36131  resconn  36178  cvmseu  36208  cvmlift2lem10  36244  cvmlift2lem12  36246  ex-sategoelel  36353  elmrsubrn  36452  mclsind  36502  r1peuqusdeg1  36575  cgrid2  36946  segconeu  36954  btwncomim  36956  btwnswapid  36960  trisegint  36971  cgrxfr  36998  brofs2  37020  endofsegid  37028  btwnconn2  37045  seglemin  37056  segletr  37057  btwnsegle  37060  colinbtwnle  37061  broutsideof2  37065  btwnoutside  37068  broutsideof3  37069  outsideoftr  37072  outsidele  37075  fvray  37084  fvline  37087  ellines  37095  nmulprop  37117  weiunpo  37431  broucube  38764  ftc1anc  38811  sdclem1  38869  sstotbnd2  38900  iscringd  39124  lsmsat  40257  lfladdcl  40320  lflnegcl  40324  lflvscl  40326  eqlkr  40348  lshpkrlem4  40362  lshpkrlem6  40364  ldualgrplem  40394  lduallmodlem  40401  latmassOLD  40478  latm12  40479  latm32  40480  latmrot  40481  latmmdiN  40483  latmmdir  40484  omlfh1N  40507  omlfh3N  40508  cvrnbtwn2  40524  cvlexchb1  40579  cvlsupr2  40592  hlatjass  40619  hlatj12  40620  hlatj32  40621  cvrat  40671  cvrat2  40678  atltcvr  40684  atexchltN  40690  cvrat3  40691  cvrat4  40692  atbtwnexOLDN  40696  atbtwnex  40697  3dimlem3  40710  3dimlem3OLDN  40711  3at  40739  2atneat  40764  llncmp  40771  2at0mat0  40774  2atmat0  40775  llncvrlpln  40807  lplncmp  40811  2llnjaN  40815  4atlem11  40858  lplncvrlvol  40865  lvolcmp  40866  2atm2atN  41034  elpaddatriN  41052  paddasslem8  41076  paddass  41087  padd12N  41088  paddssw2  41093  paddss  41094  pmod1i  41097  pmodN  41099  pmapjlln1  41104  atmod1i1  41106  atmod1i2  41108  pexmidlem2N  41220  pl42lem2N  41229  pl42lem3N  41230  pl42lem4N  41231  pl42N  41232  lhpm0atN  41278  lautlt  41340  lautcvr  41341  lautj  41342  lautm  41343  ltrneq2  41397  cdlemd1  41447  cdleme1b  41475  cdleme1  41476  cdleme2  41477  cdleme3e  41481  cdlemefr27cl  41652  cdlemefs27cl  41662  cdleme42ke  41734  cdleme42mN  41736  cdlemf2  41811  cdlemftr2  41815  trljco  41989  tgrpgrplem  41998  tendoplass  42032  tendodi1  42033  tendodi2  42034  cdlemk34  42159  cdlemk36  42162  erngdvlem3-rN  42247  tendospdi1  42269  dialss  42295  dvhvaddass  42346  dvhopvsca  42351  dvhlveclem  42357  diblss  42419  diclss  42442  diclspsn  42443  cdlemn11pre  42459  dihmeetlem12N  42567  dihmeetlem16N  42571  dihmeetlem17N  42572  dihmeetlem18N  42573  dvh4dimN  42696  lpolconN  42736  dochpolN  42739  lclkr  42782  lclkrs  42788  lcfr  42834  aks6d1c1  43358  irrapxlem6  44027  jm2.26lem3  44201  dgrsub2  44329  mpaaroot  44349  mendring  44382  mendlmod  44383  mendassa  44384  relexpmulg  44902  iunrelexpmin2  44904  relexpxpmin  44909  neicvgel1  45311  grumnud  45462  rfcnpre3  46255  fmuldfeq  46800  xlimbr  47042  stoweidlem43  47258  stoweidlem52  47267  stoweidlem53  47268  stoweidlem56  47271  stoweidlem57  47272  stoweidlem60  47275  issmfle  47960  issmfgt  47971  issmfge  47985  smflimlem4  47989  tmachlem-franscan  48164  ltsubsubaddltsub  48576  iccpartigtl  48710  iccelpart  48720  prproropf1olem1  48790  fpprel2  49044  cycl3grtrilem  49249  grlimprclnbgr  49299  upgrwlkupwlk  49443  copissgrp  49470  cznrng  49563  funcringcsetcALTV2lem9  49600  funcringcsetclem9ALTV  49623  idomcanl  49649  ldepsprlem  49789  lincresunit3  49798  lincreslvec3  49799  itsclc0yqe  50078  itsclc0yqsol  50081  resipos  50294  topdlat  50323  catprs  50330  endmndlem  50334  idmon  50339  idepi  50340  thincmon  50773  thincepi  50774  functhinclem1  50784  grptcmon  50936  grptcepi  50937  nellindf  51250