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  7159  isopolem  7293  fr3nr  7719  sexp3  8097  dif1en  9090  frfi  9189  intrnfi  9323  fisupcl  9377  cnfcomlem  9612  ackbij1lem15  10147  cofsmo  10183  sornom  10191  fpwwe2lem4  10549  dedekindle  11301  supmul1  12115  eluzuzle  12764  xlesubadd  13182  elioc2  13329  elico2  13330  elicc2  13331  fseq1p1m1  13518  fz0fzelfz0  13554  hash7g  14413  swrdsbslen  14592  ccatswrd  14596  swrdswrdlem  14631  wwlktovf1  14884  tanadd  16096  dvds2ln  16220  cshwsidrepsw  17025  ressress  17178  f1ovscpbl  17451  mreexexlem4d  17574  mreexexd  17575  iscatd2  17608  2oppccomf  17652  issubc3  17777  fthmon  17857  fuccocl  17895  fucidcl  17896  invfuc  17905  initoeu2lem0  17941  initoeu2lem1  17942  curf2cl  18158  yonedalem4c  18204  yonedalem3  18207  pospo  18270  latjle12  18377  latjlej1  18380  latnlej2  18386  latlem12  18393  latmlem1  18396  latledi  18404  latjass  18410  latj12  18411  latj32  18412  latj13  18413  latj31  18414  latjrot  18415  latjjdi  18418  latjjdir  18419  latdisdlem  18423  prdssgrpd  18662  prdsmndd  18699  mndissubm  18736  frmdmnd  18788  grpsubrcan  18955  grpsubadd  18962  grpaddsubass  18964  grpsubsub4  18967  grppnpcan2  18968  grpnpncan  18969  mulgnndir  19037  mulgnn0dir  19038  mulgdir  19040  mulgnnass  19043  mulgnn0ass  19044  mulgass  19045  mulgsubdir  19048  pwsmulg  19053  issubg2  19075  eqgval  19110  qusgrp  19119  galcan  19237  gacan  19238  oppgmnd  19287  fvcosymgeq  19362  pmtrprfv  19386  psgnunilem3  19429  cmn32  19733  cmn12  19735  abladdsub  19745  ablsubaddsub  19747  ablsubsub23  19757  mulgdi  19759  mulgsubdi  19762  dprdss  19964  dprdz  19965  dprdf1o  19967  dprdsn  19971  dprd2da  19977  dmdprdsplit  19982  ablfac1b  20005  pgpfac1lem5  20014  prdsrngd  20115  srgdilem  20131  srgbinom  20170  ringdilem  20188  prdsringd  20260  opprrng  20285  mulgass3  20293  dvrass  20348  dvrdir  20352  subrgunit  20527  issubrg2  20529  isdomn4  20653  abvdiv  20766  lsssn0  20903  islss3  20914  prdslmodd  20924  islmhm2  20994  lspsolv  21102  islbs2  21113  islbs3  21114  lbsextlem4  21120  sralmod  21143  rnglidl1  21191  psgndiflemB  21559  ipdir  21598  ipdi  21599  ipsubdir  21601  ipsubdi  21602  ipass  21604  ipassr  21605  ipassr2  21606  isphld  21613  ocvlss  21631  sraassab  21827  sraassaOLD  21829  psrlmod  21919  psrring  21929  psrassa  21932  mamudm  22343  matring  22391  matassa  22392  ofco2  22399  ma1repveval  22519  mdetunilem1  22560  mdetunilem9  22568  chpscmatgsumbin  22792  iinopn  22850  restopnb  23123  subbascn  23202  nrmsep2  23304  isnrm3  23307  regsep2  23324  dnsconst  23326  dfconn2  23367  1stcelcls  23409  dislly  23445  ptuni2  23524  tx1stc  23598  0nelfb  23779  infil  23811  fsubbas  23815  filssufilg  23859  hauspwpwf1  23935  cnextcn  24015  tmdcn2  24037  ustuqtoplem  24187  utopsnneiplem  24195  psmettri  24259  isxmet2d  24275  xmettri  24299  xmetres2  24309  bldisj  24346  blss2ps  24351  blss2  24352  xmstri2  24414  mstri2  24415  xmstri  24416  mstri  24417  xmstri3  24418  mstri3  24419  msrtri  24420  comet  24461  stdbdbl  24465  met2ndci  24470  ngprcan  24558  ngplcan  24559  ngpsubcan  24562  nmtri2  24575  nrgdsdi  24613  nrgdsdir  24614  nlmdsdi  24629  nlmdsdir  24630  blcvx  24746  icoopnst  24896  pi1grplem  25009  clmpm1dir  25063  cmodscmulexp  25082  cvsdiv  25092  cvsdivcl  25093  cphdivcl  25142  cphsubdir  25168  cphsubdi  25169  tcphcph  25197  bcthlem5  25288  volfiniun  25508  volcn  25567  itg1val2  25645  dvconst  25878  dvlip  25958  ftc1a  26004  ulmval  26349  ulmdvlem3  26371  ang180  26784  cvxcl  26955  scvxcvx  26956  sgmmul  27172  dchrabl  27225  gausslemma2dlem1a  27336  nosupbnd1  27686  noinfbnd1lem5  27699  noinfbnd1  27701  ssltss2  27766  addscom  27948  addsbday  28000  motgrp  28598  iscgra1  28865  cgrane1  28867  cgrane3  28869  cgrahl1  28871  cgrahl2  28872  cgracgr  28873  cgratr  28878  cgrabtwn  28881  cgrahl  28882  dfcgra2  28885  sacgr  28886  f1otrge  28927  colinearalglem1  28962  axcgrtr  28971  axeuclidlem  29018  axcontlem3  29022  axcontlem4  29023  axcontlem7  29026  eengtrkg  29042  eengtrkge  29043  edglnl  29199  subgruhgredgd  29340  nbfusgrlevtxm2  29434  lfgriswlk  29743  wwlknbp1  29900  usgrwwlks2on  30014  umgrwwlks2on  30015  rusgrnumwwlks  30033  clwlkclwwlkfo  30067  3spthd  30234  3vfriswmgr  30336  frgr2wwlkeqm  30389  numclwwlk1lem2f  30413  numclwwlk2  30439  numclwwlk3  30443  numclwwlk5  30446  grpomuldivass  30599  ablomuldiv  30610  ablodivdiv4  30612  ablonnncan1  30615  nvmdi  30706  dipassr  30904  archiabllem2c  33258  dvrcan5  33299  rloccring  33333  reofld  33405  eqgvscpbl  33412  qusvsval  33414  quslmod  33420  quslmhm  33421  prmidlc  33510  ssdifidl  33519  ssmxidl  33536  ply1degltlss  33658  r1plmhm  33672  drgextlsp  33731  ccfldsrarelvec  33809  constrconj  33883  constrfin  33884  constrelextdg2  33885  pstmfval  34034  qqhval2lem  34119  qqhvq  34125  measdivcst  34362  measdivcstALTV  34363  carsggect  34456  tgoldbachgtd  34800  bnj1098  34920  bnj149  35012  bnj1118  35121  erdszelem9  35374  resconn  35421  cvmseu  35451  cvmlift2lem10  35487  cvmlift2lem12  35489  ex-sategoelel  35596  elmrsubrn  35695  mclsind  35745  r1peuqusdeg1  35818  cgrid2  36178  segconeu  36186  btwncomim  36188  btwnswapid  36192  trisegint  36203  cgrxfr  36230  brofs2  36252  endofsegid  36260  btwnconn2  36277  seglemin  36288  segletr  36289  btwnsegle  36292  colinbtwnle  36293  broutsideof2  36297  btwnoutside  36300  broutsideof3  36301  outsideoftr  36304  outsidele  36307  fvray  36316  fvline  36319  ellines  36327  weiunpo  36640  broucube  37826  ftc1anc  37873  sdclem1  37915  sstotbnd2  37946  iscringd  38170  lsmsat  39305  lfladdcl  39368  lflnegcl  39372  lflvscl  39374  eqlkr  39396  lshpkrlem4  39410  lshpkrlem6  39412  ldualgrplem  39442  lduallmodlem  39449  latmassOLD  39526  latm12  39527  latm32  39528  latmrot  39529  latmmdiN  39531  latmmdir  39532  omlfh1N  39555  omlfh3N  39556  cvrnbtwn2  39572  cvlexchb1  39627  cvlsupr2  39640  hlatjass  39667  hlatj12  39668  hlatj32  39669  cvrat  39719  cvrat2  39726  atltcvr  39732  atexchltN  39738  cvrat3  39739  cvrat4  39740  atbtwnexOLDN  39744  atbtwnex  39745  3dimlem3  39758  3dimlem3OLDN  39759  3at  39787  2atneat  39812  llncmp  39819  2at0mat0  39822  2atmat0  39823  llncvrlpln  39855  lplncmp  39859  2llnjaN  39863  4atlem11  39906  lplncvrlvol  39913  lvolcmp  39914  2atm2atN  40082  elpaddatriN  40100  paddasslem8  40124  paddass  40135  padd12N  40136  paddssw2  40141  paddss  40142  pmod1i  40145  pmodN  40147  pmapjlln1  40152  atmod1i1  40154  atmod1i2  40156  pexmidlem2N  40268  pl42lem2N  40277  pl42lem3N  40278  pl42lem4N  40279  pl42N  40280  lhpm0atN  40326  lautlt  40388  lautcvr  40389  lautj  40390  lautm  40391  ltrneq2  40445  cdlemd1  40495  cdleme1b  40523  cdleme1  40524  cdleme2  40525  cdleme3e  40529  cdlemefr27cl  40700  cdlemefs27cl  40710  cdleme42ke  40782  cdleme42mN  40784  cdlemf2  40859  cdlemftr2  40863  trljco  41037  tgrpgrplem  41046  tendoplass  41080  tendodi1  41081  tendodi2  41082  cdlemk34  41207  cdlemk36  41210  erngdvlem3-rN  41295  tendospdi1  41317  dialss  41343  dvhvaddass  41394  dvhopvsca  41399  dvhlveclem  41405  diblss  41467  diclss  41490  diclspsn  41491  cdlemn11pre  41507  dihmeetlem12N  41615  dihmeetlem16N  41619  dihmeetlem17N  41620  dihmeetlem18N  41621  dvh4dimN  41744  lpolconN  41784  dochpolN  41787  lclkr  41830  lclkrs  41836  lcfr  41882  aks6d1c1  42407  irrapxlem6  43105  jm2.26lem3  43279  dgrsub2  43413  mpaaroot  43433  mendring  43466  mendlmod  43467  mendassa  43468  relexpmulg  43987  iunrelexpmin2  43989  relexpxpmin  43994  neicvgel1  44396  grumnud  44563  rfcnpre3  45314  fmuldfeq  45865  xlimbr  46107  stoweidlem43  46323  stoweidlem52  46332  stoweidlem53  46333  stoweidlem56  46336  stoweidlem57  46337  stoweidlem60  46340  issmfle  47025  issmfgt  47036  issmfge  47050  smflimlem4  47054  ltsubsubaddltsub  47583  iccpartigtl  47705  iccelpart  47715  prproropf1olem1  47785  fpprel2  48023  cycl3grtrilem  48228  grlimprclnbgr  48278  upgrwlkupwlk  48422  copissgrp  48450  cznrng  48543  funcringcsetcALTV2lem9  48580  funcringcsetclem9ALTV  48603  ldepsprlem  48754  lincresunit3  48763  lincreslvec3  48764  itsclc0yqe  49043  itsclc0yqsol  49046  resipos  49256  topdlat  49285  catprs  49292  endmndlem  49296  idmon  49301  idepi  49302  thincmon  49714  thincepi  49715  functhinclem1  49725  grptcmon  49874  grptcepi  49875