Theorem simpr3 1193

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 488	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜃)
2	1	3ad2antr3 1187	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpr13  1256  simpr23  1259  simpr33  1262  simp1r3  1268  simp2r3  1274  simp3r3  1280  3anandis  1468  funopsn  6887  fpr2g  6951  isopolem  7077  fr3nr  7474  suppfnss  7838  elfir  8863  intrnfi  8864  fisupcl  8917  cnfcomlem  9146  ackbij1lem15  9645  pwfseqlem4a  10072  pwfseqlem4  10073  eluzuzle  12240  xlesubadd  12644  elioc2  12788  elico2  12789  elicc2  12790  fseq1p1m1  12976  ccatswrd  14021  pfxccat3a  14091  2cshw  14166  tanadd  15512  dvds2ln  15634  prmgaplem5  16381  prmgaplem8  16384  cshwsidrepsw  16419  ressress  16554  f1ovscpbl  16791  mreexexlem4d  16910  mreexexd  16911  2oppccomf  16987  fthmon  17189  fuccocl  17226  fucidcl  17227  invfuc  17236  initoeu2lem1  17266  curf2cl  17473  yonedalem4c  17519  yonedalem3  17522  pospo  17575  latjle12  17664  latjlej1  17667  latnlej2  17673  latlem12  17680  latmlem1  17683  latledi  17691  latjass  17697  latj12  17698  latj32  17699  latj13  17700  latj31  17701  latjrot  17702  latjjdi  17705  latjjdir  17706  latdisdlem  17791  prdsmndd  17936  imasmnd2  17940  imasmnd  17941  frmdmnd  18016  grpsubadd  18179  grpaddsubass  18181  grpsubsub4  18184  grppnpcan2  18185  grpnpncan  18186  grpnnncan2  18188  imasgrp2  18206  imasgrp  18207  mulgnndir  18248  mulgnn0dir  18249  mulgnnass  18254  mulgnn0ass  18255  mulgass  18256  pwsmulg  18264  issubg2  18286  qusgrp  18327  galcan  18426  gacan  18427  oppgmnd  18474  pmtrprfv  18573  pmtr3ncom  18595  psgnunilem3  18616  frgp0  18878  cmn32  18917  cmn12  18919  abladdsub  18928  ablsubsub23  18938  mulgdi  18940  mulgsubdi  18943  dprdss  19144  dprdf1o  19147  dprdsn  19151  dmdprdsplit  19162  pgpfac1lem5  19194  srgi  19254  ringi  19306  prdsringd  19358  imasring  19365  opprring  19377  mulgass3  19383  dvrass  19436  kerf1ghm  19491  subrgunit  19546  issubrg2  19548  abvdiv  19601  lss1  19703  lsssn0  19712  islss3  19724  prdslmodd  19734  islmhm2  19803  lspsolv  19908  lbsextlem4  19926  sralmod  19952  ipdi  20329  ipsubdir  20331  ipsubdi  20332  ipassr  20335  ipassr2  20336  isphld  20343  ocvlss  20361  sraassa  20556  psrbaglesupp  20606  psrbagcon  20609  psrgrp  20636  psrlmod  20639  psrring  20649  psrassa  20652  mpllsslem  20673  mamudm  20995  matring  21048  matassa  21049  ofco2  21056  scmatlss  21130  ma1repveval  21176  mdetunilem1  21217  mdetunilem9  21225  monmatcollpw  21384  iinopn  21507  restopnb  21780  subbascn  21859  hausnei2  21958  nrmsep2  21961  isnrm3  21964  t1sep  21975  regsep2  21981  dnsconst  21983  dfconn2  22024  dislly  22102  tx1stc  22255  qtophmeo  22422  filss  22458  infil  22468  fsubbas  22472  filssufilg  22516  hauspwpwf1  22592  cnextcn  22672  tmdcn2  22694  psmettri  22918  isxmet2d  22934  xmettri  22958  xmetres2  22968  bldisj  23005  blss2ps  23010  blss2  23011  xmstri2  23073  mstri2  23074  xmstri  23075  mstri  23076  xmstri3  23077  mstri3  23078  msrtri  23079  comet  23120  met2ndci  23129  ngprcan  23216  ngplcan  23217  ngpsubcan  23220  nmtri2  23233  nrgdsdi  23271  nrgdsdir  23272  nlmdsdi  23287  nlmdsdir  23288  blcvx  23403  iocopnst  23545  icccvx  23555  pi1grplem  23654  pi1xfrf  23658  pi1cof  23664  clmpm1dir  23708  cmodscmulexp  23727  cvsdiv  23737  cvsdivcl  23738  cphdivcl  23787  cphsubdir  23813  cphsubdi  23814  bcthlem5  23932  rrxcph  23996  volfiniun  24151  volcn  24210  itg1val2  24288  dvconst  24520  dvlip  24596  ftc1a  24640  ulmdvlem3  24997  ang180  25400  cvxcl  25570  scvxcvx  25571  sgmmul  25785  logexprlim  25809  dchrabl  25838  motgrp  26337  iscgra1  26604  cgrane2  26607  cgrane4  26609  cgrahl1  26610  cgrahl2  26611  cgracgr  26612  cgratr  26617  cgrabtwn  26620  cgrahl  26621  dfcgra2  26624  sacgr  26625  f1otrge  26666  xmstrkgc  26680  colinearalglem1  26700  colinearalg  26704  axcgrtr  26709  axlowdimlem16  26751  axeuclidlem  26756  axcontlem4  26761  axcontlem7  26764  axcontlem12  26769  eengtrkg  26780  eengtrkge  26781  edglnl  26936  subgruhgredgd  27074  nbfusgrlevtxm2  27168  upgrwlkdvde  27526  crctcshwlkn0lem5  27600  crctcshwlkn0  27607  umgrwwlks2on  27743  rusgrnumwwlks  27760  clwlkclwwlkfo  27794  3spthd  27961  frgr2wwlkeqm  28116  dlwwlknondlwlknonf1o  28150  numclwwlk5  28173  friendship  28184  grpomuldivass  28324  ablodivdiv4  28337  dipdi  28626  dipsubdi  28632  disjdsct  30462  omndmul2  30763  archiabllem2c  30874  dvrdir  30912  dvrcan5  30915  reofld  30964  eqgvscpbl  30970  qusscaval  30972  quslmod  30974  quslmhm  30975  prmidlc  31032  ssmxidl  31050  drgextlsp  31084  ccfldsrarelvec  31144  pstmfval  31249  qqhval2lem  31332  qqhvq  31338  esumcvg  31455  sigaclcu  31486  measdivcst  31593  measdivcstALTV  31594  carsggect  31686  tgoldbachgtd  32043  bnj970  32329  bnj910  32330  erdszelem9  32559  cvmseu  32636  elmrsubrn  32880  noprefixmo  33315  nosupbnd1  33327  ssltsep  33372  cgrid2  33577  btwncomim  33587  btwnswapid  33591  trisegint  33602  cgrxfr  33629  btwnxfr  33630  brofs2  33651  brifs2  33652  endofsegid  33659  btwnconn1lem11  33671  btwnconn2  33676  segcon2  33679  seglemin  33687  segletr  33688  btwnsegle  33691  colinbtwnle  33692  broutsideof2  33696  btwnoutside  33699  broutsideof3  33700  outsideoftr  33703  outsidele  33706  ellines  33726  linethrueu  33730  unbdqndv2  33963  poimirlem28  35085  ftc1anc  35138  sdclem1  35181  sstotbnd2  35212  ismndo1  35311  zerdivemp1x  35385  isdrngo2  35396  iscringd  35436  lsmsat  36304  lfladdcl  36367  lflnegcl  36371  lflvscl  36373  lshpkrlem4  36409  lshpkrlem6  36411  ldualgrplem  36441  lduallmodlem  36448  latmassOLD  36525  latm12  36526  latm32  36527  latmrot  36528  latmmdiN  36530  latmmdir  36531  omlfh1N  36554  omlfh3N  36555  cvrnbtwn2  36571  cvlexchb1  36626  cvlexch3  36628  cvlexch4N  36629  cvlatexchb1  36630  cvlsupr2  36639  hlatjass  36666  hlatj12  36667  hlatj32  36668  cvrat  36718  atcvrj0  36724  cvrat2  36725  atltcvr  36731  atexchltN  36737  cvrat3  36738  cvrat4  36739  atbtwnexOLDN  36743  atbtwnex  36744  3dimlem3  36757  3dimlem3OLDN  36758  3at  36786  2atneat  36811  llncmp  36818  2at0mat0  36821  2atmat0  36822  islpln2a  36844  llncvrlpln  36854  lplncmp  36858  3atnelvolN  36882  4atlem11  36905  lplncvrlvol  36912  lvolcmp  36913  2atm2atN  37081  elpaddatriN  37099  elpadd2at2  37103  paddasslem8  37123  paddasslem17  37132  paddass  37134  padd12N  37135  paddssw1  37139  pmodlem2  37143  pmodN  37146  pmapjlln1  37151  atmod1i2  37155  pexmidlem2N  37267  pexmidlem7N  37272  pl42lem2N  37276  pl42lem3N  37277  pl42lem4N  37278  pl42N  37279  lhp2lt  37297  lhpm0atN  37325  lautlt  37387  lautcvr  37388  lautj  37389  lautm  37390  ltrneq2  37444  cdleme1b  37522  cdleme3b  37525  cdleme3c  37526  cdleme9b  37548  cdlemefs27cl  37709  cdleme42mN  37783  cdlemg4c  37908  trljco  38036  tgrpgrplem  38045  tendoplass  38079  tendodi1  38080  tendodi2  38081  erngplus2  38100  erngplus2-rN  38108  cdlemk36  38209  erngdvlem3  38286  erngdvlem3-rN  38294  dvaplusgv  38306  tendospass  38315  tendospdi1  38316  dvalveclem  38321  dialss  38342  dvhvaddass  38393  dvhopvsca  38398  dvhlveclem  38404  diblss  38466  diclss  38489  diclspsn  38490  cdlemn11pre  38506  dihmeetlem12N  38614  dihmeetlem16N  38618  dihmeetlem17N  38619  dvh4dimN  38743  lpolsatN  38784  lpolpolsatN  38785  dochpolN  38786  lclkr  38829  lclkrs  38835  lcfr  38881  lcmineqlem13  39329  irrapxlem6  39768  jm2.26lem3  39942  mpaamn  40100  mendring  40136  mendlmod  40137  mendassa  40138  neicvgel1  40822  rfcnpre4  41663  fmuldfeq  42225  stoweidlem43  42685  stoweidlem52  42694  stoweidlem53  42695  stoweidlem56  42698  issmfgt  43390  issmfge  43403  iccelpart  43950  prproropf1olem1  44020  fmtnoprmfac1  44082  fmtnoprmfac2  44084  copissgrp  44428  ringrng  44503  cznrng  44579  funcringcsetcALTV2lem9  44668  funcringcsetclem9ALTV  44691  linccl  44823  lincsumscmcl  44842  ldepsprlem  44881  lincresunit3lem1  44888  itsclc0yqe  45175