Theorem simpr1 1187

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpr1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1

Step	Hyp	Ref	Expression
1		simpr 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1181	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  simpr11  1250  simpr21  1253  simpr31  1256  simp1r1  1262  simp2r1  1268  simp3r1  1274  3anandis  1463  fpr2g  6847  isopolem  6968  fr3nr  7357  suppfnss  7713  frfi  8616  intrnfi  8733  iinfi  8734  eqsup  8773  fisupcl  8786  cnfcomlem  9015  ackbij1lem15  9509  fpwwe2lem5  9909  dedekindle  10657  ico0  12638  elioc2  12653  elico2  12654  elicc2  12655  iccsplit  12725  fseq1p1m1  12835  elfz0ubfz0  12865  hashtpg  13693  swrdsbslen  13866  swrdspsleq  13867  ccatswrd  13870  tanadd  15357  dvds2ln  15479  qredeq  15834  ressress  16395  mreexexlem4d  16751  mreexexd  16752  0catg  16791  2oppccomf  16828  issubc3  16952  fthmon  17030  fuccocl  17067  fucidcl  17068  invfuc  17077  initoeu2lem0  17106  initoeu2lem1  17107  curf2cl  17314  yonedalem4c  17360  yonedalem3  17363  pospo  17416  latjle12  17505  latjlej1  17508  latnlej2  17514  latlem12  17521  latmlem1  17524  latledi  17532  latmlej11  17533  latjass  17538  latj12  17539  latj32  17540  latj13  17541  latj31  17542  latjrot  17543  latjjdi  17546  latjjdir  17547  latdisdlem  17632  prdsmndd  17766  imasmnd2  17770  frmdmnd  17839  grpsubrcan  17941  grpsubadd  17948  grpsubsub  17949  grpaddsubass  17950  grpsubsub4  17953  grpnnncan2  17957  imasgrp2  17975  mulgnndir  18014  mulgnn0dir  18015  mulgdir  18017  mulgnnass  18020  mulgnn0ass  18021  mulgass  18022  mulgsubdir  18025  pwsmulg  18030  issubg2  18052  eqgval  18086  qusgrp  18092  galcan  18179  gacan  18180  oppgmnd  18227  symggrp  18263  pmtrprfv  18316  pmtr3ncom  18338  psgnunilem3  18359  cmn32  18655  cmn12  18657  abladdsub  18664  mulgnn0di  18675  mulgdi  18676  mulgsubdi  18679  dprdss  18872  dprdz  18873  dprdf1o  18875  dprdsn  18879  dprd2da  18885  ablfac1b  18913  pgpfac1lem5  18922  srgbinomlem2  18985  srgbinom  18989  ringi  19004  prdsringd  19056  imasring  19063  opprring  19075  mulgass3  19081  dvrass  19134  kerf1ghm  19191  kerf1hrmOLD  19192  subrgunit  19247  issubrg2  19249  abvdiv  19302  islss3  19425  prdslmodd  19435  islmhm2  19504  lspsolv  19609  islbs2  19620  islbs3  19621  lbsextlem4  19627  sralmod  19653  issubassa  19790  sraassa  19791  psrbaglecl  19841  psrbagcon  19843  psrgrp  19870  psrlmod  19873  psrring  19883  psrassa  19886  ipdir  20469  ipdi  20470  ipsubdir  20472  ipsubdi  20473  ipass  20475  ipassr  20476  ipassr2  20477  ocvlss  20502  mamudm  20685  matring  20740  matassa  20741  ofco2  20748  mdetunilem1  20909  mdetunilem9  20917  mdetuni0  20918  mdetmul  20920  gsummatr01lem3  20954  iinopn  21198  subbascn  21550  nrmsep2  21652  isnrm3  21655  regsep2  21672  dnsconst  21674  dfconn2  21715  1stcelcls  21757  nllyidm  21785  dislly  21793  upxp  21919  fbasne0  22126  filss  22149  infil  22159  fsubbas  22163  filssufilg  22207  tmdcn2  22385  psmettri  22608  isxmet2d  22624  xmettri  22648  xmetres2  22658  bldisj  22695  blss2ps  22700  blss2  22701  xmstri2  22763  mstri2  22764  xmstri  22765  mstri  22766  xmstri3  22767  mstri3  22768  msrtri  22769  comet  22810  stdbdbl  22814  met2ndci  22819  ngprcan  22906  ngplcan  22907  ngpsubcan  22910  nmtri2  22923  nrgdsdi  22961  nrgdsdir  22962  nlmdsdi  22977  nlmdsdir  22978  blcvx  23093  icccmplem2  23118  pi1grplem  23340  pi1cof  23350  clmpm1dir  23394  cvsdiv  23423  cvsdivcl  23424  cphdivcl  23473  cphsubdir  23499  cphsubdi  23500  cphassr  23503  bcthlem5  23618  rrxcph  23682  volfiniun  23835  volcn  23894  itg1val2  23972  dvconst  24201  dvlip  24277  dvfsumlem4  24313  ftc1a  24321  ulmval  24655  ulmdvlem3  24677  ang180  25077  cvxcl  25248  scvxcvx  25249  sgmmul  25463  logexprlim  25487  dchrabl  25516  motgrp  26015  iscgra1  26282  cgrane1  26284  cgrane2  26285  cgrahl1  26288  cgrahl2  26289  cgracgr  26290  cgratr  26295  cgrabtwn  26298  dfcgra2  26302  sacgr  26303  sacgrOLD  26304  f1otrge  26345  colinearalglem1  26379  colinearalg  26383  axcgrtr  26388  axlowdimlem16  26430  axeuclidlem  26435  axcontlem7  26443  eengtrkg  26459  eengtrkge  26460  nbfusgrlevtxm2  26847  lfgriswlk  27156  upgrwlkdvde  27204  wwlknbp1  27308  erclwwlktr  27486  erclwwlkntr  27536  frgr2wwlkeqm  27798  numclwwlk1lem2f  27822  numclwwlk5  27855  friendship  27866  grpodivdiv  28004  grpomuldivass  28005  ablodivdiv4  28018  ablonnncan1  28021  nvmdi  28112  dipassr  28310  archiabllem2c  30458  dvrdir  30511  dvrcan5  30514  reofld  30563  eqgvscpbl  30569  qusscaval  30571  quslmod  30573  quslmhm  30574  drgextlsp  30596  ccfldsrarelvec  30656  pstmfval  30749  tpr2rico  30768  qqhval2lem  30835  qqhvq  30841  issiga  30984  measdivcst  31096  measdivcstALTV  31097  carsggect  31189  signsply0  31434  tgoldbachgtd  31546  bnj149  31759  bnj1118  31866  bnj1128  31872  erdszelem9  32056  resconn  32103  cvmseu  32133  cvmlift2lem12  32171  ex-sategoelel  32278  elmrsubrn  32377  mclsind  32427  frrlem4  32737  frrlem8  32741  noprefixmo  32813  nosupbnd1  32825  ssltss1  32868  cgrid2  33075  segconeu  33083  btwncomim  33085  btwnswapid  33089  cgrxfr  33127  btwnxfr  33128  colineardim1  33133  brofs2  33149  brifs2  33150  idinside  33156  endofsegid  33157  btwnconn1lem7  33165  btwnconn1lem11  33169  btwnconn1  33173  segcon2  33177  seglemin  33185  segletr  33186  btwnsegle  33189  colinbtwnle  33190  broutsideof2  33194  broutsideof3  33198  outsidele  33204  fvray  33213  fvline  33216  linerflx1  33221  ellines  33224  ivthALT  33294  poimirlem32  34476  ftc1anc  34527  sdclem1  34571  sstotbnd2  34605  zerdivemp1x  34778  isdrngo2  34789  iscringd  34829  lsmsat  35696  lfladdcl  35759  lflnegcl  35763  lflvscl  35765  lshpkrlem4  35801  lshpkrlem6  35803  ldualgrplem  35833  lduallmodlem  35840  latmassOLD  35917  latm12  35918  latm32  35919  latmrot  35920  latmmdiN  35922  latmmdir  35923  omlfh1N  35946  omlfh3N  35947  cvlexchb1  36018  cvlexch3  36020  cvlexch4N  36021  cvlatexchb1  36022  cvlsupr2  36031  hlatjass  36058  hlatj12  36059  hlatj32  36060  cvratlem  36109  cvrat  36110  atcvrj0  36116  cvrat2  36117  atltcvr  36123  atexchltN  36129  cvrat3  36130  cvrat4  36131  3dimlem3  36149  3dimlem3OLDN  36150  3at  36178  2atneat  36203  llncmp  36210  2at0mat0  36213  2atmat0  36214  lplnnle2at  36229  llncvrlpln  36246  lplncmp  36250  lplnexllnN  36252  2llnjaN  36254  4atlem11  36297  lplncvrlvol  36304  lvolcmp  36305  2atm2atN  36473  elpaddatriN  36491  paddasslem9  36516  paddass  36526  padd12N  36527  paddssw2  36532  paddss  36533  pmodlem2  36535  pmodN  36538  pmapjlln1  36543  atmod1i1  36545  atmod1i2  36547  pexmidlem2N  36659  pexmidlem6N  36663  pl42N  36671  lhpm0atN  36717  lautlt  36779  lautcvr  36780  lautj  36781  lautm  36782  ltrneq2  36836  cdlemc3  36881  cdlemc4  36882  cdlemd1  36886  cdleme1b  36914  cdleme1  36915  cdleme2  36916  cdleme3e  36920  cdlemefr27cl  37091  cdlemefs27cl  37101  cdleme42mN  37175  cdlemftr2  37254  trljco  37428  tgrpgrplem  37437  tendoplass  37471  tendodi1  37472  tendodi2  37473  cdlemk36  37601  erngdvlem3  37678  erngdvlem3-rN  37686  tendospdi1  37708  dvalveclem  37713  dialss  37734  dvhvaddass  37785  dvhopvsca  37790  dvhlveclem  37796  diblss  37858  diclss  37881  dihmeetlem12N  38006  dihmeetlem15N  38009  dihmeetlem16N  38010  dihmeetlem17N  38011  dihmeetlem18N  38012  dihmeetlem19N  38013  dvh4dimN  38135  lpolvN  38174  lclkr  38221  lclkrs  38227  lcfr  38273  irrapxlem6  38930  jm2.26lem3  39104  dgrsub2  39241  mpaadgr  39260  mendring  39298  mendlmod  39299  mendassa  39300  relexpmulg  39561  iunrelexpmin2  39563  relexpxpmin  39568  neicvgel1  39975  fmuldfeq  41427  stoweidlem43  41892  stoweidlem52  41901  stoweidlem53  41902  stoweidlem56  41905  stoweidlem57  41906  issmfle  42586  issmfgt  42597  issmfge  42610  fmtnoprmfac1  43231  fmtnoprmfac2  43233  upgrwlkupwlk  43519  copissgrp  43579  cznrng  43726  funcringcsetcALTV2lem9  43815  funcringcsetclem9ALTV  43838  ply1ass23l  43938  linccl  43971  lincext1  44011  lincext3  44013  lincresunit2  44035  line  44222  rrxline  44224  itsclc0yqsol  44254