Theorem simpr1 1194

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 486	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2antr1 1188	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  simpr11  1257  simpr21  1260  simpr31  1263  simp1r1  1269  simp2r1  1275  simp3r1  1281  3anandis  1471  fpr2g  7119  isopolem  7248  fr3nr  7654  suppfnss  8036  frrlem4  8136  frrlem8  8140  frfi  9103  intrnfi  9219  iinfi  9220  eqsup  9259  fisupcl  9272  cnfcomlem  9501  ttrclss  9522  ackbij1lem15  10036  fpwwe2lem4  10436  dedekindle  11185  ico0  13171  elioc2  13188  elico2  13189  elicc2  13190  iccsplit  13263  fseq1p1m1  13376  elfz0ubfz0  13406  hashtpg  14244  swrdsbslen  14422  ccatswrd  14426  wwlktovf1  14717  tanadd  15921  dvds2ln  16043  qredeq  16407  ressress  17003  mreexexlem4d  17401  mreexexd  17402  0catg  17442  2oppccomf  17481  issubc3  17609  fthmon  17688  fuccocl  17727  fucidcl  17728  invfuc  17737  initoeu2lem0  17773  initoeu2lem1  17774  curf2cl  17994  yonedalem4c  18040  yonedalem3  18043  pospo  18108  latjle12  18213  latjlej1  18216  latnlej2  18222  latlem12  18229  latmlem1  18232  latledi  18240  latmlej11  18241  latjass  18246  latj12  18247  latj32  18248  latj13  18249  latj31  18250  latjrot  18251  latjjdi  18254  latjjdir  18255  latdisdlem  18259  prdsmndd  18463  imasmnd2  18467  mndissubm  18491  frmdmnd  18543  grpsubrcan  18701  grpsubadd  18708  grpsubsub  18709  grpaddsubass  18710  grpsubsub4  18713  grpnnncan2  18717  imasgrp2  18735  mulgnndir  18777  mulgnn0dir  18778  mulgdir  18780  mulgnnass  18783  mulgnn0ass  18784  mulgass  18785  mulgsubdir  18788  pwsmulg  18793  issubg2  18815  eqgval  18850  qusgrp  18856  galcan  18955  gacan  18956  oppgmnd  19006  pmtrprfv  19106  pmtr3ncom  19128  psgnunilem3  19149  cmn32  19450  cmn12  19452  abladdsub  19461  mulgnn0di  19472  mulgdi  19473  mulgsubdi  19476  dprdss  19677  dprdz  19678  dprdf1o  19680  dprdsn  19684  dprd2da  19690  ablfac1b  19718  pgpfac1lem5  19727  srgbinomlem2  19822  srgbinom  19826  ringi  19844  prdsringd  19896  imasring  19903  opprring  19918  mulgass3  19924  dvrass  19977  kerf1ghm  20032  subrgunit  20087  issubrg2  20089  abvdiv  20142  islss3  20266  prdslmodd  20276  islmhm2  20345  lspsolv  20450  islbs2  20461  islbs3  20462  lbsextlem4  20468  sralmod  20502  ipdir  20889  ipdi  20890  ipsubdir  20892  ipsubdi  20893  ipass  20895  ipassr  20896  ipassr2  20897  ocvlss  20922  sraassa  21119  psrbagleclOLD  21175  psrbagconOLD  21179  psrgrp  21212  psrlmod  21215  psrring  21225  psrassa  21228  mamudm  21582  matring  21637  matassa  21638  ofco2  21645  mdetunilem1  21806  mdetunilem9  21814  mdetuni0  21815  mdetmul  21817  gsummatr01lem3  21851  iinopn  22096  subbascn  22450  nrmsep2  22552  isnrm3  22555  regsep2  22572  dnsconst  22574  dfconn2  22615  1stcelcls  22657  nllyidm  22685  dislly  22693  upxp  22819  fbasne0  23026  filss  23049  infil  23059  fsubbas  23063  filssufilg  23107  tmdcn2  23285  psmettri  23509  isxmet2d  23525  xmettri  23549  xmetres2  23559  bldisj  23596  blss2ps  23601  blss2  23602  xmstri2  23664  mstri2  23665  xmstri  23666  mstri  23667  xmstri3  23668  mstri3  23669  msrtri  23670  comet  23714  stdbdbl  23718  met2ndci  23723  ngprcan  23811  ngplcan  23812  ngpsubcan  23815  nmtri2  23828  nrgdsdi  23874  nrgdsdir  23875  nlmdsdi  23890  nlmdsdir  23891  blcvx  24006  icccmplem2  24031  pi1grplem  24257  pi1cof  24267  clmpm1dir  24311  cvsdiv  24340  cvsdivcl  24341  cphdivcl  24391  cphsubdir  24417  cphsubdi  24418  cphassr  24421  bcthlem5  24537  rrxcph  24601  volfiniun  24756  volcn  24815  itg1val2  24893  dvconst  25126  dvlip  25202  dvfsumlem4  25238  ftc1a  25246  ulmval  25584  ulmdvlem3  25606  ang180  26009  cvxcl  26179  scvxcvx  26180  sgmmul  26394  logexprlim  26418  dchrabl  26447  motgrp  26949  iscgra1  27216  cgrane1  27218  cgrane2  27219  cgrahl1  27222  cgrahl2  27223  cgracgr  27224  cgratr  27229  cgrabtwn  27232  dfcgra2  27236  sacgr  27237  f1otrge  27278  colinearalglem1  27319  colinearalg  27323  axcgrtr  27328  axlowdimlem16  27370  axeuclidlem  27375  axcontlem7  27383  eengtrkg  27399  eengtrkge  27400  nbfusgrlevtxm2  27790  lfgriswlk  28101  upgrwlkdvde  28150  wwlknbp1  28254  erclwwlktr  28431  erclwwlkntr  28480  frgr2wwlkeqm  28740  numclwwlk1lem2f  28764  numclwwlk5  28797  friendship  28808  grpodivdiv  28947  grpomuldivass  28948  ablodivdiv4  28961  ablonnncan1  28964  nvmdi  29055  dipassr  29253  archiabllem2c  31494  dvrdir  31532  dvrcan5  31535  reofld  31589  eqgvscpbl  31595  qusscaval  31597  quslmod  31599  quslmhm  31600  prmidlc  31669  ssmxidl  31687  drgextlsp  31726  ccfldsrarelvec  31786  pstmfval  31891  tpr2rico  31907  qqhval2lem  31976  qqhvq  31982  issiga  32125  measdivcst  32237  measdivcstALTV  32238  carsggect  32330  signsply0  32575  tgoldbachgtd  32687  bnj149  32900  bnj1118  33009  bnj1128  33015  erdszelem9  33206  resconn  33253  cvmseu  33283  cvmlift2lem12  33321  ex-sategoelel  33428  elmrsubrn  33527  mclsind  33577  xpord3pred  33843  sexp3  33844  nosupbnd1  33962  noinfbnd1lem5  33975  noinfbnd1  33977  ssltss1  34028  cgrid2  34350  segconeu  34358  btwncomim  34360  btwnswapid  34364  cgrxfr  34402  btwnxfr  34403  colineardim1  34408  brofs2  34424  brifs2  34425  idinside  34431  endofsegid  34432  btwnconn1lem7  34440  btwnconn1lem11  34444  btwnconn1  34448  segcon2  34452  seglemin  34460  segletr  34461  btwnsegle  34464  colinbtwnle  34465  broutsideof2  34469  broutsideof3  34473  outsidele  34479  fvray  34488  fvline  34491  linerflx1  34496  ellines  34499  ivthALT  34569  poimirlem32  35853  ftc1anc  35902  sdclem1  35945  sstotbnd2  35976  zerdivemp1x  36149  isdrngo2  36160  iscringd  36200  lsmsat  37064  lfladdcl  37127  lflnegcl  37131  lflvscl  37133  lshpkrlem4  37169  lshpkrlem6  37171  ldualgrplem  37201  lduallmodlem  37208  latmassOLD  37285  latm12  37286  latm32  37287  latmrot  37288  latmmdiN  37290  latmmdir  37291  omlfh1N  37314  omlfh3N  37315  cvlexchb1  37386  cvlexch3  37388  cvlexch4N  37389  cvlatexchb1  37390  cvlsupr2  37399  hlatjass  37426  hlatj12  37427  hlatj32  37428  cvratlem  37477  cvrat  37478  atcvrj0  37484  cvrat2  37485  atltcvr  37491  atexchltN  37497  cvrat3  37498  cvrat4  37499  3dimlem3  37517  3dimlem3OLDN  37518  3at  37546  2atneat  37571  llncmp  37578  2at0mat0  37581  2atmat0  37582  lplnnle2at  37597  llncvrlpln  37614  lplncmp  37618  lplnexllnN  37620  2llnjaN  37622  4atlem11  37665  lplncvrlvol  37672  lvolcmp  37673  2atm2atN  37841  elpaddatriN  37859  paddasslem9  37884  paddass  37894  padd12N  37895  paddssw2  37900  paddss  37901  pmodlem2  37903  pmodN  37906  pmapjlln1  37911  atmod1i1  37913  atmod1i2  37915  pexmidlem2N  38027  pexmidlem6N  38031  pl42N  38039  lhpm0atN  38085  lautlt  38147  lautcvr  38148  lautj  38149  lautm  38150  ltrneq2  38204  cdlemc3  38249  cdlemc4  38250  cdlemd1  38254  cdleme1b  38282  cdleme1  38283  cdleme2  38284  cdleme3e  38288  cdlemefr27cl  38459  cdlemefs27cl  38469  cdleme42mN  38543  cdlemftr2  38622  trljco  38796  tgrpgrplem  38805  tendoplass  38839  tendodi1  38840  tendodi2  38841  cdlemk36  38969  erngdvlem3  39046  erngdvlem3-rN  39054  tendospdi1  39076  dvalveclem  39081  dialss  39102  dvhvaddass  39153  dvhopvsca  39158  dvhlveclem  39164  diblss  39226  diclss  39249  dihmeetlem12N  39374  dihmeetlem15N  39377  dihmeetlem16N  39378  dihmeetlem17N  39379  dihmeetlem18N  39380  dihmeetlem19N  39381  dvh4dimN  39503  lpolvN  39542  lclkr  39589  lclkrs  39595  lcfr  39641  irrapxlem6  40686  jm2.26lem3  40861  dgrsub2  40998  mpaadgr  41017  mendring  41055  mendlmod  41056  mendassa  41057  relexpmulg  41356  iunrelexpmin2  41358  relexpxpmin  41363  neicvgel1  41767  fmuldfeq  43173  stoweidlem43  43633  stoweidlem52  43642  stoweidlem53  43643  stoweidlem56  43646  stoweidlem57  43647  issmfle  44333  issmfgt  44344  issmfge  44358  fmtnoprmfac1  45075  fmtnoprmfac2  45077  upgrwlkupwlk  45360  copissgrp  45420  cznrng  45571  funcringcsetcALTV2lem9  45660  funcringcsetclem9ALTV  45683  ply1ass23l  45781  linccl  45813  lincext1  45853  lincext3  45855  lincresunit2  45877  line  46136  rrxline  46138  itsclc0yqsol  46168  topdlat  46348  catprs  46350  endmndlem  46354  idmon  46355  idepi  46356  thincmon  46373  thincepi  46374  grptcmon  46435  grptcepi  46436