Theorem simpr2 1194

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

This theorem is referenced by:  simpr12  1257  simpr22  1260  simpr32  1263  simp1r2  1269  simp2r2  1275  simp3r2  1281  3anandis  1470  fpr2g  7215  isopolem  7345  fr3nr  7763  sexp3  8144  dif1en  9166  frfi  9294  intrnfi  9417  fisupcl  9470  cnfcomlem  9700  ackbij1lem15  10235  cofsmo  10270  sornom  10278  fpwwe2lem4  10635  dedekindle  11385  supmul1  12190  eluzuzle  12838  xlesubadd  13249  elioc2  13394  elico2  13395  elicc2  13396  fseq1p1m1  13582  fz0fzelfz0  13614  swrdsbslen  14621  ccatswrd  14625  swrdswrdlem  14661  wwlktovf1  14915  tanadd  16117  dvds2ln  16239  cshwsidrepsw  17034  ressress  17200  f1ovscpbl  17479  mreexexlem4d  17598  mreexexd  17599  iscatd2  17632  2oppccomf  17678  issubc3  17806  fthmon  17887  fuccocl  17927  fucidcl  17928  invfuc  17937  initoeu2lem0  17973  initoeu2lem1  17974  curf2cl  18194  yonedalem4c  18240  yonedalem3  18243  pospo  18308  latjle12  18413  latjlej1  18416  latnlej2  18422  latlem12  18429  latmlem1  18432  latledi  18440  latjass  18446  latj12  18447  latj32  18448  latj13  18449  latj31  18450  latjrot  18451  latjjdi  18454  latjjdir  18455  latdisdlem  18459  prdssgrpd  18664  prdsmndd  18698  mndissubm  18730  frmdmnd  18782  grpsubrcan  18947  grpsubadd  18954  grpaddsubass  18956  grpsubsub4  18959  grppnpcan2  18960  grpnpncan  18961  mulgnndir  19026  mulgnn0dir  19027  mulgdir  19029  mulgnnass  19032  mulgnn0ass  19033  mulgass  19034  mulgsubdir  19037  pwsmulg  19042  issubg2  19064  eqgval  19100  qusgrp  19108  galcan  19216  gacan  19217  oppgmnd  19269  fvcosymgeq  19345  pmtrprfv  19369  psgnunilem3  19412  cmn32  19716  cmn12  19718  abladdsub  19728  ablsubaddsub  19730  ablsubsub23  19740  mulgdi  19742  mulgsubdi  19745  dprdss  19947  dprdz  19948  dprdf1o  19950  dprdsn  19954  dprd2da  19960  dmdprdsplit  19965  ablfac1b  19988  pgpfac1lem5  19997  prdsrngd  20077  srgdilem  20093  srgbinom  20132  ringdilem  20150  prdsringd  20216  opprrng  20243  mulgass3  20251  dvrass  20306  dvrdir  20310  subrgunit  20488  issubrg2  20490  abvdiv  20676  lsssn0  20791  islss3  20802  prdslmodd  20812  islmhm2  20882  lspsolv  20990  islbs2  21001  islbs3  21002  lbsextlem4  21008  sralmod  21043  rnglidl1  21122  isdomn4  21207  psgndiflemB  21463  ipdir  21502  ipdi  21503  ipsubdir  21505  ipsubdi  21506  ipass  21508  ipassr  21509  ipassr2  21510  isphld  21517  ocvlss  21535  sraassab  21732  sraassaOLD  21734  psrbaglesuppOLD  21788  psrbagleclOLD  21790  psrbagconOLD  21794  psrgrpOLD  21829  psrlmod  21832  psrring  21842  psrassa  21845  mamudm  22210  matring  22265  matassa  22266  ofco2  22273  ma1repveval  22393  mdetunilem1  22434  mdetunilem9  22442  chpscmatgsumbin  22666  iinopn  22724  restopnb  22999  subbascn  23078  nrmsep2  23180  isnrm3  23183  regsep2  23200  dnsconst  23202  dfconn2  23243  1stcelcls  23285  dislly  23321  ptuni2  23400  tx1stc  23474  0nelfb  23655  infil  23687  fsubbas  23691  filssufilg  23735  hauspwpwf1  23811  cnextcn  23891  tmdcn2  23913  ustuqtoplem  24064  utopsnneiplem  24072  psmettri  24137  isxmet2d  24153  xmettri  24177  xmetres2  24187  bldisj  24224  blss2ps  24229  blss2  24230  xmstri2  24292  mstri2  24293  xmstri  24294  mstri  24295  xmstri3  24296  mstri3  24297  msrtri  24298  comet  24342  stdbdbl  24346  met2ndci  24351  ngprcan  24439  ngplcan  24440  ngpsubcan  24443  nmtri2  24456  nrgdsdi  24502  nrgdsdir  24503  nlmdsdi  24518  nlmdsdir  24519  blcvx  24634  icoopnst  24783  pi1grplem  24896  clmpm1dir  24950  cmodscmulexp  24969  cvsdiv  24979  cvsdivcl  24980  cphdivcl  25030  cphsubdir  25056  cphsubdi  25057  tcphcph  25085  bcthlem5  25176  volfiniun  25396  volcn  25455  itg1val2  25533  dvconst  25766  dvlip  25846  ftc1a  25892  ulmval  26231  ulmdvlem3  26253  ang180  26660  cvxcl  26830  scvxcvx  26831  sgmmul  27047  dchrabl  27100  gausslemma2dlem1a  27211  nosupbnd1  27560  noinfbnd1lem5  27573  noinfbnd1  27575  ssltss2  27635  addscom  27796  motgrp  28227  iscgra1  28494  cgrane1  28496  cgrane3  28498  cgrahl1  28500  cgrahl2  28501  cgracgr  28502  cgratr  28507  cgrabtwn  28510  cgrahl  28511  dfcgra2  28514  sacgr  28515  f1otrge  28556  colinearalglem1  28597  axcgrtr  28606  axeuclidlem  28653  axcontlem3  28657  axcontlem4  28658  axcontlem7  28661  eengtrkg  28677  eengtrkge  28678  edglnl  28836  subgruhgredgd  28974  nbfusgrlevtxm2  29068  lfgriswlk  29378  wwlknbp1  29531  umgrwwlks2on  29644  rusgrnumwwlks  29661  clwlkclwwlkfo  29695  3spthd  29862  3vfriswmgr  29964  frgr2wwlkeqm  30017  numclwwlk1lem2f  30041  numclwwlk2  30067  numclwwlk3  30071  numclwwlk5  30074  grpomuldivass  30227  ablomuldiv  30238  ablodivdiv4  30240  ablonnncan1  30243  nvmdi  30334  dipassr  30532  archiabllem2c  32777  dvrcan5  32821  reofld  32895  eqgvscpbl  32901  qusvsval  32903  quslmod  32909  quslmhm  32910  prmidlc  33007  ssmxidl  33030  ply1degltlss  33108  r1plmhm  33121  drgextlsp  33134  ccfldsrarelvec  33200  pstmfval  33340  qqhval2lem  33425  qqhvq  33431  measdivcst  33686  measdivcstALTV  33687  carsggect  33781  tgoldbachgtd  34138  bnj1098  34258  bnj149  34350  bnj1118  34459  erdszelem9  34654  resconn  34701  cvmseu  34731  cvmlift2lem10  34767  cvmlift2lem12  34769  ex-sategoelel  34876  elmrsubrn  34975  mclsind  35025  cgrid2  35445  segconeu  35453  btwncomim  35455  btwnswapid  35459  trisegint  35470  cgrxfr  35497  brofs2  35519  endofsegid  35527  btwnconn2  35544  seglemin  35555  segletr  35556  btwnsegle  35559  colinbtwnle  35560  broutsideof2  35564  btwnoutside  35567  broutsideof3  35568  outsideoftr  35571  outsidele  35574  fvray  35583  fvline  35586  ellines  35594  broucube  36986  ftc1anc  37033  sdclem1  37075  sstotbnd2  37106  iscringd  37330  lsmsat  38342  lfladdcl  38405  lflnegcl  38409  lflvscl  38411  eqlkr  38433  lshpkrlem4  38447  lshpkrlem6  38449  ldualgrplem  38479  lduallmodlem  38486  latmassOLD  38563  latm12  38564  latm32  38565  latmrot  38566  latmmdiN  38568  latmmdir  38569  omlfh1N  38592  omlfh3N  38593  cvrnbtwn2  38609  cvlexchb1  38664  cvlsupr2  38677  hlatjass  38704  hlatj12  38705  hlatj32  38706  cvrat  38757  cvrat2  38764  atltcvr  38770  atexchltN  38776  cvrat3  38777  cvrat4  38778  atbtwnexOLDN  38782  atbtwnex  38783  3dimlem3  38796  3dimlem3OLDN  38797  3at  38825  2atneat  38850  llncmp  38857  2at0mat0  38860  2atmat0  38861  llncvrlpln  38893  lplncmp  38897  2llnjaN  38901  4atlem11  38944  lplncvrlvol  38951  lvolcmp  38952  2atm2atN  39120  elpaddatriN  39138  paddasslem8  39162  paddass  39173  padd12N  39174  paddssw2  39179  paddss  39180  pmod1i  39183  pmodN  39185  pmapjlln1  39190  atmod1i1  39192  atmod1i2  39194  pexmidlem2N  39306  pl42lem2N  39315  pl42lem3N  39316  pl42lem4N  39317  pl42N  39318  lhpm0atN  39364  lautlt  39426  lautcvr  39427  lautj  39428  lautm  39429  ltrneq2  39483  cdlemd1  39533  cdleme1b  39561  cdleme1  39562  cdleme2  39563  cdleme3e  39567  cdlemefr27cl  39738  cdlemefs27cl  39748  cdleme42ke  39820  cdleme42mN  39822  cdlemf2  39897  cdlemftr2  39901  trljco  40075  tgrpgrplem  40084  tendoplass  40118  tendodi1  40119  tendodi2  40120  cdlemk34  40245  cdlemk36  40248  erngdvlem3-rN  40333  tendospdi1  40355  dialss  40381  dvhvaddass  40432  dvhopvsca  40437  dvhlveclem  40443  diblss  40505  diclss  40528  diclspsn  40529  cdlemn11pre  40545  dihmeetlem12N  40653  dihmeetlem16N  40657  dihmeetlem17N  40658  dihmeetlem18N  40659  dvh4dimN  40782  lpolconN  40822  dochpolN  40825  lclkr  40868  lclkrs  40874  lcfr  40920  irrapxlem6  42028  jm2.26lem3  42203  dgrsub2  42340  mpaaroot  42360  mendring  42397  mendlmod  42398  mendassa  42399  relexpmulg  42924  iunrelexpmin2  42926  relexpxpmin  42931  neicvgel1  43333  grumnud  43508  rfcnpre3  44180  fmuldfeq  44758  xlimbr  45002  stoweidlem43  45218  stoweidlem52  45227  stoweidlem53  45228  stoweidlem56  45231  stoweidlem57  45232  stoweidlem60  45235  issmfle  45920  issmfgt  45931  issmfge  45945  smflimlem4  45949  ltsubsubaddltsub  46468  iccpartigtl  46550  iccelpart  46560  prproropf1olem1  46630  fpprel2  46868  upgrwlkupwlk  46977  copissgrp  47005  cznrng  47098  funcringcsetcALTV2lem9  47135  funcringcsetclem9ALTV  47158  ldepsprlem  47315  lincresunit3  47324  lincreslvec3  47325  itsclc0yqe  47609  itsclc0yqsol  47612  topdlat  47791  catprs  47793  endmndlem  47797  idmon  47798  idepi  47799  thincmon  47816  thincepi  47817  functhinclem1  47823  grptcmon  47878  grptcepi  47879