Theorem simpr2 1196

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

This theorem is referenced by:  simpr12  1259  simpr22  1262  simpr32  1265  simp1r2  1271  simp2r2  1277  simp3r2  1283  3anandis  1473  fpr2g  7185  isopolem  7320  fr3nr  7748  sexp3  8132  dif1en  9124  frfi  9232  intrnfi  9367  fisupcl  9421  cnfcomlem  9652  ackbij1lem15  10186  cofsmo  10222  sornom  10230  fpwwe2lem4  10587  dedekindle  11338  supmul1  12152  eluzuzle  12802  xlesubadd  13223  elioc2  13370  elico2  13371  elicc2  13372  fseq1p1m1  13559  fz0fzelfz0  13595  hash7g  14451  swrdsbslen  14629  ccatswrd  14633  swrdswrdlem  14669  wwlktovf1  14923  tanadd  16135  dvds2ln  16259  cshwsidrepsw  17064  ressress  17217  f1ovscpbl  17489  mreexexlem4d  17608  mreexexd  17609  iscatd2  17642  2oppccomf  17686  issubc3  17811  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  initoeu2lem0  17975  initoeu2lem1  17976  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  pospo  18304  latjle12  18409  latjlej1  18412  latnlej2  18418  latlem12  18425  latmlem1  18428  latledi  18436  latjass  18442  latj12  18443  latj32  18444  latj13  18445  latj31  18446  latjrot  18447  latjjdi  18450  latjjdir  18451  latdisdlem  18455  prdssgrpd  18660  prdsmndd  18697  mndissubm  18734  frmdmnd  18786  grpsubrcan  18953  grpsubadd  18960  grpaddsubass  18962  grpsubsub4  18965  grppnpcan2  18966  grpnpncan  18967  mulgnndir  19035  mulgnn0dir  19036  mulgdir  19038  mulgnnass  19041  mulgnn0ass  19042  mulgass  19043  mulgsubdir  19046  pwsmulg  19051  issubg2  19073  eqgval  19109  qusgrp  19118  galcan  19236  gacan  19237  oppgmnd  19286  fvcosymgeq  19359  pmtrprfv  19383  psgnunilem3  19426  cmn32  19730  cmn12  19732  abladdsub  19742  ablsubaddsub  19744  ablsubsub23  19754  mulgdi  19756  mulgsubdi  19759  dprdss  19961  dprdz  19962  dprdf1o  19964  dprdsn  19968  dprd2da  19974  dmdprdsplit  19979  ablfac1b  20002  pgpfac1lem5  20011  prdsrngd  20085  srgdilem  20101  srgbinom  20140  ringdilem  20158  prdsringd  20230  opprrng  20254  mulgass3  20262  dvrass  20317  dvrdir  20321  subrgunit  20499  issubrg2  20501  isdomn4  20625  abvdiv  20738  lsssn0  20854  islss3  20865  prdslmodd  20875  islmhm2  20945  lspsolv  21053  islbs2  21064  islbs3  21065  lbsextlem4  21071  sralmod  21094  rnglidl1  21142  psgndiflemB  21509  ipdir  21548  ipdi  21549  ipsubdir  21551  ipsubdi  21552  ipass  21554  ipassr  21555  ipassr2  21556  isphld  21563  ocvlss  21581  sraassab  21777  sraassaOLD  21779  psrgrpOLD  21866  psrlmod  21869  psrring  21879  psrassa  21882  mamudm  22282  matring  22330  matassa  22331  ofco2  22338  ma1repveval  22458  mdetunilem1  22499  mdetunilem9  22507  chpscmatgsumbin  22731  iinopn  22789  restopnb  23062  subbascn  23141  nrmsep2  23243  isnrm3  23246  regsep2  23263  dnsconst  23265  dfconn2  23306  1stcelcls  23348  dislly  23384  ptuni2  23463  tx1stc  23537  0nelfb  23718  infil  23750  fsubbas  23754  filssufilg  23798  hauspwpwf1  23874  cnextcn  23954  tmdcn2  23976  ustuqtoplem  24127  utopsnneiplem  24135  psmettri  24199  isxmet2d  24215  xmettri  24239  xmetres2  24249  bldisj  24286  blss2ps  24291  blss2  24292  xmstri2  24354  mstri2  24355  xmstri  24356  mstri  24357  xmstri3  24358  mstri3  24359  msrtri  24360  comet  24401  stdbdbl  24405  met2ndci  24410  ngprcan  24498  ngplcan  24499  ngpsubcan  24502  nmtri2  24515  nrgdsdi  24553  nrgdsdir  24554  nlmdsdi  24569  nlmdsdir  24570  blcvx  24686  icoopnst  24836  pi1grplem  24949  clmpm1dir  25003  cmodscmulexp  25022  cvsdiv  25032  cvsdivcl  25033  cphdivcl  25082  cphsubdir  25108  cphsubdi  25109  tcphcph  25137  bcthlem5  25228  volfiniun  25448  volcn  25507  itg1val2  25585  dvconst  25818  dvlip  25898  ftc1a  25944  ulmval  26289  ulmdvlem3  26311  ang180  26724  cvxcl  26895  scvxcvx  26896  sgmmul  27112  dchrabl  27165  gausslemma2dlem1a  27276  nosupbnd1  27626  noinfbnd1lem5  27639  noinfbnd1  27641  ssltss2  27701  addscom  27873  addsbday  27924  motgrp  28470  iscgra1  28737  cgrane1  28739  cgrane3  28741  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgratr  28750  cgrabtwn  28753  cgrahl  28754  dfcgra2  28757  sacgr  28758  f1otrge  28799  colinearalglem1  28833  axcgrtr  28842  axeuclidlem  28889  axcontlem3  28893  axcontlem4  28894  axcontlem7  28897  eengtrkg  28913  eengtrkge  28914  edglnl  29070  subgruhgredgd  29211  nbfusgrlevtxm2  29305  lfgriswlk  29616  wwlknbp1  29774  umgrwwlks2on  29887  rusgrnumwwlks  29904  clwlkclwwlkfo  29938  3spthd  30105  3vfriswmgr  30207  frgr2wwlkeqm  30260  numclwwlk1lem2f  30284  numclwwlk2  30310  numclwwlk3  30314  numclwwlk5  30317  grpomuldivass  30470  ablomuldiv  30481  ablodivdiv4  30483  ablonnncan1  30486  nvmdi  30577  dipassr  30775  archiabllem2c  33149  dvrcan5  33187  rloccring  33221  reofld  33315  eqgvscpbl  33321  qusvsval  33323  quslmod  33329  quslmhm  33330  prmidlc  33419  ssdifidl  33428  ssmxidl  33445  ply1degltlss  33562  r1plmhm  33575  drgextlsp  33589  ccfldsrarelvec  33666  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33886  qqhval2lem  33971  qqhvq  33977  measdivcst  34214  measdivcstALTV  34215  carsggect  34309  tgoldbachgtd  34653  bnj1098  34773  bnj149  34865  bnj1118  34974  erdszelem9  35186  resconn  35233  cvmseu  35263  cvmlift2lem10  35299  cvmlift2lem12  35301  ex-sategoelel  35408  elmrsubrn  35507  mclsind  35557  r1peuqusdeg1  35630  cgrid2  35991  segconeu  35999  btwncomim  36001  btwnswapid  36005  trisegint  36016  cgrxfr  36043  brofs2  36065  endofsegid  36073  btwnconn2  36090  seglemin  36101  segletr  36102  btwnsegle  36105  colinbtwnle  36106  broutsideof2  36110  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  outsidele  36120  fvray  36129  fvline  36132  ellines  36140  weiunpo  36453  broucube  37648  ftc1anc  37695  sdclem1  37737  sstotbnd2  37768  iscringd  37992  lsmsat  39001  lfladdcl  39064  lflnegcl  39068  lflvscl  39070  eqlkr  39092  lshpkrlem4  39106  lshpkrlem6  39108  ldualgrplem  39138  lduallmodlem  39145  latmassOLD  39222  latm12  39223  latm32  39224  latmrot  39225  latmmdiN  39227  latmmdir  39228  omlfh1N  39251  omlfh3N  39252  cvrnbtwn2  39268  cvlexchb1  39323  cvlsupr2  39336  hlatjass  39363  hlatj12  39364  hlatj32  39365  cvrat  39416  cvrat2  39423  atltcvr  39429  atexchltN  39435  cvrat3  39436  cvrat4  39437  atbtwnexOLDN  39441  atbtwnex  39442  3dimlem3  39455  3dimlem3OLDN  39456  3at  39484  2atneat  39509  llncmp  39516  2at0mat0  39519  2atmat0  39520  llncvrlpln  39552  lplncmp  39556  2llnjaN  39560  4atlem11  39603  lplncvrlvol  39610  lvolcmp  39611  2atm2atN  39779  elpaddatriN  39797  paddasslem8  39821  paddass  39832  padd12N  39833  paddssw2  39838  paddss  39839  pmod1i  39842  pmodN  39844  pmapjlln1  39849  atmod1i1  39851  atmod1i2  39853  pexmidlem2N  39965  pl42lem2N  39974  pl42lem3N  39975  pl42lem4N  39976  pl42N  39977  lhpm0atN  40023  lautlt  40085  lautcvr  40086  lautj  40087  lautm  40088  ltrneq2  40142  cdlemd1  40192  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3e  40226  cdlemefr27cl  40397  cdlemefs27cl  40407  cdleme42ke  40479  cdleme42mN  40481  cdlemf2  40556  cdlemftr2  40560  trljco  40734  tgrpgrplem  40743  tendoplass  40777  tendodi1  40778  tendodi2  40779  cdlemk34  40904  cdlemk36  40907  erngdvlem3-rN  40992  tendospdi1  41014  dialss  41040  dvhvaddass  41091  dvhopvsca  41096  dvhlveclem  41102  diblss  41164  diclss  41187  diclspsn  41188  cdlemn11pre  41204  dihmeetlem12N  41312  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem18N  41318  dvh4dimN  41441  lpolconN  41481  dochpolN  41484  lclkr  41527  lclkrs  41533  lcfr  41579  aks6d1c1  42104  irrapxlem6  42815  jm2.26lem3  42990  dgrsub2  43124  mpaaroot  43144  mendring  43177  mendlmod  43178  mendassa  43179  relexpmulg  43699  iunrelexpmin2  43701  relexpxpmin  43706  neicvgel1  44108  grumnud  44275  rfcnpre3  45027  fmuldfeq  45581  xlimbr  45825  stoweidlem43  46041  stoweidlem52  46050  stoweidlem53  46051  stoweidlem56  46054  stoweidlem57  46055  stoweidlem60  46058  issmfle  46743  issmfgt  46754  issmfge  46768  smflimlem4  46772  ltsubsubaddltsub  47302  iccpartigtl  47424  iccelpart  47434  prproropf1olem1  47504  fpprel2  47742  cycl3grtrilem  47945  grlimgrtrilem1  47993  upgrwlkupwlk  48128  copissgrp  48156  cznrng  48249  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  ldepsprlem  48461  lincresunit3  48470  lincreslvec3  48471  itsclc0yqe  48750  itsclc0yqsol  48753  resipos  48963  topdlat  48992  catprs  49000  endmndlem  49004  idmon  49009  idepi  49010  thincmon  49422  thincepi  49423  functhinclem1  49433  grptcmon  49582  grptcepi  49583