Theorem simpr2 1214

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr12  1277  simpr22  1280  simpr32  1283  simp1r2  1289  simp2r2  1295  simp3r2  1301  3anandis  1500  fpr2g  7209  isopolem  7345  fr3nr  7775  sexp3  8154  dif1en  9161  frfi  9260  intrnfi  9392  fisupcl  9446  cnfcomlem  9684  ackbij1lem15  10289  cofsmo  10325  sornom  10333  fpwwe2lem4  10697  dedekindle  11452  supmul1  12264  eluzuzle  12952  xlesubadd  13371  elioc2  13518  elico2  13519  elicc2  13520  fseq1p1m1  13709  fz0fzelfz0  13745  hash7g  14608  swrdsbslen  14791  ccatswrd  14795  swrdswrdlem  14830  wwlktovf1  15087  tanadd  16312  dvds2ln  16436  cshwsidrepsw  17248  ressress  17402  f1ovscpbl  17675  mreexexlem4d  17798  mreexexd  17799  iscatd2  17832  2oppccomf  17876  issubc3  18001  fthmon  18081  fuccocl  18119  fucidcl  18120  invfuc  18129  initoeu2lem0  18165  initoeu2lem1  18166  curf2cl  18382  yonedalem4c  18428  yonedalem3  18431  pospo  18494  latjle12  18601  latjlej1  18604  latnlej2  18610  latlem12  18617  latmlem1  18620  latledi  18628  latjass  18634  latj12  18635  latj32  18636  latj13  18637  latj31  18638  latjrot  18639  latjjdi  18642  latjjdir  18643  latdisdlem  18647  prdssgrpd  18899  prdsmndd  18941  mndissubm  18979  frmdmnd  19032  grpsubrcan  19208  grpsubadd  19215  grpaddsubass  19217  grpsubsub4  19220  grppnpcan2  19221  grpnpncan  19222  mulgnndir  19290  mulgnn0dir  19291  mulgdir  19293  mulgnnass  19296  mulgnn0ass  19297  mulgass  19298  mulgsubdir  19301  pwsmulg  19306  issubg2  19329  eqgval  19366  qusgrp  19378  galcan  19495  gacan  19496  oppgmnd  19545  fvcosymgeq  19620  pmtrprfv  19644  psgnunilem3  19687  cmn32  19991  cmn12  19993  abladdsub  20003  ablsubaddsub  20005  ablsubsub23  20015  mulgdi  20017  mulgsubdi  20020  dprdss  20222  dprdz  20223  dprdf1o  20225  dprdsn  20229  dprd2da  20235  dmdprdsplit  20240  ablfac1b  20263  pgpfac1lem5  20272  prdsrngd  20375  srgdilem  20395  srgbinom  20434  ringdilem  20453  prdsringd  20527  opprrng  20552  mulgass3  20560  dvrass  20615  dvrdir  20619  subrgunit  20819  issubrg2  20821  isdomn4  20944  abvdiv  21063  lsssn0  21200  islss3  21211  prdslmodd  21221  islmhm2  21290  lspsolv  21398  islbs2  21409  islbs3  21410  lbsextlem4  21416  sralmod  21439  rnglidl1  21489  prmidlc  21606  ssdifidl  21618  psgndiflemB  21883  ipdir  21922  ipdi  21923  ipsubdir  21925  ipsubdi  21926  ipass  21928  ipassr  21929  ipassr2  21930  isphld  21937  ocvlss  21955  sraassab  22153  psrlmod  22244  psrring  22254  psrassa  22257  mamudm  22687  matring  22735  matassa  22736  ofco2  22743  ma1repveval  22863  mdetunilem1  22904  mdetunilem9  22912  chpscmatgsumbin  23139  iinopn  23197  restopnb  23470  subbascn  23549  nrmsep2  23651  isnrm3  23654  regsep2  23671  dnsconst  23673  dfconn2  23714  1stcelcls  23757  dislly  23793  ptuni2  23872  tx1stc  23946  0nelfb  24127  infil  24159  fsubbas  24163  filssufilg  24207  hauspwpwf1  24283  cnextcn  24363  tmdcn2  24385  ustuqtoplem  24535  utopsnneiplem  24543  psmettri  24607  isxmet2d  24623  xmettri  24647  xmetres2  24657  bldisj  24694  blss2ps  24699  blss2  24700  xmstri2  24762  mstri2  24763  xmstri  24764  mstri  24765  xmstri3  24766  mstri3  24767  msrtri  24768  comet  24809  stdbdbl  24813  met2ndci  24818  ngprcan  24906  ngplcan  24907  ngpsubcan  24910  nmtri2  24923  nrgdsdi  24961  nrgdsdir  24962  nlmdsdi  24977  nlmdsdir  24978  blcvx  25094  icoopnst  25237  pi1grplem  25347  clmpm1dir  25401  cmodscmulexp  25420  cvsdiv  25430  cvsdivcl  25431  cphdivcl  25480  cphsubdir  25506  cphsubdi  25507  tcphcph  25535  bcthlem5  25626  volfiniun  25845  volcn  25904  itg1val2  25982  dvconst  26214  dvlip  26290  ftc1a  26334  ulmval  26686  ulmdvlem3  26708  ang180  27121  cvxcl  27291  scvxcvx  27292  sgmmul  27507  dchrabl  27560  gausslemma2dlem1a  27671  nosupbnd1  28050  noinfbnd1lem5  28063  noinfbnd1  28065  sltsss2  28131  addscom  28331  addbday  28383  motgrp  28985  iscgra1  29296  cgrane1  29298  cgrane3  29300  cgrahl1  29302  cgrahl2  29303  cgracgr  29304  cgratr  29309  cgrabtwn  29313  cgrahl  29314  dfcgra2  29317  sacgr  29318  angmgmaddcl  29370  f1otrge  29428  colinearalglem1  29463  axcgrtr  29472  axeuclidlem  29519  axcontlem3  29523  axcontlem4  29524  axcontlem7  29527  eengtrkg  29543  eengtrkge  29544  edglnl  29700  subgruhgredgd  29844  nbfusgrlevtxm2  29938  lfgriswlk  30250  wwlknbp1  30412  usgrwwlks2on  30526  umgrwwlks2on  30527  rusgrnumwwlks  30545  clwlkclwwlkfo  30579  3spthd  30756  3vfriswmgr  30858  frgr2wwlkeqm  30911  numclwwlk1lem2f  30935  numclwwlk2  30961  numclwwlk3  30965  numclwwlk5  30968  grpomuldivass  31122  ablomuldiv  31133  ablodivdiv4  31135  ablonnncan1  31138  nvmdi  31229  dipassr  31427  archiabllem2c  33735  dvrcan5  33775  rloccring  33811  reofld  33883  eqgvscpbl  33890  qusvsval  33892  quslmod  33898  quslmhm  33899  ssmxidl  33978  ply1degltlss  34107  r1plmhm  34120  drgextlsp  34205  ccfldsrarelvec  34282  constrconj  34356  constrfin  34357  constrelextdg2  34358  pstmfval  34507  qqhval2lem  34592  qqhvq  34598  measdivcst  34836  measdivcstALTV  34837  carsggect  34930  tgoldbachgtd  35271  bnj1098  35394  bnj149  35485  bnj1118  35594  erdszelem9  35930  resconn  35977  cvmseu  36007  cvmlift2lem10  36043  cvmlift2lem12  36045  ex-sategoelel  36152  elmrsubrn  36251  mclsind  36301  r1peuqusdeg1  36374  cgrid2  36735  segconeu  36743  btwncomim  36745  btwnswapid  36749  trisegint  36760  cgrxfr  36787  brofs2  36809  endofsegid  36817  btwnconn2  36834  seglemin  36845  segletr  36846  btwnsegle  36849  colinbtwnle  36850  broutsideof2  36854  btwnoutside  36857  broutsideof3  36858  outsideoftr  36861  outsidele  36864  fvray  36873  fvline  36876  ellines  36884  nmulprop  36906  weiunpo  37220  broucube  38537  ftc1anc  38584  sdclem1  38642  sstotbnd2  38673  iscringd  38897  lsmsat  40030  lfladdcl  40093  lflnegcl  40097  lflvscl  40099  eqlkr  40121  lshpkrlem4  40135  lshpkrlem6  40137  ldualgrplem  40167  lduallmodlem  40174  latmassOLD  40251  latm12  40252  latm32  40253  latmrot  40254  latmmdiN  40256  latmmdir  40257  omlfh1N  40280  omlfh3N  40281  cvrnbtwn2  40297  cvlexchb1  40352  cvlsupr2  40365  hlatjass  40392  hlatj12  40393  hlatj32  40394  cvrat  40444  cvrat2  40451  atltcvr  40457  atexchltN  40463  cvrat3  40464  cvrat4  40465  atbtwnexOLDN  40469  atbtwnex  40470  3dimlem3  40483  3dimlem3OLDN  40484  3at  40512  2atneat  40537  llncmp  40544  2at0mat0  40547  2atmat0  40548  llncvrlpln  40580  lplncmp  40584  2llnjaN  40588  4atlem11  40631  lplncvrlvol  40638  lvolcmp  40639  2atm2atN  40807  elpaddatriN  40825  paddasslem8  40849  paddass  40860  padd12N  40861  paddssw2  40866  paddss  40867  pmod1i  40870  pmodN  40872  pmapjlln1  40877  atmod1i1  40879  atmod1i2  40881  pexmidlem2N  40993  pl42lem2N  41002  pl42lem3N  41003  pl42lem4N  41004  pl42N  41005  lhpm0atN  41051  lautlt  41113  lautcvr  41114  lautj  41115  lautm  41116  ltrneq2  41170  cdlemd1  41220  cdleme1b  41248  cdleme1  41249  cdleme2  41250  cdleme3e  41254  cdlemefr27cl  41425  cdlemefs27cl  41435  cdleme42ke  41507  cdleme42mN  41509  cdlemf2  41584  cdlemftr2  41588  trljco  41762  tgrpgrplem  41771  tendoplass  41805  tendodi1  41806  tendodi2  41807  cdlemk34  41932  cdlemk36  41935  erngdvlem3-rN  42020  tendospdi1  42042  dialss  42068  dvhvaddass  42119  dvhopvsca  42124  dvhlveclem  42130  diblss  42192  diclss  42215  diclspsn  42216  cdlemn11pre  42232  dihmeetlem12N  42340  dihmeetlem16N  42344  dihmeetlem17N  42345  dihmeetlem18N  42346  dvh4dimN  42469  lpolconN  42509  dochpolN  42512  lclkr  42555  lclkrs  42561  lcfr  42607  aks6d1c1  43131  irrapxlem6  43784  jm2.26lem3  43958  dgrsub2  44092  mpaaroot  44112  mendring  44145  mendlmod  44146  mendassa  44147  relexpmulg  44666  iunrelexpmin2  44668  relexpxpmin  44673  neicvgel1  45075  grumnud  45226  rfcnpre3  45990  fmuldfeq  46536  xlimbr  46778  stoweidlem43  46994  stoweidlem52  47003  stoweidlem53  47004  stoweidlem56  47007  stoweidlem57  47008  stoweidlem60  47011  issmfle  47696  issmfgt  47707  issmfge  47721  smflimlem4  47725  tmachlem-franscan  47900  ltsubsubaddltsub  48312  iccpartigtl  48446  iccelpart  48456  prproropf1olem1  48526  fpprel2  48780  cycl3grtrilem  48985  grlimprclnbgr  49035  upgrwlkupwlk  49179  copissgrp  49206  cznrng  49299  funcringcsetcALTV2lem9  49336  funcringcsetclem9ALTV  49359  idomcanl  49385  ldepsprlem  49525  lincresunit3  49534  lincreslvec3  49535  itsclc0yqe  49814  itsclc0yqsol  49817  resipos  50024  topdlat  50053  catprs  50060  endmndlem  50064  idmon  50069  idepi  50070  thincmon  50482  thincepi  50483  functhinclem1  50493  grptcmon  50642  grptcepi  50643  nellindf  50911