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  7087  fpr2g  7151  isopolem  7285  fr3nr  7711  sexp3  8089  suppfnss  8125  naddass  8617  dif1en  9078  elfir  9306  intrnfi  9307  fisupcl  9361  cnfcomlem  9596  ttrclss  9617  dmttrcl  9618  rnttrcl  9619  ttrclselem2  9623  ackbij1lem15  10131  pwfseqlem4a  10559  pwfseqlem4  10560  eluzuzle  12747  xlesubadd  13164  elioc2  13311  elico2  13312  elicc2  13313  fseq1p1m1  13500  ccatswrd  14578  pfxccat3a  14647  2cshw  14722  tanadd  16078  dvds2ln  16202  prmgaplem5  16969  prmgaplem8  16972  cshwsidrepsw  17007  ressress  17160  f1ovscpbl  17432  mreexexlem4d  17555  mreexexd  17556  2oppccomf  17633  fthmon  17838  fuccocl  17876  fucidcl  17877  invfuc  17886  initoeu2lem1  17923  curf2cl  18139  yonedalem4c  18185  yonedalem3  18188  pospo  18251  latjle12  18358  latjlej1  18361  latnlej2  18367  latlem12  18374  latmlem1  18377  latledi  18385  latjass  18391  latj12  18392  latj32  18393  latj13  18394  latj31  18395  latjrot  18396  latjjdi  18399  latjjdir  18400  latdisdlem  18404  prdssgrpd  18643  prdsmndd  18680  imasmnd2  18684  imasmnd  18685  frmdmnd  18769  grpsubadd  18943  grpaddsubass  18945  grpsubsub4  18948  grppnpcan2  18949  grpnpncan  18950  grpnnncan2  18952  imasgrp2  18970  imasgrp  18971  mulgnndir  19018  mulgnn0dir  19019  mulgnnass  19024  mulgnn0ass  19025  mulgass  19026  pwsmulg  19034  issubg2  19056  qusgrp  19100  kerf1ghm  19161  galcan  19218  gacan  19219  oppgmnd  19268  pmtrprfv  19367  pmtr3ncom  19389  psgnunilem3  19410  frgp0  19674  cmn32  19714  cmn12  19716  abladdsub  19726  ablsubaddsub  19728  ablsubsub23  19738  mulgdi  19740  mulgsubdi  19743  dprdss  19945  dprdf1o  19948  dprdsn  19952  dmdprdsplit  19963  pgpfac1lem5  19995  omndmul2  20047  prdsrngd  20096  imasrng  20097  srgdilem  20112  ringdilem  20169  ringrng  20205  prdsringd  20241  imasring  20250  opprrng  20265  mulgass3  20273  dvrass  20328  dvrdir  20332  subrgunit  20507  issubrg2  20509  isdomn4  20633  abvdiv  20746  lss1  20873  lsssn0  20883  islss3  20894  prdslmodd  20904  islmhm2  20974  lspsolv  21082  lbsextlem4  21100  sralmod  21123  rnglidl1  21171  ipdi  21579  ipsubdir  21581  ipsubdi  21582  ipassr  21585  ipassr2  21586  isphld  21593  ocvlss  21611  sraassab  21807  sraassaOLD  21809  psrlmod  21898  psrring  21908  psrassa  21911  mpllsslem  21938  mamudm  22311  matring  22359  matassa  22360  ofco2  22367  scmatlss  22441  ma1repveval  22487  mdetunilem1  22528  mdetunilem9  22536  monmatcollpw  22695  iinopn  22818  restopnb  23091  subbascn  23170  hausnei2  23269  nrmsep2  23272  isnrm3  23275  t1sep  23286  regsep2  23292  dnsconst  23294  dfconn2  23335  dislly  23413  tx1stc  23566  qtophmeo  23733  filss  23769  infil  23779  fsubbas  23783  filssufilg  23827  hauspwpwf1  23903  cnextcn  23983  tmdcn2  24005  psmettri  24227  isxmet2d  24243  xmettri  24267  xmetres2  24277  bldisj  24314  blss2ps  24319  blss2  24320  xmstri2  24382  mstri2  24383  xmstri  24384  mstri  24385  xmstri3  24386  mstri3  24387  msrtri  24388  comet  24429  met2ndci  24438  ngprcan  24526  ngplcan  24527  ngpsubcan  24530  nmtri2  24543  nrgdsdi  24581  nrgdsdir  24582  nlmdsdi  24597  nlmdsdir  24598  blcvx  24714  iocopnst  24865  icccvx  24876  pi1grplem  24977  pi1xfrf  24981  pi1cof  24987  clmpm1dir  25031  cmodscmulexp  25050  cvsdiv  25060  cvsdivcl  25061  cphdivcl  25110  cphsubdir  25136  cphsubdi  25137  bcthlem5  25256  rrxcph  25320  volfiniun  25476  volcn  25535  itg1val2  25613  dvconst  25846  dvlip  25926  ftc1a  25972  ulmdvlem3  26339  ang180  26752  cvxcl  26923  scvxcvx  26924  sgmmul  27140  logexprlim  27164  dchrabl  27193  nosupbnd1  27654  noinfbnd1lem5  27667  noinfbnd1  27669  ssltsep  27731  addscom  27910  addsbday  27961  addsdi  28095  mulsass  28106  motgrp  28522  iscgra1  28789  cgrane2  28792  cgrane4  28794  cgrahl1  28795  cgrahl2  28796  cgracgr  28797  cgratr  28802  cgrabtwn  28805  cgrahl  28806  dfcgra2  28809  sacgr  28810  f1otrge  28851  xmstrkgc  28865  colinearalglem1  28886  colinearalg  28890  axcgrtr  28895  axlowdimlem16  28937  axeuclidlem  28942  axcontlem4  28947  axcontlem7  28950  axcontlem12  28955  eengtrkg  28966  eengtrkge  28967  edglnl  29123  subgruhgredgd  29264  nbfusgrlevtxm2  29358  upgrwlkdvde  29717  crctcshwlkn0lem5  29794  crctcshwlkn0  29801  usgrwwlks2on  29938  umgrwwlks2on  29939  rusgrnumwwlks  29957  clwlkclwwlkfo  29991  3spthd  30158  frgr2wwlkeqm  30313  dlwwlknondlwlknonf1o  30347  numclwwlk5  30370  friendship  30381  grpomuldivass  30523  ablodivdiv4  30536  dipdi  30825  dipsubdi  30831  disjdsct  32688  archiabllem2c  33171  dvrcan5  33210  rloccring  33244  reofld  33315  eqgvscpbl  33322  qusvsval  33324  quslmod  33330  quslmhm  33331  prmidlc  33420  ssdifidl  33429  ssmxidl  33446  ply1degltlss  33564  r1plmhm  33577  drgextlsp  33627  ccfldsrarelvec  33705  constrconj  33779  constrfin  33780  constrelextdg2  33781  pstmfval  33930  qqhval2lem  34015  qqhvq  34021  esumcvg  34120  sigaclcu  34151  measdivcst  34258  measdivcstALTV  34259  carsggect  34352  tgoldbachgtd  34696  bnj970  34980  bnj910  34981  erdszelem9  35264  cvmseu  35341  elmrsubrn  35585  r1peuqusdeg1  35708  cgrid2  36068  btwncomim  36078  btwnswapid  36082  trisegint  36093  cgrxfr  36120  btwnxfr  36121  brofs2  36142  brifs2  36143  endofsegid  36150  btwnconn1lem11  36162  btwnconn2  36167  segcon2  36170  seglemin  36178  segletr  36179  btwnsegle  36182  colinbtwnle  36183  broutsideof2  36187  btwnoutside  36190  broutsideof3  36191  outsideoftr  36194  outsidele  36197  ellines  36217  linethrueu  36221  weiunpo  36530  unbdqndv2  36576  poimirlem28  37708  ftc1anc  37761  sdclem1  37803  sstotbnd2  37834  ismndo1  37933  zerdivemp1x  38007  isdrngo2  38018  iscringd  38058  lsmsat  39127  lfladdcl  39190  lflnegcl  39194  lflvscl  39196  lshpkrlem4  39232  lshpkrlem6  39234  ldualgrplem  39264  lduallmodlem  39271  latmassOLD  39348  latm12  39349  latm32  39350  latmrot  39351  latmmdiN  39353  latmmdir  39354  omlfh1N  39377  omlfh3N  39378  cvrnbtwn2  39394  cvlexchb1  39449  cvlexch3  39451  cvlexch4N  39452  cvlatexchb1  39453  cvlsupr2  39462  hlatjass  39489  hlatj12  39490  hlatj32  39491  cvrat  39541  atcvrj0  39547  cvrat2  39548  atltcvr  39554  atexchltN  39560  cvrat3  39561  cvrat4  39562  atbtwnexOLDN  39566  atbtwnex  39567  3dimlem3  39580  3dimlem3OLDN  39581  3at  39609  2atneat  39634  llncmp  39641  2at0mat0  39644  2atmat0  39645  islpln2a  39667  llncvrlpln  39677  lplncmp  39681  3atnelvolN  39705  4atlem11  39728  lplncvrlvol  39735  lvolcmp  39736  2atm2atN  39904  elpaddatriN  39922  elpadd2at2  39926  paddasslem8  39946  paddasslem17  39955  paddass  39957  padd12N  39958  paddssw1  39962  pmodlem2  39966  pmodN  39969  pmapjlln1  39974  atmod1i2  39978  pexmidlem2N  40090  pexmidlem7N  40095  pl42lem2N  40099  pl42lem3N  40100  pl42lem4N  40101  pl42N  40102  lhp2lt  40120  lhpm0atN  40148  lautlt  40210  lautcvr  40211  lautj  40212  lautm  40213  ltrneq2  40267  cdleme1b  40345  cdleme3b  40348  cdleme3c  40349  cdleme9b  40371  cdlemefs27cl  40532  cdleme42mN  40606  cdlemg4c  40731  trljco  40859  tgrpgrplem  40868  tendoplass  40902  tendodi1  40903  tendodi2  40904  erngplus2  40923  erngplus2-rN  40931  cdlemk36  41032  erngdvlem3  41109  erngdvlem3-rN  41117  dvaplusgv  41129  tendospass  41138  tendospdi1  41139  dvalveclem  41144  dialss  41165  dvhvaddass  41216  dvhopvsca  41221  dvhlveclem  41227  diblss  41289  diclss  41312  diclspsn  41313  cdlemn11pre  41329  dihmeetlem12N  41437  dihmeetlem16N  41441  dihmeetlem17N  41442  dvh4dimN  41566  lpolsatN  41607  lpolpolsatN  41608  dochpolN  41609  lclkr  41652  lclkrs  41658  lcfr  41704  lcmineqlem13  42154  aks6d1c1  42229  irrapxlem6  42944  jm2.26lem3  43118  mpaamn  43273  mendring  43305  mendlmod  43306  mendassa  43307  nnoeomeqom  43429  omabs2  43449  neicvgel1  44236  rfcnpre4  45155  fmuldfeq  45707  stoweidlem43  46165  stoweidlem52  46174  stoweidlem53  46175  stoweidlem56  46178  issmfgt  46878  issmfge  46892  iccelpart  47557  prproropf1olem1  47627  fmtnoprmfac1  47689  fmtnoprmfac2  47691  isubgr3stgrlem2  48091  isubgr3stgrlem4  48093  grlimgrtrilem1  48125  copissgrp  48292  cznrng  48385  funcringcsetcALTV2lem9  48422  funcringcsetclem9ALTV  48445  linccl  48539  lincsumscmcl  48558  ldepsprlem  48597  lincresunit3lem1  48604  itsclc0yqe  48886  resipos  49099  topdlat  49128  catprs  49136  endmndlem  49140  idmon  49145  idepi  49146  thincmon  49558  thincepi  49559  functhinclem1  49569  grptcmon  49718  grptcepi  49719