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  7120  fpr2g  7185  isopolem  7320  fr3nr  7748  sexp3  8132  suppfnss  8168  naddass  8660  dif1en  9124  elfir  9366  intrnfi  9367  fisupcl  9421  cnfcomlem  9652  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  ackbij1lem15  10186  pwfseqlem4a  10614  pwfseqlem4  10615  eluzuzle  12802  xlesubadd  13223  elioc2  13370  elico2  13371  elicc2  13372  fseq1p1m1  13559  ccatswrd  14633  pfxccat3a  14703  2cshw  14778  tanadd  16135  dvds2ln  16259  prmgaplem5  17026  prmgaplem8  17029  cshwsidrepsw  17064  ressress  17217  f1ovscpbl  17489  mreexexlem4d  17608  mreexexd  17609  2oppccomf  17686  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  initoeu2lem1  17976  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  pospo  18304  latjle12  18409  latjlej1  18412  latnlej2  18418  latlem12  18425  latmlem1  18428  latledi  18436  latjass  18442  latj12  18443  latj32  18444  latj13  18445  latj31  18446  latjrot  18447  latjjdi  18450  latjjdir  18451  latdisdlem  18455  prdssgrpd  18660  prdsmndd  18697  imasmnd2  18701  imasmnd  18702  frmdmnd  18786  grpsubadd  18960  grpaddsubass  18962  grpsubsub4  18965  grppnpcan2  18966  grpnpncan  18967  grpnnncan2  18969  imasgrp2  18987  imasgrp  18988  mulgnndir  19035  mulgnn0dir  19036  mulgnnass  19041  mulgnn0ass  19042  mulgass  19043  pwsmulg  19051  issubg2  19073  qusgrp  19118  kerf1ghm  19179  galcan  19236  gacan  19237  oppgmnd  19286  pmtrprfv  19383  pmtr3ncom  19405  psgnunilem3  19426  frgp0  19690  cmn32  19730  cmn12  19732  abladdsub  19742  ablsubaddsub  19744  ablsubsub23  19754  mulgdi  19756  mulgsubdi  19759  dprdss  19961  dprdf1o  19964  dprdsn  19968  dmdprdsplit  19979  pgpfac1lem5  20011  prdsrngd  20085  imasrng  20086  srgdilem  20101  ringdilem  20158  ringrng  20194  prdsringd  20230  imasring  20239  opprrng  20254  mulgass3  20262  dvrass  20317  dvrdir  20321  subrgunit  20499  issubrg2  20501  isdomn4  20625  abvdiv  20738  lss1  20844  lsssn0  20854  islss3  20865  prdslmodd  20875  islmhm2  20945  lspsolv  21053  lbsextlem4  21071  sralmod  21094  rnglidl1  21142  ipdi  21549  ipsubdir  21551  ipsubdi  21552  ipassr  21555  ipassr2  21556  isphld  21563  ocvlss  21581  sraassab  21777  sraassaOLD  21779  psrgrpOLD  21866  psrlmod  21869  psrring  21879  psrassa  21882  mpllsslem  21909  mamudm  22282  matring  22330  matassa  22331  ofco2  22338  scmatlss  22412  ma1repveval  22458  mdetunilem1  22499  mdetunilem9  22507  monmatcollpw  22666  iinopn  22789  restopnb  23062  subbascn  23141  hausnei2  23240  nrmsep2  23243  isnrm3  23246  t1sep  23257  regsep2  23263  dnsconst  23265  dfconn2  23306  dislly  23384  tx1stc  23537  qtophmeo  23704  filss  23740  infil  23750  fsubbas  23754  filssufilg  23798  hauspwpwf1  23874  cnextcn  23954  tmdcn2  23976  psmettri  24199  isxmet2d  24215  xmettri  24239  xmetres2  24249  bldisj  24286  blss2ps  24291  blss2  24292  xmstri2  24354  mstri2  24355  xmstri  24356  mstri  24357  xmstri3  24358  mstri3  24359  msrtri  24360  comet  24401  met2ndci  24410  ngprcan  24498  ngplcan  24499  ngpsubcan  24502  nmtri2  24515  nrgdsdi  24553  nrgdsdir  24554  nlmdsdi  24569  nlmdsdir  24570  blcvx  24686  iocopnst  24837  icccvx  24848  pi1grplem  24949  pi1xfrf  24953  pi1cof  24959  clmpm1dir  25003  cmodscmulexp  25022  cvsdiv  25032  cvsdivcl  25033  cphdivcl  25082  cphsubdir  25108  cphsubdi  25109  bcthlem5  25228  rrxcph  25292  volfiniun  25448  volcn  25507  itg1val2  25585  dvconst  25818  dvlip  25898  ftc1a  25944  ulmdvlem3  26311  ang180  26724  cvxcl  26895  scvxcvx  26896  sgmmul  27112  logexprlim  27136  dchrabl  27165  nosupbnd1  27626  noinfbnd1lem5  27639  noinfbnd1  27641  ssltsep  27702  addscom  27873  addsbday  27924  addsdi  28058  mulsass  28069  motgrp  28470  iscgra1  28737  cgrane2  28740  cgrane4  28742  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgratr  28750  cgrabtwn  28753  cgrahl  28754  dfcgra2  28757  sacgr  28758  f1otrge  28799  xmstrkgc  28813  colinearalglem1  28833  colinearalg  28837  axcgrtr  28842  axlowdimlem16  28884  axeuclidlem  28889  axcontlem4  28894  axcontlem7  28897  axcontlem12  28902  eengtrkg  28913  eengtrkge  28914  edglnl  29070  subgruhgredgd  29211  nbfusgrlevtxm2  29305  upgrwlkdvde  29667  crctcshwlkn0lem5  29744  crctcshwlkn0  29751  umgrwwlks2on  29887  rusgrnumwwlks  29904  clwlkclwwlkfo  29938  3spthd  30105  frgr2wwlkeqm  30260  dlwwlknondlwlknonf1o  30294  numclwwlk5  30317  friendship  30328  grpomuldivass  30470  ablodivdiv4  30483  dipdi  30772  dipsubdi  30778  disjdsct  32626  omndmul2  33026  archiabllem2c  33149  dvrcan5  33187  rloccring  33221  reofld  33315  eqgvscpbl  33321  qusvsval  33323  quslmod  33329  quslmhm  33330  prmidlc  33419  ssdifidl  33428  ssmxidl  33445  ply1degltlss  33562  r1plmhm  33575  drgextlsp  33589  ccfldsrarelvec  33666  constrconj  33735  constrfin  33736  constrelextdg2  33737  pstmfval  33886  qqhval2lem  33971  qqhvq  33977  esumcvg  34076  sigaclcu  34107  measdivcst  34214  measdivcstALTV  34215  carsggect  34309  tgoldbachgtd  34653  bnj970  34937  bnj910  34938  erdszelem9  35186  cvmseu  35263  elmrsubrn  35507  r1peuqusdeg1  35630  cgrid2  35991  btwncomim  36001  btwnswapid  36005  trisegint  36016  cgrxfr  36043  btwnxfr  36044  brofs2  36065  brifs2  36066  endofsegid  36073  btwnconn1lem11  36085  btwnconn2  36090  segcon2  36093  seglemin  36101  segletr  36102  btwnsegle  36105  colinbtwnle  36106  broutsideof2  36110  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  outsidele  36120  ellines  36140  linethrueu  36144  weiunpo  36453  unbdqndv2  36499  poimirlem28  37642  ftc1anc  37695  sdclem1  37737  sstotbnd2  37768  ismndo1  37867  zerdivemp1x  37941  isdrngo2  37952  iscringd  37992  lsmsat  39001  lfladdcl  39064  lflnegcl  39068  lflvscl  39070  lshpkrlem4  39106  lshpkrlem6  39108  ldualgrplem  39138  lduallmodlem  39145  latmassOLD  39222  latm12  39223  latm32  39224  latmrot  39225  latmmdiN  39227  latmmdir  39228  omlfh1N  39251  omlfh3N  39252  cvrnbtwn2  39268  cvlexchb1  39323  cvlexch3  39325  cvlexch4N  39326  cvlatexchb1  39327  cvlsupr2  39336  hlatjass  39363  hlatj12  39364  hlatj32  39365  cvrat  39416  atcvrj0  39422  cvrat2  39423  atltcvr  39429  atexchltN  39435  cvrat3  39436  cvrat4  39437  atbtwnexOLDN  39441  atbtwnex  39442  3dimlem3  39455  3dimlem3OLDN  39456  3at  39484  2atneat  39509  llncmp  39516  2at0mat0  39519  2atmat0  39520  islpln2a  39542  llncvrlpln  39552  lplncmp  39556  3atnelvolN  39580  4atlem11  39603  lplncvrlvol  39610  lvolcmp  39611  2atm2atN  39779  elpaddatriN  39797  elpadd2at2  39801  paddasslem8  39821  paddasslem17  39830  paddass  39832  padd12N  39833  paddssw1  39837  pmodlem2  39841  pmodN  39844  pmapjlln1  39849  atmod1i2  39853  pexmidlem2N  39965  pexmidlem7N  39970  pl42lem2N  39974  pl42lem3N  39975  pl42lem4N  39976  pl42N  39977  lhp2lt  39995  lhpm0atN  40023  lautlt  40085  lautcvr  40086  lautj  40087  lautm  40088  ltrneq2  40142  cdleme1b  40220  cdleme3b  40223  cdleme3c  40224  cdleme9b  40246  cdlemefs27cl  40407  cdleme42mN  40481  cdlemg4c  40606  trljco  40734  tgrpgrplem  40743  tendoplass  40777  tendodi1  40778  tendodi2  40779  erngplus2  40798  erngplus2-rN  40806  cdlemk36  40907  erngdvlem3  40984  erngdvlem3-rN  40992  dvaplusgv  41004  tendospass  41013  tendospdi1  41014  dvalveclem  41019  dialss  41040  dvhvaddass  41091  dvhopvsca  41096  dvhlveclem  41102  diblss  41164  diclss  41187  diclspsn  41188  cdlemn11pre  41204  dihmeetlem12N  41312  dihmeetlem16N  41316  dihmeetlem17N  41317  dvh4dimN  41441  lpolsatN  41482  lpolpolsatN  41483  dochpolN  41484  lclkr  41527  lclkrs  41533  lcfr  41579  lcmineqlem13  42029  aks6d1c1  42104  irrapxlem6  42815  jm2.26lem3  42990  mpaamn  43145  mendring  43177  mendlmod  43178  mendassa  43179  nnoeomeqom  43301  omabs2  43321  neicvgel1  44108  rfcnpre4  45028  fmuldfeq  45581  stoweidlem43  46041  stoweidlem52  46050  stoweidlem53  46051  stoweidlem56  46054  issmfgt  46754  issmfge  46768  iccelpart  47434  prproropf1olem1  47504  fmtnoprmfac1  47566  fmtnoprmfac2  47568  isubgr3stgrlem2  47966  isubgr3stgrlem4  47968  grlimgrtrilem1  47993  copissgrp  48156  cznrng  48249  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  linccl  48403  lincsumscmcl  48422  ldepsprlem  48461  lincresunit3lem1  48468  itsclc0yqe  48750  resipos  48963  topdlat  48992  catprs  49000  endmndlem  49004  idmon  49009  idepi  49010  thincmon  49422  thincepi  49423  functhinclem1  49433  grptcmon  49582  grptcepi  49583