Theorem simpr3 1194

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 1188	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simpr13  1257  simpr23  1260  simpr33  1263  simp1r3  1269  simp2r3  1275  simp3r3  1281  3anandis  1469  funopsn  7014  fpr2g  7081  isopolem  7209  fr3nr  7613  suppfnss  7989  elfir  9135  intrnfi  9136  fisupcl  9189  cnfcomlem  9418  ttrclss  9439  dmttrcl  9440  rnttrcl  9441  ttrclselem2  9445  ackbij1lem15  9974  pwfseqlem4a  10401  pwfseqlem4  10402  eluzuzle  12573  xlesubadd  12979  elioc2  13124  elico2  13125  elicc2  13126  fseq1p1m1  13312  ccatswrd  14362  pfxccat3a  14432  2cshw  14507  tanadd  15857  dvds2ln  15979  prmgaplem5  16737  prmgaplem8  16740  cshwsidrepsw  16776  ressress  16939  f1ovscpbl  17218  mreexexlem4d  17337  mreexexd  17338  2oppccomf  17417  fthmon  17624  fuccocl  17663  fucidcl  17664  invfuc  17673  initoeu2lem1  17710  curf2cl  17930  yonedalem4c  17976  yonedalem3  17979  pospo  18044  latjle12  18149  latjlej1  18152  latnlej2  18158  latlem12  18165  latmlem1  18168  latledi  18176  latjass  18182  latj12  18183  latj32  18184  latj13  18185  latj31  18186  latjrot  18187  latjjdi  18190  latjjdir  18191  latdisdlem  18195  prdsmndd  18399  imasmnd2  18403  imasmnd  18404  frmdmnd  18479  grpsubadd  18644  grpaddsubass  18646  grpsubsub4  18649  grppnpcan2  18650  grpnpncan  18651  grpnnncan2  18653  imasgrp2  18671  imasgrp  18672  mulgnndir  18713  mulgnn0dir  18714  mulgnnass  18719  mulgnn0ass  18720  mulgass  18721  pwsmulg  18729  issubg2  18751  qusgrp  18792  galcan  18891  gacan  18892  oppgmnd  18942  pmtrprfv  19042  pmtr3ncom  19064  psgnunilem3  19085  frgp0  19347  cmn32  19386  cmn12  19388  abladdsub  19397  ablsubsub23  19407  mulgdi  19409  mulgsubdi  19412  dprdss  19613  dprdf1o  19616  dprdsn  19620  dmdprdsplit  19631  pgpfac1lem5  19663  srgi  19728  ringi  19780  prdsringd  19832  imasring  19839  opprring  19854  mulgass3  19860  dvrass  19913  kerf1ghm  19968  subrgunit  20023  issubrg2  20025  abvdiv  20078  lss1  20181  lsssn0  20190  islss3  20202  prdslmodd  20212  islmhm2  20281  lspsolv  20386  lbsextlem4  20404  sralmod  20438  ipdi  20826  ipsubdir  20828  ipsubdi  20829  ipassr  20832  ipassr2  20833  isphld  20840  ocvlss  20858  sraassa  21055  psrbaglesuppOLD  21109  psrbagconOLD  21115  psrgrp  21148  psrlmod  21151  psrring  21161  psrassa  21164  mpllsslem  21187  mamudm  21518  matring  21573  matassa  21574  ofco2  21581  scmatlss  21655  ma1repveval  21701  mdetunilem1  21742  mdetunilem9  21750  monmatcollpw  21909  iinopn  22032  restopnb  22307  subbascn  22386  hausnei2  22485  nrmsep2  22488  isnrm3  22491  t1sep  22502  regsep2  22508  dnsconst  22510  dfconn2  22551  dislly  22629  tx1stc  22782  qtophmeo  22949  filss  22985  infil  22995  fsubbas  22999  filssufilg  23043  hauspwpwf1  23119  cnextcn  23199  tmdcn2  23221  psmettri  23445  isxmet2d  23461  xmettri  23485  xmetres2  23495  bldisj  23532  blss2ps  23537  blss2  23538  xmstri2  23600  mstri2  23601  xmstri  23602  mstri  23603  xmstri3  23604  mstri3  23605  msrtri  23606  comet  23650  met2ndci  23659  ngprcan  23747  ngplcan  23748  ngpsubcan  23751  nmtri2  23764  nrgdsdi  23810  nrgdsdir  23811  nlmdsdi  23826  nlmdsdir  23827  blcvx  23942  iocopnst  24084  icccvx  24094  pi1grplem  24193  pi1xfrf  24197  pi1cof  24203  clmpm1dir  24247  cmodscmulexp  24266  cvsdiv  24276  cvsdivcl  24277  cphdivcl  24327  cphsubdir  24353  cphsubdi  24354  bcthlem5  24473  rrxcph  24537  volfiniun  24692  volcn  24751  itg1val2  24829  dvconst  25062  dvlip  25138  ftc1a  25182  ulmdvlem3  25542  ang180  25945  cvxcl  26115  scvxcvx  26116  sgmmul  26330  logexprlim  26354  dchrabl  26383  motgrp  26885  iscgra1  27152  cgrane2  27155  cgrane4  27157  cgrahl1  27158  cgrahl2  27159  cgracgr  27160  cgratr  27165  cgrabtwn  27168  cgrahl  27169  dfcgra2  27172  sacgr  27173  f1otrge  27214  xmstrkgc  27234  colinearalglem1  27255  colinearalg  27259  axcgrtr  27264  axlowdimlem16  27306  axeuclidlem  27311  axcontlem4  27316  axcontlem7  27319  axcontlem12  27324  eengtrkg  27335  eengtrkge  27336  edglnl  27494  subgruhgredgd  27632  nbfusgrlevtxm2  27726  upgrwlkdvde  28084  crctcshwlkn0lem5  28158  crctcshwlkn0  28165  umgrwwlks2on  28301  rusgrnumwwlks  28318  clwlkclwwlkfo  28352  3spthd  28519  frgr2wwlkeqm  28674  dlwwlknondlwlknonf1o  28708  numclwwlk5  28731  friendship  28742  grpomuldivass  28882  ablodivdiv4  28895  dipdi  29184  dipsubdi  29190  disjdsct  31014  omndmul2  31317  archiabllem2c  31428  dvrdir  31466  dvrcan5  31469  reofld  31523  eqgvscpbl  31529  qusscaval  31531  quslmod  31533  quslmhm  31534  prmidlc  31603  ssmxidl  31621  drgextlsp  31660  ccfldsrarelvec  31720  pstmfval  31825  qqhval2lem  31910  qqhvq  31916  esumcvg  32033  sigaclcu  32064  measdivcst  32171  measdivcstALTV  32172  carsggect  32264  tgoldbachgtd  32621  bnj970  32906  bnj910  32907  erdszelem9  33140  cvmseu  33217  elmrsubrn  33461  xpord3pred  33777  sexp3  33778  nosupbnd1  33896  noinfbnd1lem5  33909  noinfbnd1  33911  ssltsep  33964  addscom  34108  cgrid2  34284  btwncomim  34294  btwnswapid  34298  trisegint  34309  cgrxfr  34336  btwnxfr  34337  brofs2  34358  brifs2  34359  endofsegid  34366  btwnconn1lem11  34378  btwnconn2  34383  segcon2  34386  seglemin  34394  segletr  34395  btwnsegle  34398  colinbtwnle  34399  broutsideof2  34403  btwnoutside  34406  broutsideof3  34407  outsideoftr  34410  outsidele  34413  ellines  34433  linethrueu  34437  unbdqndv2  34670  poimirlem28  35784  ftc1anc  35837  sdclem1  35880  sstotbnd2  35911  ismndo1  36010  zerdivemp1x  36084  isdrngo2  36095  iscringd  36135  lsmsat  37001  lfladdcl  37064  lflnegcl  37068  lflvscl  37070  lshpkrlem4  37106  lshpkrlem6  37108  ldualgrplem  37138  lduallmodlem  37145  latmassOLD  37222  latm12  37223  latm32  37224  latmrot  37225  latmmdiN  37227  latmmdir  37228  omlfh1N  37251  omlfh3N  37252  cvrnbtwn2  37268  cvlexchb1  37323  cvlexch3  37325  cvlexch4N  37326  cvlatexchb1  37327  cvlsupr2  37336  hlatjass  37363  hlatj12  37364  hlatj32  37365  cvrat  37415  atcvrj0  37421  cvrat2  37422  atltcvr  37428  atexchltN  37434  cvrat3  37435  cvrat4  37436  atbtwnexOLDN  37440  atbtwnex  37441  3dimlem3  37454  3dimlem3OLDN  37455  3at  37483  2atneat  37508  llncmp  37515  2at0mat0  37518  2atmat0  37519  islpln2a  37541  llncvrlpln  37551  lplncmp  37555  3atnelvolN  37579  4atlem11  37602  lplncvrlvol  37609  lvolcmp  37610  2atm2atN  37778  elpaddatriN  37796  elpadd2at2  37800  paddasslem8  37820  paddasslem17  37829  paddass  37831  padd12N  37832  paddssw1  37836  pmodlem2  37840  pmodN  37843  pmapjlln1  37848  atmod1i2  37852  pexmidlem2N  37964  pexmidlem7N  37969  pl42lem2N  37973  pl42lem3N  37974  pl42lem4N  37975  pl42N  37976  lhp2lt  37994  lhpm0atN  38022  lautlt  38084  lautcvr  38085  lautj  38086  lautm  38087  ltrneq2  38141  cdleme1b  38219  cdleme3b  38222  cdleme3c  38223  cdleme9b  38245  cdlemefs27cl  38406  cdleme42mN  38480  cdlemg4c  38605  trljco  38733  tgrpgrplem  38742  tendoplass  38776  tendodi1  38777  tendodi2  38778  erngplus2  38797  erngplus2-rN  38805  cdlemk36  38906  erngdvlem3  38983  erngdvlem3-rN  38991  dvaplusgv  39003  tendospass  39012  tendospdi1  39013  dvalveclem  39018  dialss  39039  dvhvaddass  39090  dvhopvsca  39095  dvhlveclem  39101  diblss  39163  diclss  39186  diclspsn  39187  cdlemn11pre  39203  dihmeetlem12N  39311  dihmeetlem16N  39315  dihmeetlem17N  39316  dvh4dimN  39440  lpolsatN  39481  lpolpolsatN  39482  dochpolN  39483  lclkr  39526  lclkrs  39532  lcfr  39578  lcmineqlem13  40029  isdomn4  40152  irrapxlem6  40629  jm2.26lem3  40803  mpaamn  40961  mendring  40997  mendlmod  40998  mendassa  40999  neicvgel1  41682  rfcnpre4  42530  fmuldfeq  43078  stoweidlem43  43538  stoweidlem52  43547  stoweidlem53  43548  stoweidlem56  43551  issmfgt  44243  issmfge  44256  iccelpart  44837  prproropf1olem1  44907  fmtnoprmfac1  44969  fmtnoprmfac2  44971  copissgrp  45314  ringrng  45389  cznrng  45465  funcringcsetcALTV2lem9  45554  funcringcsetclem9ALTV  45577  linccl  45707  lincsumscmcl  45726  ldepsprlem  45765  lincresunit3lem1  45772  itsclc0yqe  46059  topdlat  46242  catprs  46244  endmndlem  46248  idmon  46249  idepi  46250  thincmon  46267  thincepi  46268  functhinclem1  46274  grptcmon  46329  grptcepi  46330