Theorem simpr2 1193

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 1187	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpr12  1256  simpr22  1259  simpr32  1262  simp1r2  1268  simp2r2  1274  simp3r2  1280  3anandis  1469  fpr2g  7069  isopolem  7196  fr3nr  7600  frfi  8989  intrnfi  9105  fisupcl  9158  cnfcomlem  9387  ackbij1lem15  9921  cofsmo  9956  sornom  9964  fpwwe2lem4  10321  dedekindle  11069  supmul1  11874  eluzuzle  12520  xlesubadd  12926  elioc2  13071  elico2  13072  elicc2  13073  fseq1p1m1  13259  fz0fzelfz0  13291  swrdsbslen  14305  ccatswrd  14309  swrdswrdlem  14345  wwlktovf1  14600  tanadd  15804  dvds2ln  15926  cshwsidrepsw  16723  ressress  16884  f1ovscpbl  17154  mreexexlem4d  17273  mreexexd  17274  iscatd2  17307  2oppccomf  17353  issubc3  17480  fthmon  17559  fuccocl  17598  fucidcl  17599  invfuc  17608  initoeu2lem0  17644  initoeu2lem1  17645  curf2cl  17865  yonedalem4c  17911  yonedalem3  17914  pospo  17978  latjle12  18083  latjlej1  18086  latnlej2  18092  latlem12  18099  latmlem1  18102  latledi  18110  latjass  18116  latj12  18117  latj32  18118  latj13  18119  latj31  18120  latjrot  18121  latjjdi  18124  latjjdir  18125  latdisdlem  18129  prdsmndd  18333  mndissubm  18361  frmdmnd  18413  grpsubrcan  18571  grpsubadd  18578  grpaddsubass  18580  grpsubsub4  18583  grppnpcan2  18584  grpnpncan  18585  mulgnndir  18647  mulgnn0dir  18648  mulgdir  18650  mulgnnass  18653  mulgnn0ass  18654  mulgass  18655  mulgsubdir  18658  pwsmulg  18663  issubg2  18685  eqgval  18720  qusgrp  18726  galcan  18825  gacan  18826  oppgmnd  18876  fvcosymgeq  18952  pmtrprfv  18976  psgnunilem3  19019  cmn32  19320  cmn12  19322  abladdsub  19331  ablsubsub23  19341  mulgdi  19343  mulgsubdi  19346  dprdss  19547  dprdz  19548  dprdf1o  19550  dprdsn  19554  dprd2da  19560  dmdprdsplit  19565  ablfac1b  19588  pgpfac1lem5  19597  srgi  19662  srgbinom  19696  ringi  19714  prdsringd  19766  opprring  19788  mulgass3  19794  dvrass  19847  subrgunit  19957  issubrg2  19959  abvdiv  20012  lsssn0  20124  islss3  20136  prdslmodd  20146  islmhm2  20215  lspsolv  20320  islbs2  20331  islbs3  20332  lbsextlem4  20338  sralmod  20370  psgndiflemB  20717  ipdir  20756  ipdi  20757  ipsubdir  20759  ipsubdi  20760  ipass  20762  ipassr  20763  ipassr2  20764  isphld  20771  ocvlss  20789  sraassa  20984  psrbaglesuppOLD  21038  psrbagleclOLD  21040  psrbagconOLD  21044  psrgrp  21077  psrlmod  21080  psrring  21090  psrassa  21093  mamudm  21447  matring  21500  matassa  21501  ofco2  21508  ma1repveval  21628  mdetunilem1  21669  mdetunilem9  21677  chpscmatgsumbin  21901  iinopn  21959  restopnb  22234  subbascn  22313  nrmsep2  22415  isnrm3  22418  regsep2  22435  dnsconst  22437  dfconn2  22478  1stcelcls  22520  dislly  22556  ptuni2  22635  tx1stc  22709  0nelfb  22890  infil  22922  fsubbas  22926  filssufilg  22970  hauspwpwf1  23046  cnextcn  23126  tmdcn2  23148  ustuqtoplem  23299  utopsnneiplem  23307  psmettri  23372  isxmet2d  23388  xmettri  23412  xmetres2  23422  bldisj  23459  blss2ps  23464  blss2  23465  xmstri2  23527  mstri2  23528  xmstri  23529  mstri  23530  xmstri3  23531  mstri3  23532  msrtri  23533  comet  23575  stdbdbl  23579  met2ndci  23584  ngprcan  23672  ngplcan  23673  ngpsubcan  23676  nmtri2  23689  nrgdsdi  23735  nrgdsdir  23736  nlmdsdi  23751  nlmdsdir  23752  blcvx  23867  icoopnst  24008  pi1grplem  24118  clmpm1dir  24172  cmodscmulexp  24191  cvsdiv  24201  cvsdivcl  24202  cphdivcl  24251  cphsubdir  24277  cphsubdi  24278  tcphcph  24306  bcthlem5  24397  volfiniun  24616  volcn  24675  itg1val2  24753  dvconst  24986  dvlip  25062  ftc1a  25106  ulmval  25444  ulmdvlem3  25466  ang180  25869  cvxcl  26039  scvxcvx  26040  sgmmul  26254  dchrabl  26307  gausslemma2dlem1a  26418  motgrp  26808  iscgra1  27075  cgrane1  27077  cgrane3  27079  cgrahl1  27081  cgrahl2  27082  cgracgr  27083  cgratr  27088  cgrabtwn  27091  cgrahl  27092  dfcgra2  27095  sacgr  27096  f1otrge  27137  colinearalglem1  27177  axcgrtr  27186  axeuclidlem  27233  axcontlem3  27237  axcontlem4  27238  axcontlem7  27241  eengtrkg  27257  eengtrkge  27258  edglnl  27416  subgruhgredgd  27554  nbfusgrlevtxm2  27648  lfgriswlk  27958  wwlknbp1  28110  umgrwwlks2on  28223  rusgrnumwwlks  28240  clwlkclwwlkfo  28274  3spthd  28441  3vfriswmgr  28543  frgr2wwlkeqm  28596  numclwwlk1lem2f  28620  numclwwlk2  28646  numclwwlk3  28650  numclwwlk5  28653  grpomuldivass  28804  ablomuldiv  28815  ablodivdiv4  28817  ablonnncan1  28820  nvmdi  28911  dipassr  29109  archiabllem2c  31351  dvrdir  31389  dvrcan5  31392  reofld  31446  eqgvscpbl  31452  qusscaval  31454  quslmod  31456  quslmhm  31457  prmidlc  31526  ssmxidl  31544  drgextlsp  31583  ccfldsrarelvec  31643  pstmfval  31748  qqhval2lem  31831  qqhvq  31837  measdivcst  32092  measdivcstALTV  32093  carsggect  32185  tgoldbachgtd  32542  bnj1098  32663  bnj149  32755  bnj1118  32864  erdszelem9  33061  resconn  33108  cvmseu  33138  cvmlift2lem10  33174  cvmlift2lem12  33176  ex-sategoelel  33283  elmrsubrn  33382  mclsind  33432  xpord3pred  33725  sexp3  33726  nosupbnd1  33844  noinfbnd1lem5  33857  noinfbnd1  33859  ssltss2  33911  addscom  34056  cgrid2  34232  segconeu  34240  btwncomim  34242  btwnswapid  34246  trisegint  34257  cgrxfr  34284  brofs2  34306  endofsegid  34314  btwnconn2  34331  seglemin  34342  segletr  34343  btwnsegle  34346  colinbtwnle  34347  broutsideof2  34351  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  outsidele  34361  fvray  34370  fvline  34373  ellines  34381  broucube  35738  ftc1anc  35785  sdclem1  35828  sstotbnd2  35859  iscringd  36083  lsmsat  36949  lfladdcl  37012  lflnegcl  37016  lflvscl  37018  eqlkr  37040  lshpkrlem4  37054  lshpkrlem6  37056  ldualgrplem  37086  lduallmodlem  37093  latmassOLD  37170  latm12  37171  latm32  37172  latmrot  37173  latmmdiN  37175  latmmdir  37176  omlfh1N  37199  omlfh3N  37200  cvrnbtwn2  37216  cvlexchb1  37271  cvlsupr2  37284  hlatjass  37311  hlatj12  37312  hlatj32  37313  cvrat  37363  cvrat2  37370  atltcvr  37376  atexchltN  37382  cvrat3  37383  cvrat4  37384  atbtwnexOLDN  37388  atbtwnex  37389  3dimlem3  37402  3dimlem3OLDN  37403  3at  37431  2atneat  37456  llncmp  37463  2at0mat0  37466  2atmat0  37467  llncvrlpln  37499  lplncmp  37503  2llnjaN  37507  4atlem11  37550  lplncvrlvol  37557  lvolcmp  37558  2atm2atN  37726  elpaddatriN  37744  paddasslem8  37768  paddass  37779  padd12N  37780  paddssw2  37785  paddss  37786  pmod1i  37789  pmodN  37791  pmapjlln1  37796  atmod1i1  37798  atmod1i2  37800  pexmidlem2N  37912  pl42lem2N  37921  pl42lem3N  37922  pl42lem4N  37923  pl42N  37924  lhpm0atN  37970  lautlt  38032  lautcvr  38033  lautj  38034  lautm  38035  ltrneq2  38089  cdlemd1  38139  cdleme1b  38167  cdleme1  38168  cdleme2  38169  cdleme3e  38173  cdlemefr27cl  38344  cdlemefs27cl  38354  cdleme42ke  38426  cdleme42mN  38428  cdlemf2  38503  cdlemftr2  38507  trljco  38681  tgrpgrplem  38690  tendoplass  38724  tendodi1  38725  tendodi2  38726  cdlemk34  38851  cdlemk36  38854  erngdvlem3-rN  38939  tendospdi1  38961  dialss  38987  dvhvaddass  39038  dvhopvsca  39043  dvhlveclem  39049  diblss  39111  diclss  39134  diclspsn  39135  cdlemn11pre  39151  dihmeetlem12N  39259  dihmeetlem16N  39263  dihmeetlem17N  39264  dihmeetlem18N  39265  dvh4dimN  39388  lpolconN  39428  dochpolN  39431  lclkr  39474  lclkrs  39480  lcfr  39526  isdomn4  40100  irrapxlem6  40565  jm2.26lem3  40739  dgrsub2  40876  mpaaroot  40896  mendring  40933  mendlmod  40934  mendassa  40935  relexpmulg  41207  iunrelexpmin2  41209  relexpxpmin  41214  neicvgel1  41618  grumnud  41793  rfcnpre3  42465  fmuldfeq  43014  xlimbr  43258  stoweidlem43  43474  stoweidlem52  43483  stoweidlem53  43484  stoweidlem56  43487  stoweidlem57  43488  stoweidlem60  43491  issmfle  44168  issmfgt  44179  issmfge  44192  smflimlem4  44196  ltsubsubaddltsub  44681  iccpartigtl  44763  iccelpart  44773  prproropf1olem1  44843  fpprel2  45081  upgrwlkupwlk  45190  copissgrp  45250  cznrng  45401  funcringcsetcALTV2lem9  45490  funcringcsetclem9ALTV  45513  ldepsprlem  45701  lincresunit3  45710  lincreslvec3  45711  itsclc0yqe  45995  itsclc0yqsol  45998  topdlat  46178  catprs  46180  endmndlem  46184  idmon  46185  idepi  46186  thincmon  46203  thincepi  46204  functhinclem1  46210  grptcmon  46263  grptcepi  46264