Theorem simpr2 1212

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpr12  1275  simpr22  1278  simpr32  1281  simp1r2  1287  simp2r2  1293  simp3r2  1299  3anandis  1498  fpr2g  7209  isopolem  7343  fr3nr  7770  sexp3  8148  dif1en  9145  frfi  9244  intrnfi  9375  fisupcl  9429  cnfcomlem  9667  ackbij1lem15  10215  cofsmo  10252  sornom  10260  fpwwe2lem4  10618  dedekindle  11373  supmul1  12183  eluzuzle  12870  xlesubadd  13288  elioc2  13435  elico2  13436  elicc2  13437  fseq1p1m1  13626  fz0fzelfz0  13662  hash7g  14523  swrdsbslen  14702  ccatswrd  14706  swrdswrdlem  14741  wwlktovf1  14994  tanadd  16222  dvds2ln  16346  cshwsidrepsw  17152  ressress  17306  f1ovscpbl  17579  mreexexlem4d  17702  mreexexd  17703  iscatd2  17736  2oppccomf  17780  issubc3  17905  fthmon  17985  fuccocl  18023  fucidcl  18024  invfuc  18033  initoeu2lem0  18069  initoeu2lem1  18070  curf2cl  18286  yonedalem4c  18332  yonedalem3  18335  pospo  18398  latjle12  18505  latjlej1  18508  latnlej2  18514  latlem12  18521  latmlem1  18524  latledi  18532  latjass  18538  latj12  18539  latj32  18540  latj13  18541  latj31  18542  latjrot  18543  latjjdi  18546  latjjdir  18547  latdisdlem  18551  prdssgrpd  18790  prdsmndd  18827  mndissubm  18864  frmdmnd  18917  grpsubrcan  19086  grpsubadd  19093  grpaddsubass  19095  grpsubsub4  19098  grppnpcan2  19099  grpnpncan  19100  mulgnndir  19168  mulgnn0dir  19169  mulgdir  19171  mulgnnass  19174  mulgnn0ass  19175  mulgass  19176  mulgsubdir  19179  pwsmulg  19184  issubg2  19207  eqgval  19244  qusgrp  19256  galcan  19373  gacan  19374  oppgmnd  19423  fvcosymgeq  19498  pmtrprfv  19522  psgnunilem3  19565  cmn32  19869  cmn12  19871  abladdsub  19881  ablsubaddsub  19883  ablsubsub23  19893  mulgdi  19895  mulgsubdi  19898  dprdss  20100  dprdz  20101  dprdf1o  20103  dprdsn  20107  dprd2da  20113  dmdprdsplit  20118  ablfac1b  20141  pgpfac1lem5  20150  prdsrngd  20253  srgdilem  20273  srgbinom  20312  ringdilem  20330  prdsringd  20401  opprrng  20426  mulgass3  20434  dvrass  20489  dvrdir  20493  subrgunit  20674  issubrg2  20676  isdomn4  20799  abvdiv  20911  lsssn0  21048  islss3  21059  prdslmodd  21069  islmhm2  21138  lspsolv  21246  islbs2  21257  islbs3  21258  lbsextlem4  21264  sralmod  21287  rnglidl1  21337  prmidlc  21452  ssdifidl  21464  psgndiflemB  21729  ipdir  21768  ipdi  21769  ipsubdir  21771  ipsubdi  21772  ipass  21774  ipassr  21775  ipassr2  21776  isphld  21783  ocvlss  21801  sraassab  21997  psrlmod  22088  psrring  22098  psrassa  22101  mamudm  22531  matring  22579  matassa  22580  ofco2  22587  ma1repveval  22707  mdetunilem1  22748  mdetunilem9  22756  chpscmatgsumbin  22980  iinopn  23038  restopnb  23311  subbascn  23390  nrmsep2  23492  isnrm3  23495  regsep2  23512  dnsconst  23514  dfconn2  23555  1stcelcls  23597  dislly  23633  ptuni2  23712  tx1stc  23786  0nelfb  23967  infil  23999  fsubbas  24003  filssufilg  24047  hauspwpwf1  24123  cnextcn  24203  tmdcn2  24225  ustuqtoplem  24375  utopsnneiplem  24383  psmettri  24447  isxmet2d  24463  xmettri  24487  xmetres2  24497  bldisj  24534  blss2ps  24539  blss2  24540  xmstri2  24602  mstri2  24603  xmstri  24604  mstri  24605  xmstri3  24606  mstri3  24607  msrtri  24608  comet  24649  stdbdbl  24653  met2ndci  24658  ngprcan  24746  ngplcan  24747  ngpsubcan  24750  nmtri2  24763  nrgdsdi  24801  nrgdsdir  24802  nlmdsdi  24817  nlmdsdir  24818  blcvx  24934  icoopnst  25077  pi1grplem  25187  clmpm1dir  25241  cmodscmulexp  25260  cvsdiv  25270  cvsdivcl  25271  cphdivcl  25320  cphsubdir  25346  cphsubdi  25347  tcphcph  25375  bcthlem5  25466  volfiniun  25685  volcn  25744  itg1val2  25822  dvconst  26055  dvlip  26131  ftc1a  26175  ulmval  26519  ulmdvlem3  26541  ang180  26955  cvxcl  27125  scvxcvx  27126  sgmmul  27341  dchrabl  27394  gausslemma2dlem1a  27505  nosupbnd1  27854  noinfbnd1lem5  27867  noinfbnd1  27869  sltsss2  27935  addscom  28135  addbday  28187  motgrp  28788  iscgra1  29094  cgrane1  29096  cgrane3  29098  cgrahl1  29100  cgrahl2  29101  cgracgr  29102  cgratr  29107  cgrabtwn  29110  cgrahl  29111  dfcgra2  29114  sacgr  29115  f1otrge  29187  colinearalglem1  29222  axcgrtr  29231  axeuclidlem  29278  axcontlem3  29282  axcontlem4  29283  axcontlem7  29286  eengtrkg  29302  eengtrkge  29303  edglnl  29459  subgruhgredgd  29600  nbfusgrlevtxm2  29694  lfgriswlk  30002  wwlknbp1  30159  usgrwwlks2on  30273  umgrwwlks2on  30274  rusgrnumwwlks  30292  clwlkclwwlkfo  30326  3spthd  30493  3vfriswmgr  30595  frgr2wwlkeqm  30648  numclwwlk1lem2f  30672  numclwwlk2  30698  numclwwlk3  30702  numclwwlk5  30705  grpomuldivass  30859  ablomuldiv  30870  ablodivdiv4  30872  ablonnncan1  30875  nvmdi  30966  dipassr  31164  archiabllem2c  33481  dvrcan5  33521  rloccring  33557  reofld  33629  eqgvscpbl  33636  qusvsval  33638  quslmod  33644  quslmhm  33645  ssmxidl  33723  ply1degltlss  33852  r1plmhm  33865  drgextlsp  33950  ccfldsrarelvec  34027  constrconj  34101  constrfin  34102  constrelextdg2  34103  pstmfval  34252  qqhval2lem  34337  qqhvq  34343  measdivcst  34580  measdivcstALTV  34581  carsggect  34674  tgoldbachgtd  35015  bnj1098  35138  bnj149  35229  bnj1118  35338  erdszelem9  35657  resconn  35704  cvmseu  35734  cvmlift2lem10  35770  cvmlift2lem12  35772  ex-sategoelel  35879  elmrsubrn  35978  mclsind  36028  r1peuqusdeg1  36101  cgrid2  36461  segconeu  36469  btwncomim  36471  btwnswapid  36475  trisegint  36486  cgrxfr  36513  brofs2  36535  endofsegid  36543  btwnconn2  36560  seglemin  36571  segletr  36572  btwnsegle  36575  colinbtwnle  36576  broutsideof2  36580  btwnoutside  36583  broutsideof3  36584  outsideoftr  36587  outsidele  36590  fvray  36599  fvline  36602  ellines  36610  nmulprop  36648  weiunpo  36942  broucube  38271  ftc1anc  38318  sdclem1  38360  sstotbnd2  38391  iscringd  38615  lsmsat  39750  lfladdcl  39813  lflnegcl  39817  lflvscl  39819  eqlkr  39841  lshpkrlem4  39855  lshpkrlem6  39857  ldualgrplem  39887  lduallmodlem  39894  latmassOLD  39971  latm12  39972  latm32  39973  latmrot  39974  latmmdiN  39976  latmmdir  39977  omlfh1N  40000  omlfh3N  40001  cvrnbtwn2  40017  cvlexchb1  40072  cvlsupr2  40085  hlatjass  40112  hlatj12  40113  hlatj32  40114  cvrat  40164  cvrat2  40171  atltcvr  40177  atexchltN  40183  cvrat3  40184  cvrat4  40185  atbtwnexOLDN  40189  atbtwnex  40190  3dimlem3  40203  3dimlem3OLDN  40204  3at  40232  2atneat  40257  llncmp  40264  2at0mat0  40267  2atmat0  40268  llncvrlpln  40300  lplncmp  40304  2llnjaN  40308  4atlem11  40351  lplncvrlvol  40358  lvolcmp  40359  2atm2atN  40527  elpaddatriN  40545  paddasslem8  40569  paddass  40580  padd12N  40581  paddssw2  40586  paddss  40587  pmod1i  40590  pmodN  40592  pmapjlln1  40597  atmod1i1  40599  atmod1i2  40601  pexmidlem2N  40713  pl42lem2N  40722  pl42lem3N  40723  pl42lem4N  40724  pl42N  40725  lhpm0atN  40771  lautlt  40833  lautcvr  40834  lautj  40835  lautm  40836  ltrneq2  40890  cdlemd1  40940  cdleme1b  40968  cdleme1  40969  cdleme2  40970  cdleme3e  40974  cdlemefr27cl  41145  cdlemefs27cl  41155  cdleme42ke  41227  cdleme42mN  41229  cdlemf2  41304  cdlemftr2  41308  trljco  41482  tgrpgrplem  41491  tendoplass  41525  tendodi1  41526  tendodi2  41527  cdlemk34  41652  cdlemk36  41655  erngdvlem3-rN  41740  tendospdi1  41762  dialss  41788  dvhvaddass  41839  dvhopvsca  41844  dvhlveclem  41850  diblss  41912  diclss  41935  diclspsn  41936  cdlemn11pre  41952  dihmeetlem12N  42060  dihmeetlem16N  42064  dihmeetlem17N  42065  dihmeetlem18N  42066  dvh4dimN  42189  lpolconN  42229  dochpolN  42232  lclkr  42275  lclkrs  42281  lcfr  42327  aks6d1c1  42851  irrapxlem6  43524  jm2.26lem3  43698  dgrsub2  43832  mpaaroot  43852  mendring  43885  mendlmod  43886  mendassa  43887  relexpmulg  44406  iunrelexpmin2  44408  relexpxpmin  44413  neicvgel1  44815  grumnud  44966  rfcnpre3  45723  fmuldfeq  46269  xlimbr  46511  stoweidlem43  46727  stoweidlem52  46736  stoweidlem53  46737  stoweidlem56  46740  stoweidlem57  46741  stoweidlem60  46744  issmfle  47429  issmfgt  47440  issmfge  47454  smflimlem4  47458  ltsubsubaddltsub  48005  iccpartigtl  48139  iccelpart  48149  prproropf1olem1  48219  fpprel2  48473  cycl3grtrilem  48678  grlimprclnbgr  48728  upgrwlkupwlk  48872  copissgrp  48900  cznrng  48993  funcringcsetcALTV2lem9  49030  funcringcsetclem9ALTV  49053  idomcanl  49079  ldepsprlem  49219  lincresunit3  49228  lincreslvec3  49229  itsclc0yqe  49508  itsclc0yqsol  49511  resipos  49720  topdlat  49749  catprs  49756  endmndlem  49760  idmon  49765  idepi  49766  thincmon  50178  thincepi  50179  functhinclem1  50189  grptcmon  50338  grptcepi  50339