Theorem simpr3 1197

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

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1191	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:  simpr13  1260  simpr23  1263  simpr33  1266  simp1r3  1272  simp2r3  1278  simp3r3  1284  3anandis  1473  funopsn  7082  fpr2g  7147  isopolem  7282  fr3nr  7708  sexp3  8086  suppfnss  8122  naddass  8614  dif1en  9075  elfir  9305  intrnfi  9306  fisupcl  9360  cnfcomlem  9595  ttrclss  9616  dmttrcl  9617  rnttrcl  9618  ttrclselem2  9622  ackbij1lem15  10127  pwfseqlem4a  10555  pwfseqlem4  10556  eluzuzle  12744  xlesubadd  13165  elioc2  13312  elico2  13313  elicc2  13314  fseq1p1m1  13501  ccatswrd  14575  pfxccat3a  14644  2cshw  14719  tanadd  16076  dvds2ln  16200  prmgaplem5  16967  prmgaplem8  16970  cshwsidrepsw  17005  ressress  17158  f1ovscpbl  17430  mreexexlem4d  17553  mreexexd  17554  2oppccomf  17631  fthmon  17836  fuccocl  17874  fucidcl  17875  invfuc  17884  initoeu2lem1  17921  curf2cl  18137  yonedalem4c  18183  yonedalem3  18186  pospo  18249  latjle12  18356  latjlej1  18359  latnlej2  18365  latlem12  18372  latmlem1  18375  latledi  18383  latjass  18389  latj12  18390  latj32  18391  latj13  18392  latj31  18393  latjrot  18394  latjjdi  18397  latjjdir  18398  latdisdlem  18402  prdssgrpd  18607  prdsmndd  18644  imasmnd2  18648  imasmnd  18649  frmdmnd  18733  grpsubadd  18907  grpaddsubass  18909  grpsubsub4  18912  grppnpcan2  18913  grpnpncan  18914  grpnnncan2  18916  imasgrp2  18934  imasgrp  18935  mulgnndir  18982  mulgnn0dir  18983  mulgnnass  18988  mulgnn0ass  18989  mulgass  18990  pwsmulg  18998  issubg2  19020  qusgrp  19065  kerf1ghm  19126  galcan  19183  gacan  19184  oppgmnd  19233  pmtrprfv  19332  pmtr3ncom  19354  psgnunilem3  19375  frgp0  19639  cmn32  19679  cmn12  19681  abladdsub  19691  ablsubaddsub  19693  ablsubsub23  19703  mulgdi  19705  mulgsubdi  19708  dprdss  19910  dprdf1o  19913  dprdsn  19917  dmdprdsplit  19928  pgpfac1lem5  19960  omndmul2  20012  prdsrngd  20061  imasrng  20062  srgdilem  20077  ringdilem  20134  ringrng  20170  prdsringd  20206  imasring  20215  opprrng  20230  mulgass3  20238  dvrass  20293  dvrdir  20297  subrgunit  20475  issubrg2  20477  isdomn4  20601  abvdiv  20714  lss1  20841  lsssn0  20851  islss3  20862  prdslmodd  20872  islmhm2  20942  lspsolv  21050  lbsextlem4  21068  sralmod  21091  rnglidl1  21139  ipdi  21547  ipsubdir  21549  ipsubdi  21550  ipassr  21553  ipassr2  21554  isphld  21561  ocvlss  21579  sraassab  21775  sraassaOLD  21777  psrgrpOLD  21864  psrlmod  21867  psrring  21877  psrassa  21880  mpllsslem  21907  mamudm  22280  matring  22328  matassa  22329  ofco2  22336  scmatlss  22410  ma1repveval  22456  mdetunilem1  22497  mdetunilem9  22505  monmatcollpw  22664  iinopn  22787  restopnb  23060  subbascn  23139  hausnei2  23238  nrmsep2  23241  isnrm3  23244  t1sep  23255  regsep2  23261  dnsconst  23263  dfconn2  23304  dislly  23382  tx1stc  23535  qtophmeo  23702  filss  23738  infil  23748  fsubbas  23752  filssufilg  23796  hauspwpwf1  23872  cnextcn  23952  tmdcn2  23974  psmettri  24197  isxmet2d  24213  xmettri  24237  xmetres2  24247  bldisj  24284  blss2ps  24289  blss2  24290  xmstri2  24352  mstri2  24353  xmstri  24354  mstri  24355  xmstri3  24356  mstri3  24357  msrtri  24358  comet  24399  met2ndci  24408  ngprcan  24496  ngplcan  24497  ngpsubcan  24500  nmtri2  24513  nrgdsdi  24551  nrgdsdir  24552  nlmdsdi  24567  nlmdsdir  24568  blcvx  24684  iocopnst  24835  icccvx  24846  pi1grplem  24947  pi1xfrf  24951  pi1cof  24957  clmpm1dir  25001  cmodscmulexp  25020  cvsdiv  25030  cvsdivcl  25031  cphdivcl  25080  cphsubdir  25106  cphsubdi  25107  bcthlem5  25226  rrxcph  25290  volfiniun  25446  volcn  25505  itg1val2  25583  dvconst  25816  dvlip  25896  ftc1a  25942  ulmdvlem3  26309  ang180  26722  cvxcl  26893  scvxcvx  26894  sgmmul  27110  logexprlim  27134  dchrabl  27163  nosupbnd1  27624  noinfbnd1lem5  27637  noinfbnd1  27639  ssltsep  27701  addscom  27878  addsbday  27929  addsdi  28063  mulsass  28074  motgrp  28488  iscgra1  28755  cgrane2  28758  cgrane4  28760  cgrahl1  28761  cgrahl2  28762  cgracgr  28763  cgratr  28768  cgrabtwn  28771  cgrahl  28772  dfcgra2  28775  sacgr  28776  f1otrge  28817  xmstrkgc  28831  colinearalglem1  28851  colinearalg  28855  axcgrtr  28860  axlowdimlem16  28902  axeuclidlem  28907  axcontlem4  28912  axcontlem7  28915  axcontlem12  28920  eengtrkg  28931  eengtrkge  28932  edglnl  29088  subgruhgredgd  29229  nbfusgrlevtxm2  29323  upgrwlkdvde  29682  crctcshwlkn0lem5  29759  crctcshwlkn0  29766  umgrwwlks2on  29902  rusgrnumwwlks  29919  clwlkclwwlkfo  29953  3spthd  30120  frgr2wwlkeqm  30275  dlwwlknondlwlknonf1o  30309  numclwwlk5  30332  friendship  30343  grpomuldivass  30485  ablodivdiv4  30498  dipdi  30787  dipsubdi  30793  disjdsct  32646  archiabllem2c  33138  dvrcan5  33177  rloccring  33211  reofld  33282  eqgvscpbl  33288  qusvsval  33290  quslmod  33296  quslmhm  33297  prmidlc  33386  ssdifidl  33395  ssmxidl  33412  ply1degltlss  33530  r1plmhm  33543  drgextlsp  33566  ccfldsrarelvec  33644  constrconj  33718  constrfin  33719  constrelextdg2  33720  pstmfval  33869  qqhval2lem  33954  qqhvq  33960  esumcvg  34059  sigaclcu  34090  measdivcst  34197  measdivcstALTV  34198  carsggect  34292  tgoldbachgtd  34636  bnj970  34920  bnj910  34921  erdszelem9  35182  cvmseu  35259  elmrsubrn  35503  r1peuqusdeg1  35626  cgrid2  35987  btwncomim  35997  btwnswapid  36001  trisegint  36012  cgrxfr  36039  btwnxfr  36040  brofs2  36061  brifs2  36062  endofsegid  36069  btwnconn1lem11  36081  btwnconn2  36086  segcon2  36089  seglemin  36097  segletr  36098  btwnsegle  36101  colinbtwnle  36102  broutsideof2  36106  btwnoutside  36109  broutsideof3  36110  outsideoftr  36113  outsidele  36116  ellines  36136  linethrueu  36140  weiunpo  36449  unbdqndv2  36495  poimirlem28  37638  ftc1anc  37691  sdclem1  37733  sstotbnd2  37764  ismndo1  37863  zerdivemp1x  37937  isdrngo2  37948  iscringd  37988  lsmsat  38997  lfladdcl  39060  lflnegcl  39064  lflvscl  39066  lshpkrlem4  39102  lshpkrlem6  39104  ldualgrplem  39134  lduallmodlem  39141  latmassOLD  39218  latm12  39219  latm32  39220  latmrot  39221  latmmdiN  39223  latmmdir  39224  omlfh1N  39247  omlfh3N  39248  cvrnbtwn2  39264  cvlexchb1  39319  cvlexch3  39321  cvlexch4N  39322  cvlatexchb1  39323  cvlsupr2  39332  hlatjass  39359  hlatj12  39360  hlatj32  39361  cvrat  39411  atcvrj0  39417  cvrat2  39418  atltcvr  39424  atexchltN  39430  cvrat3  39431  cvrat4  39432  atbtwnexOLDN  39436  atbtwnex  39437  3dimlem3  39450  3dimlem3OLDN  39451  3at  39479  2atneat  39504  llncmp  39511  2at0mat0  39514  2atmat0  39515  islpln2a  39537  llncvrlpln  39547  lplncmp  39551  3atnelvolN  39575  4atlem11  39598  lplncvrlvol  39605  lvolcmp  39606  2atm2atN  39774  elpaddatriN  39792  elpadd2at2  39796  paddasslem8  39816  paddasslem17  39825  paddass  39827  padd12N  39828  paddssw1  39832  pmodlem2  39836  pmodN  39839  pmapjlln1  39844  atmod1i2  39848  pexmidlem2N  39960  pexmidlem7N  39965  pl42lem2N  39969  pl42lem3N  39970  pl42lem4N  39971  pl42N  39972  lhp2lt  39990  lhpm0atN  40018  lautlt  40080  lautcvr  40081  lautj  40082  lautm  40083  ltrneq2  40137  cdleme1b  40215  cdleme3b  40218  cdleme3c  40219  cdleme9b  40241  cdlemefs27cl  40402  cdleme42mN  40476  cdlemg4c  40601  trljco  40729  tgrpgrplem  40738  tendoplass  40772  tendodi1  40773  tendodi2  40774  erngplus2  40793  erngplus2-rN  40801  cdlemk36  40902  erngdvlem3  40979  erngdvlem3-rN  40987  dvaplusgv  40999  tendospass  41008  tendospdi1  41009  dvalveclem  41014  dialss  41035  dvhvaddass  41086  dvhopvsca  41091  dvhlveclem  41097  diblss  41159  diclss  41182  diclspsn  41183  cdlemn11pre  41199  dihmeetlem12N  41307  dihmeetlem16N  41311  dihmeetlem17N  41312  dvh4dimN  41436  lpolsatN  41477  lpolpolsatN  41478  dochpolN  41479  lclkr  41522  lclkrs  41528  lcfr  41574  lcmineqlem13  42024  aks6d1c1  42099  irrapxlem6  42810  jm2.26lem3  42984  mpaamn  43139  mendring  43171  mendlmod  43172  mendassa  43173  nnoeomeqom  43295  omabs2  43315  neicvgel1  44102  rfcnpre4  45022  fmuldfeq  45574  stoweidlem43  46034  stoweidlem52  46043  stoweidlem53  46044  stoweidlem56  46047  issmfgt  46747  issmfge  46761  iccelpart  47427  prproropf1olem1  47497  fmtnoprmfac1  47559  fmtnoprmfac2  47561  isubgr3stgrlem2  47961  isubgr3stgrlem4  47963  grlimgrtrilem1  47995  copissgrp  48162  cznrng  48255  funcringcsetcALTV2lem9  48292  funcringcsetclem9ALTV  48315  linccl  48409  lincsumscmcl  48428  ldepsprlem  48467  lincresunit3lem1  48474  itsclc0yqe  48756  resipos  48969  topdlat  48998  catprs  49006  endmndlem  49010  idmon  49015  idepi  49016  thincmon  49428  thincepi  49429  functhinclem1  49439  grptcmon  49588  grptcepi  49589