Theorem simpr2 1197

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpr12  1260  simpr22  1263  simpr32  1266  simp1r2  1272  simp2r2  1278  simp3r2  1284  3anandis  1474  fpr2g  7167  isopolem  7301  fr3nr  7727  sexp3  8105  dif1en  9098  frfi  9197  intrnfi  9331  fisupcl  9385  cnfcomlem  9620  ackbij1lem15  10155  cofsmo  10191  sornom  10199  fpwwe2lem4  10557  dedekindle  11309  supmul1  12123  eluzuzle  12772  xlesubadd  13190  elioc2  13337  elico2  13338  elicc2  13339  fseq1p1m1  13526  fz0fzelfz0  13562  hash7g  14421  swrdsbslen  14600  ccatswrd  14604  swrdswrdlem  14639  wwlktovf1  14892  tanadd  16104  dvds2ln  16228  cshwsidrepsw  17033  ressress  17186  f1ovscpbl  17459  mreexexlem4d  17582  mreexexd  17583  iscatd2  17616  2oppccomf  17660  issubc3  17785  fthmon  17865  fuccocl  17903  fucidcl  17904  invfuc  17913  initoeu2lem0  17949  initoeu2lem1  17950  curf2cl  18166  yonedalem4c  18212  yonedalem3  18215  pospo  18278  latjle12  18385  latjlej1  18388  latnlej2  18394  latlem12  18401  latmlem1  18404  latledi  18412  latjass  18418  latj12  18419  latj32  18420  latj13  18421  latj31  18422  latjrot  18423  latjjdi  18426  latjjdir  18427  latdisdlem  18431  prdssgrpd  18670  prdsmndd  18707  mndissubm  18744  frmdmnd  18796  grpsubrcan  18963  grpsubadd  18970  grpaddsubass  18972  grpsubsub4  18975  grppnpcan2  18976  grpnpncan  18977  mulgnndir  19045  mulgnn0dir  19046  mulgdir  19048  mulgnnass  19051  mulgnn0ass  19052  mulgass  19053  mulgsubdir  19056  pwsmulg  19061  issubg2  19083  eqgval  19118  qusgrp  19127  galcan  19245  gacan  19246  oppgmnd  19295  fvcosymgeq  19370  pmtrprfv  19394  psgnunilem3  19437  cmn32  19741  cmn12  19743  abladdsub  19753  ablsubaddsub  19755  ablsubsub23  19765  mulgdi  19767  mulgsubdi  19770  dprdss  19972  dprdz  19973  dprdf1o  19975  dprdsn  19979  dprd2da  19985  dmdprdsplit  19990  ablfac1b  20013  pgpfac1lem5  20022  prdsrngd  20123  srgdilem  20139  srgbinom  20178  ringdilem  20196  prdsringd  20268  opprrng  20293  mulgass3  20301  dvrass  20356  dvrdir  20360  subrgunit  20535  issubrg2  20537  isdomn4  20661  abvdiv  20774  lsssn0  20911  islss3  20922  prdslmodd  20932  islmhm2  21002  lspsolv  21110  islbs2  21121  islbs3  21122  lbsextlem4  21128  sralmod  21151  rnglidl1  21199  psgndiflemB  21567  ipdir  21606  ipdi  21607  ipsubdir  21609  ipsubdi  21610  ipass  21612  ipassr  21613  ipassr2  21614  isphld  21621  ocvlss  21639  sraassab  21835  sraassaOLD  21837  psrlmod  21927  psrring  21937  psrassa  21940  mamudm  22351  matring  22399  matassa  22400  ofco2  22407  ma1repveval  22527  mdetunilem1  22568  mdetunilem9  22576  chpscmatgsumbin  22800  iinopn  22858  restopnb  23131  subbascn  23210  nrmsep2  23312  isnrm3  23315  regsep2  23332  dnsconst  23334  dfconn2  23375  1stcelcls  23417  dislly  23453  ptuni2  23532  tx1stc  23606  0nelfb  23787  infil  23819  fsubbas  23823  filssufilg  23867  hauspwpwf1  23943  cnextcn  24023  tmdcn2  24045  ustuqtoplem  24195  utopsnneiplem  24203  psmettri  24267  isxmet2d  24283  xmettri  24307  xmetres2  24317  bldisj  24354  blss2ps  24359  blss2  24360  xmstri2  24422  mstri2  24423  xmstri  24424  mstri  24425  xmstri3  24426  mstri3  24427  msrtri  24428  comet  24469  stdbdbl  24473  met2ndci  24478  ngprcan  24566  ngplcan  24567  ngpsubcan  24570  nmtri2  24583  nrgdsdi  24621  nrgdsdir  24622  nlmdsdi  24637  nlmdsdir  24638  blcvx  24754  icoopnst  24904  pi1grplem  25017  clmpm1dir  25071  cmodscmulexp  25090  cvsdiv  25100  cvsdivcl  25101  cphdivcl  25150  cphsubdir  25176  cphsubdi  25177  tcphcph  25205  bcthlem5  25296  volfiniun  25516  volcn  25575  itg1val2  25653  dvconst  25886  dvlip  25966  ftc1a  26012  ulmval  26357  ulmdvlem3  26379  ang180  26792  cvxcl  26963  scvxcvx  26964  sgmmul  27180  dchrabl  27233  gausslemma2dlem1a  27344  nosupbnd1  27694  noinfbnd1lem5  27707  noinfbnd1  27709  sltsss2  27774  addscom  27974  addbday  28026  motgrp  28627  iscgra1  28894  cgrane1  28896  cgrane3  28898  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgratr  28907  cgrabtwn  28910  cgrahl  28911  dfcgra2  28914  sacgr  28915  f1otrge  28956  colinearalglem1  28991  axcgrtr  29000  axeuclidlem  29047  axcontlem3  29051  axcontlem4  29052  axcontlem7  29055  eengtrkg  29071  eengtrkge  29072  edglnl  29228  subgruhgredgd  29369  nbfusgrlevtxm2  29463  lfgriswlk  29772  wwlknbp1  29929  usgrwwlks2on  30043  umgrwwlks2on  30044  rusgrnumwwlks  30062  clwlkclwwlkfo  30096  3spthd  30263  3vfriswmgr  30365  frgr2wwlkeqm  30418  numclwwlk1lem2f  30442  numclwwlk2  30468  numclwwlk3  30472  numclwwlk5  30475  grpomuldivass  30628  ablomuldiv  30639  ablodivdiv4  30641  ablonnncan1  30644  nvmdi  30735  dipassr  30933  archiabllem2c  33288  dvrcan5  33329  rloccring  33363  reofld  33435  eqgvscpbl  33442  qusvsval  33444  quslmod  33450  quslmhm  33451  prmidlc  33540  ssdifidl  33549  ssmxidl  33566  ply1degltlss  33688  r1plmhm  33702  drgextlsp  33770  ccfldsrarelvec  33848  constrconj  33922  constrfin  33923  constrelextdg2  33924  pstmfval  34073  qqhval2lem  34158  qqhvq  34164  measdivcst  34401  measdivcstALTV  34402  carsggect  34495  tgoldbachgtd  34839  bnj1098  34959  bnj149  35050  bnj1118  35159  erdszelem9  35412  resconn  35459  cvmseu  35489  cvmlift2lem10  35525  cvmlift2lem12  35527  ex-sategoelel  35634  elmrsubrn  35733  mclsind  35783  r1peuqusdeg1  35856  cgrid2  36216  segconeu  36224  btwncomim  36226  btwnswapid  36230  trisegint  36241  cgrxfr  36268  brofs2  36290  endofsegid  36298  btwnconn2  36315  seglemin  36326  segletr  36327  btwnsegle  36330  colinbtwnle  36331  broutsideof2  36335  btwnoutside  36338  broutsideof3  36339  outsideoftr  36342  outsidele  36345  fvray  36354  fvline  36357  ellines  36365  weiunpo  36678  broucube  37894  ftc1anc  37941  sdclem1  37983  sstotbnd2  38014  iscringd  38238  lsmsat  39373  lfladdcl  39436  lflnegcl  39440  lflvscl  39442  eqlkr  39464  lshpkrlem4  39478  lshpkrlem6  39480  ldualgrplem  39510  lduallmodlem  39517  latmassOLD  39594  latm12  39595  latm32  39596  latmrot  39597  latmmdiN  39599  latmmdir  39600  omlfh1N  39623  omlfh3N  39624  cvrnbtwn2  39640  cvlexchb1  39695  cvlsupr2  39708  hlatjass  39735  hlatj12  39736  hlatj32  39737  cvrat  39787  cvrat2  39794  atltcvr  39800  atexchltN  39806  cvrat3  39807  cvrat4  39808  atbtwnexOLDN  39812  atbtwnex  39813  3dimlem3  39826  3dimlem3OLDN  39827  3at  39855  2atneat  39880  llncmp  39887  2at0mat0  39890  2atmat0  39891  llncvrlpln  39923  lplncmp  39927  2llnjaN  39931  4atlem11  39974  lplncvrlvol  39981  lvolcmp  39982  2atm2atN  40150  elpaddatriN  40168  paddasslem8  40192  paddass  40203  padd12N  40204  paddssw2  40209  paddss  40210  pmod1i  40213  pmodN  40215  pmapjlln1  40220  atmod1i1  40222  atmod1i2  40224  pexmidlem2N  40336  pl42lem2N  40345  pl42lem3N  40346  pl42lem4N  40347  pl42N  40348  lhpm0atN  40394  lautlt  40456  lautcvr  40457  lautj  40458  lautm  40459  ltrneq2  40513  cdlemd1  40563  cdleme1b  40591  cdleme1  40592  cdleme2  40593  cdleme3e  40597  cdlemefr27cl  40768  cdlemefs27cl  40778  cdleme42ke  40850  cdleme42mN  40852  cdlemf2  40927  cdlemftr2  40931  trljco  41105  tgrpgrplem  41114  tendoplass  41148  tendodi1  41149  tendodi2  41150  cdlemk34  41275  cdlemk36  41278  erngdvlem3-rN  41363  tendospdi1  41385  dialss  41411  dvhvaddass  41462  dvhopvsca  41467  dvhlveclem  41473  diblss  41535  diclss  41558  diclspsn  41559  cdlemn11pre  41575  dihmeetlem12N  41683  dihmeetlem16N  41687  dihmeetlem17N  41688  dihmeetlem18N  41689  dvh4dimN  41812  lpolconN  41852  dochpolN  41855  lclkr  41898  lclkrs  41904  lcfr  41950  aks6d1c1  42475  irrapxlem6  43173  jm2.26lem3  43347  dgrsub2  43481  mpaaroot  43501  mendring  43534  mendlmod  43535  mendassa  43536  relexpmulg  44055  iunrelexpmin2  44057  relexpxpmin  44062  neicvgel1  44464  grumnud  44631  rfcnpre3  45382  fmuldfeq  45932  xlimbr  46174  stoweidlem43  46390  stoweidlem52  46399  stoweidlem53  46400  stoweidlem56  46403  stoweidlem57  46404  stoweidlem60  46407  issmfle  47092  issmfgt  47103  issmfge  47117  smflimlem4  47121  ltsubsubaddltsub  47650  iccpartigtl  47772  iccelpart  47782  prproropf1olem1  47852  fpprel2  48090  cycl3grtrilem  48295  grlimprclnbgr  48345  upgrwlkupwlk  48489  copissgrp  48517  cznrng  48610  funcringcsetcALTV2lem9  48647  funcringcsetclem9ALTV  48670  ldepsprlem  48821  lincresunit3  48830  lincreslvec3  48831  itsclc0yqe  49110  itsclc0yqsol  49113  resipos  49323  topdlat  49352  catprs  49359  endmndlem  49363  idmon  49368  idepi  49369  thincmon  49781  thincepi  49782  functhinclem1  49792  grptcmon  49941  grptcepi  49942