Theorem simpr2 1207

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simplr2OLD  1235  simprr2OLD  1247  simpr12  1306  simpr22  1312  simpr32  1318  simp1r2  1326  simp2r2  1332  simp3r2  1338  3anandis  1544  fpr2g  6747  isopolem  6867  fr3nr  7257  frfi  8493  intrnfi  8610  fisupcl  8663  cnfcomlem  8893  ackbij1lem15  9391  cofsmo  9426  sornom  9434  fpwwe2lem5  9791  dedekindle  10540  supmul1  11346  eluzuzle  12001  xlesubadd  12405  elioc2  12548  elico2  12549  elicc2  12550  fseq1p1m1  12732  fz0fzelfz0  12764  swrdsbslen  13768  swrdspsleq  13769  ccatswrd  13776  swrdswrdlem  13813  tanadd  15299  dvds2ln  15421  cshwsidrepsw  16199  ressress  16335  f1ovscpbl  16572  mreexexlem4d  16693  mreexexd  16694  iscatd2  16727  2oppccomf  16770  issubc3  16894  fthmon  16972  fuccocl  17009  fucidcl  17010  invfuc  17019  initoeu2lem0  17048  initoeu2lem1  17049  curf2cl  17257  yonedalem4c  17303  yonedalem3  17306  pospo  17359  latjle12  17448  latjlej1  17451  latnlej2  17457  latlem12  17464  latmlem1  17467  latledi  17475  latjass  17481  latj12  17482  latj32  17483  latj13  17484  latj31  17485  latjrot  17486  latjjdi  17489  latjjdir  17490  latdisdlem  17575  prdsmndd  17709  frmdmnd  17783  grpsubrcan  17883  grpsubadd  17890  grpaddsubass  17892  grpsubsub4  17895  grppnpcan2  17896  grpnpncan  17897  mulgnndir  17955  mulgnn0dir  17956  mulgdir  17958  mulgnnass  17961  mulgnn0ass  17962  mulgass  17963  mulgsubdir  17966  pwsmulg  17971  issubg2  17993  eqgval  18027  qusgrp  18033  galcan  18120  gacan  18121  oppgmnd  18167  symggrp  18203  fvcosymgeq  18232  pmtrprfv  18256  psgnunilem3  18300  cmn32  18597  cmn12  18599  abladdsub  18606  ablsubsub23  18616  mulgdi  18618  mulgsubdi  18621  dprdss  18815  dprdz  18816  dprdf1o  18818  dprdsn  18822  dprd2da  18828  dmdprdsplit  18833  ablfac1b  18856  pgpfac1lem5  18865  srgi  18898  srgbinom  18932  ringi  18947  prdsringd  18999  opprring  19018  mulgass3  19024  dvrass  19077  subrgunit  19190  issubrg2  19192  abvdiv  19229  lsssn0  19340  islss3  19354  prdslmodd  19364  islmhm2  19433  lspsolv  19539  islbs2  19551  islbs3  19552  lbsextlem4  19558  sralmod  19584  issubassa  19721  sraassa  19722  psrbaglesupp  19765  psrbaglecl  19766  psrbagcon  19768  psrgrp  19795  psrlmod  19798  psrring  19808  psrassa  19811  psgndiflemB  20342  ipdir  20382  ipdi  20383  ipsubdir  20385  ipsubdi  20386  ipass  20388  ipassr  20389  ipassr2  20390  isphld  20397  ocvlss  20415  mamudm  20598  matring  20653  matassa  20654  ofco2  20662  ma1repveval  20782  mdetunilem1  20823  mdetunilem9  20831  chpscmatgsumbin  21056  iinopn  21114  restopnb  21387  subbascn  21466  nrmsep2  21568  isnrm3  21571  regsep2  21588  dnsconst  21590  dfconn2  21631  1stcelcls  21673  dislly  21709  ptuni2  21788  tx1stc  21862  0nelfb  22043  infil  22075  fsubbas  22079  filssufilg  22123  hauspwpwf1  22199  cnextcn  22279  tmdcn2  22301  ustuqtoplem  22451  utopsnneiplem  22459  psmettri  22524  isxmet2d  22540  xmettri  22564  xmetres2  22574  bldisj  22611  blss2ps  22616  blss2  22617  xmstri2  22679  mstri2  22680  xmstri  22681  mstri  22682  xmstri3  22683  mstri3  22684  msrtri  22685  comet  22726  stdbdbl  22730  met2ndci  22735  ngprcan  22822  ngplcan  22823  ngpsubcan  22826  nmtri2  22839  nrgdsdi  22877  nrgdsdir  22878  nlmdsdi  22893  nlmdsdir  22894  blcvx  23009  icoopnst  23146  pi1grplem  23256  clmpm1dir  23310  cmodscmulexp  23329  cvsdiv  23339  cvsdivcl  23340  cphdivcl  23389  cphsubdir  23415  cphsubdi  23416  tcphcph  23443  bcthlem5  23534  volfiniun  23751  volcn  23810  itg1val2  23888  dvconst  24117  dvlip  24193  ftc1a  24237  ulmval  24571  ulmdvlem3  24593  ang180  24992  cvxcl  25163  scvxcvx  25164  sgmmul  25378  dchrabl  25431  gausslemma2dlem1a  25542  motgrp  25894  iscgra1  26158  cgrane1  26160  cgrane3  26162  cgrahl1  26164  cgrahl2  26165  cgracgr  26166  cgratr  26171  cgrabtwn  26174  cgrahl  26175  dfcgra2  26178  sacgr  26179  sacgrOLD  26180  f1otrge  26221  colinearalglem1  26255  axcgrtr  26264  axeuclidlem  26311  axcontlem3  26315  axcontlem4  26316  axcontlem7  26319  eengtrkg  26335  eengtrkge  26336  edglnl  26492  subgruhgredgd  26631  nbfusgrlevtxm2  26726  lfgriswlk  27039  wwlknbp1  27193  umgrwwlks2on  27337  rusgrnumwwlks  27354  rusgrnumwwlksOLD  27355  clwlkclwwlkfoOLD  27393  clwlkclwwlkfo  27397  3spthd  27579  3vfriswmgr  27686  frgr2wwlkeqm  27739  numclwwlk1lem2f  27771  numclwwlk1lem2fOLD  27776  numclwwlk2  27813  numclwwlk3  27817  numclwwlk5  27820  grpomuldivass  27968  ablomuldiv  27979  ablodivdiv4  27981  ablonnncan1  27984  nvmdi  28075  dipassr  28273  archiabllem2c  30311  dvrdir  30352  dvrcan5  30355  reofld  30402  eqgvscpbl  30408  qusscaval  30410  quslmod  30412  quslmhm  30413  pstmfval  30537  qqhval2lem  30623  qqhvq  30629  measdivcstOLD  30885  measdivcst  30886  carsggect  30978  tgoldbachgtd  31342  bnj1098  31453  bnj149  31544  bnj1118  31651  erdszelem9  31780  resconn  31827  cvmseu  31857  cvmlift2lem10  31893  cvmlift2lem12  31895  elmrsubrn  32016  mclsind  32066  noprefixmo  32437  nosupbnd1  32449  ssltss2  32493  cgrid2  32699  segconeu  32707  btwncomim  32709  btwnswapid  32713  trisegint  32724  cgrxfr  32751  brofs2  32773  endofsegid  32781  btwnconn2  32798  seglemin  32809  segletr  32810  btwnsegle  32813  colinbtwnle  32814  broutsideof2  32818  btwnoutside  32821  broutsideof3  32822  outsideoftr  32825  outsidele  32828  fvray  32837  fvline  32840  ellines  32848  broucube  34069  ftc1anc  34118  sdclem1  34163  sstotbnd2  34197  iscringd  34421  lsmsat  35162  lfladdcl  35225  lflnegcl  35229  lflvscl  35231  eqlkr  35253  lshpkrlem4  35267  lshpkrlem6  35269  ldualgrplem  35299  lduallmodlem  35306  latmassOLD  35383  latm12  35384  latm32  35385  latmrot  35386  latmmdiN  35388  latmmdir  35389  omlfh1N  35412  omlfh3N  35413  cvrnbtwn2  35429  cvlexchb1  35484  cvlsupr2  35497  hlatjass  35524  hlatj12  35525  hlatj32  35526  cvrat  35576  cvrat2  35583  atltcvr  35589  atexchltN  35595  cvrat3  35596  cvrat4  35597  atbtwnexOLDN  35601  atbtwnex  35602  3dimlem3  35615  3dimlem3OLDN  35616  3at  35644  2atneat  35669  llncmp  35676  2at0mat0  35679  2atmat0  35680  llncvrlpln  35712  lplncmp  35716  2llnjaN  35720  4atlem11  35763  lplncvrlvol  35770  lvolcmp  35771  2atm2atN  35939  elpaddatriN  35957  paddasslem8  35981  paddass  35992  padd12N  35993  paddssw2  35998  paddss  35999  pmod1i  36002  pmodN  36004  pmapjlln1  36009  atmod1i1  36011  atmod1i2  36013  pexmidlem2N  36125  pl42lem2N  36134  pl42lem3N  36135  pl42lem4N  36136  pl42N  36137  lhpm0atN  36183  lautlt  36245  lautcvr  36246  lautj  36247  lautm  36248  ltrneq2  36302  cdlemd1  36352  cdleme1b  36380  cdleme1  36381  cdleme2  36382  cdleme3e  36386  cdlemefr27cl  36557  cdlemefs27cl  36567  cdleme42ke  36639  cdleme42mN  36641  cdlemf2  36716  cdlemftr2  36720  trljco  36894  tgrpgrplem  36903  tendoplass  36937  tendodi1  36938  tendodi2  36939  cdlemk34  37064  cdlemk36  37067  erngdvlem3-rN  37152  tendospdi1  37174  dialss  37200  dvhvaddass  37251  dvhopvsca  37256  dvhlveclem  37262  diblss  37324  diclss  37347  diclspsn  37348  cdlemn11pre  37364  dihmeetlem12N  37472  dihmeetlem16N  37476  dihmeetlem17N  37477  dihmeetlem18N  37478  dvh4dimN  37601  lpolconN  37641  dochpolN  37644  lclkr  37687  lclkrs  37693  lcfr  37739  irrapxlem6  38351  jm2.26lem3  38527  dgrsub2  38664  mpaaroot  38684  mendring  38721  mendlmod  38722  mendassa  38723  relexpmulg  38959  iunrelexpmin2  38961  relexpxpmin  38966  neicvgel1  39373  rfcnpre3  40125  fmuldfeq  40723  xlimbr  40967  stoweidlem43  41187  stoweidlem52  41196  stoweidlem53  41197  stoweidlem56  41200  stoweidlem57  41201  stoweidlem60  41204  issmfle  41881  issmfgt  41892  issmfge  41905  smflimlem4  41909  ltsubsubaddltsub  42343  iccpartigtl  42391  iccelpart  42401  prproropf1olem1  42442  upgrwlkupwlk  42763  copissgrp  42823  cznrng  42970  funcringcsetcALTV2lem9  43059  funcringcsetclem9ALTV  43082  ldepsprlem  43276  lincresunit3  43285  lincreslvec3  43286  itsclc0yqe  43497  itsclc0yqsol  43500