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  7123  fpr2g  7188  isopolem  7323  fr3nr  7751  sexp3  8135  suppfnss  8171  naddass  8663  dif1en  9130  elfir  9373  intrnfi  9374  fisupcl  9428  cnfcomlem  9659  ttrclss  9680  dmttrcl  9681  rnttrcl  9682  ttrclselem2  9686  ackbij1lem15  10193  pwfseqlem4a  10621  pwfseqlem4  10622  eluzuzle  12809  xlesubadd  13230  elioc2  13377  elico2  13378  elicc2  13379  fseq1p1m1  13566  ccatswrd  14640  pfxccat3a  14710  2cshw  14785  tanadd  16142  dvds2ln  16266  prmgaplem5  17033  prmgaplem8  17036  cshwsidrepsw  17071  ressress  17224  f1ovscpbl  17496  mreexexlem4d  17615  mreexexd  17616  2oppccomf  17693  fthmon  17898  fuccocl  17936  fucidcl  17937  invfuc  17946  initoeu2lem1  17983  curf2cl  18199  yonedalem4c  18245  yonedalem3  18248  pospo  18311  latjle12  18416  latjlej1  18419  latnlej2  18425  latlem12  18432  latmlem1  18435  latledi  18443  latjass  18449  latj12  18450  latj32  18451  latj13  18452  latj31  18453  latjrot  18454  latjjdi  18457  latjjdir  18458  latdisdlem  18462  prdssgrpd  18667  prdsmndd  18704  imasmnd2  18708  imasmnd  18709  frmdmnd  18793  grpsubadd  18967  grpaddsubass  18969  grpsubsub4  18972  grppnpcan2  18973  grpnpncan  18974  grpnnncan2  18976  imasgrp2  18994  imasgrp  18995  mulgnndir  19042  mulgnn0dir  19043  mulgnnass  19048  mulgnn0ass  19049  mulgass  19050  pwsmulg  19058  issubg2  19080  qusgrp  19125  kerf1ghm  19186  galcan  19243  gacan  19244  oppgmnd  19293  pmtrprfv  19390  pmtr3ncom  19412  psgnunilem3  19433  frgp0  19697  cmn32  19737  cmn12  19739  abladdsub  19749  ablsubaddsub  19751  ablsubsub23  19761  mulgdi  19763  mulgsubdi  19766  dprdss  19968  dprdf1o  19971  dprdsn  19975  dmdprdsplit  19986  pgpfac1lem5  20018  prdsrngd  20092  imasrng  20093  srgdilem  20108  ringdilem  20165  ringrng  20201  prdsringd  20237  imasring  20246  opprrng  20261  mulgass3  20269  dvrass  20324  dvrdir  20328  subrgunit  20506  issubrg2  20508  isdomn4  20632  abvdiv  20745  lss1  20851  lsssn0  20861  islss3  20872  prdslmodd  20882  islmhm2  20952  lspsolv  21060  lbsextlem4  21078  sralmod  21101  rnglidl1  21149  ipdi  21556  ipsubdir  21558  ipsubdi  21559  ipassr  21562  ipassr2  21563  isphld  21570  ocvlss  21588  sraassab  21784  sraassaOLD  21786  psrgrpOLD  21873  psrlmod  21876  psrring  21886  psrassa  21889  mpllsslem  21916  mamudm  22289  matring  22337  matassa  22338  ofco2  22345  scmatlss  22419  ma1repveval  22465  mdetunilem1  22506  mdetunilem9  22514  monmatcollpw  22673  iinopn  22796  restopnb  23069  subbascn  23148  hausnei2  23247  nrmsep2  23250  isnrm3  23253  t1sep  23264  regsep2  23270  dnsconst  23272  dfconn2  23313  dislly  23391  tx1stc  23544  qtophmeo  23711  filss  23747  infil  23757  fsubbas  23761  filssufilg  23805  hauspwpwf1  23881  cnextcn  23961  tmdcn2  23983  psmettri  24206  isxmet2d  24222  xmettri  24246  xmetres2  24256  bldisj  24293  blss2ps  24298  blss2  24299  xmstri2  24361  mstri2  24362  xmstri  24363  mstri  24364  xmstri3  24365  mstri3  24366  msrtri  24367  comet  24408  met2ndci  24417  ngprcan  24505  ngplcan  24506  ngpsubcan  24509  nmtri2  24522  nrgdsdi  24560  nrgdsdir  24561  nlmdsdi  24576  nlmdsdir  24577  blcvx  24693  iocopnst  24844  icccvx  24855  pi1grplem  24956  pi1xfrf  24960  pi1cof  24966  clmpm1dir  25010  cmodscmulexp  25029  cvsdiv  25039  cvsdivcl  25040  cphdivcl  25089  cphsubdir  25115  cphsubdi  25116  bcthlem5  25235  rrxcph  25299  volfiniun  25455  volcn  25514  itg1val2  25592  dvconst  25825  dvlip  25905  ftc1a  25951  ulmdvlem3  26318  ang180  26731  cvxcl  26902  scvxcvx  26903  sgmmul  27119  logexprlim  27143  dchrabl  27172  nosupbnd1  27633  noinfbnd1lem5  27646  noinfbnd1  27648  ssltsep  27709  addscom  27880  addsbday  27931  addsdi  28065  mulsass  28076  motgrp  28477  iscgra1  28744  cgrane2  28747  cgrane4  28749  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgratr  28757  cgrabtwn  28760  cgrahl  28761  dfcgra2  28764  sacgr  28765  f1otrge  28806  xmstrkgc  28820  colinearalglem1  28840  colinearalg  28844  axcgrtr  28849  axlowdimlem16  28891  axeuclidlem  28896  axcontlem4  28901  axcontlem7  28904  axcontlem12  28909  eengtrkg  28920  eengtrkge  28921  edglnl  29077  subgruhgredgd  29218  nbfusgrlevtxm2  29312  upgrwlkdvde  29674  crctcshwlkn0lem5  29751  crctcshwlkn0  29758  umgrwwlks2on  29894  rusgrnumwwlks  29911  clwlkclwwlkfo  29945  3spthd  30112  frgr2wwlkeqm  30267  dlwwlknondlwlknonf1o  30301  numclwwlk5  30324  friendship  30335  grpomuldivass  30477  ablodivdiv4  30490  dipdi  30779  dipsubdi  30785  disjdsct  32633  omndmul2  33033  archiabllem2c  33156  dvrcan5  33194  rloccring  33228  reofld  33322  eqgvscpbl  33328  qusvsval  33330  quslmod  33336  quslmhm  33337  prmidlc  33426  ssdifidl  33435  ssmxidl  33452  ply1degltlss  33569  r1plmhm  33582  drgextlsp  33596  ccfldsrarelvec  33673  constrconj  33742  constrfin  33743  constrelextdg2  33744  pstmfval  33893  qqhval2lem  33978  qqhvq  33984  esumcvg  34083  sigaclcu  34114  measdivcst  34221  measdivcstALTV  34222  carsggect  34316  tgoldbachgtd  34660  bnj970  34944  bnj910  34945  erdszelem9  35193  cvmseu  35270  elmrsubrn  35514  r1peuqusdeg1  35637  cgrid2  35998  btwncomim  36008  btwnswapid  36012  trisegint  36023  cgrxfr  36050  btwnxfr  36051  brofs2  36072  brifs2  36073  endofsegid  36080  btwnconn1lem11  36092  btwnconn2  36097  segcon2  36100  seglemin  36108  segletr  36109  btwnsegle  36112  colinbtwnle  36113  broutsideof2  36117  btwnoutside  36120  broutsideof3  36121  outsideoftr  36124  outsidele  36127  ellines  36147  linethrueu  36151  weiunpo  36460  unbdqndv2  36506  poimirlem28  37649  ftc1anc  37702  sdclem1  37744  sstotbnd2  37775  ismndo1  37874  zerdivemp1x  37948  isdrngo2  37959  iscringd  37999  lsmsat  39008  lfladdcl  39071  lflnegcl  39075  lflvscl  39077  lshpkrlem4  39113  lshpkrlem6  39115  ldualgrplem  39145  lduallmodlem  39152  latmassOLD  39229  latm12  39230  latm32  39231  latmrot  39232  latmmdiN  39234  latmmdir  39235  omlfh1N  39258  omlfh3N  39259  cvrnbtwn2  39275  cvlexchb1  39330  cvlexch3  39332  cvlexch4N  39333  cvlatexchb1  39334  cvlsupr2  39343  hlatjass  39370  hlatj12  39371  hlatj32  39372  cvrat  39423  atcvrj0  39429  cvrat2  39430  atltcvr  39436  atexchltN  39442  cvrat3  39443  cvrat4  39444  atbtwnexOLDN  39448  atbtwnex  39449  3dimlem3  39462  3dimlem3OLDN  39463  3at  39491  2atneat  39516  llncmp  39523  2at0mat0  39526  2atmat0  39527  islpln2a  39549  llncvrlpln  39559  lplncmp  39563  3atnelvolN  39587  4atlem11  39610  lplncvrlvol  39617  lvolcmp  39618  2atm2atN  39786  elpaddatriN  39804  elpadd2at2  39808  paddasslem8  39828  paddasslem17  39837  paddass  39839  padd12N  39840  paddssw1  39844  pmodlem2  39848  pmodN  39851  pmapjlln1  39856  atmod1i2  39860  pexmidlem2N  39972  pexmidlem7N  39977  pl42lem2N  39981  pl42lem3N  39982  pl42lem4N  39983  pl42N  39984  lhp2lt  40002  lhpm0atN  40030  lautlt  40092  lautcvr  40093  lautj  40094  lautm  40095  ltrneq2  40149  cdleme1b  40227  cdleme3b  40230  cdleme3c  40231  cdleme9b  40253  cdlemefs27cl  40414  cdleme42mN  40488  cdlemg4c  40613  trljco  40741  tgrpgrplem  40750  tendoplass  40784  tendodi1  40785  tendodi2  40786  erngplus2  40805  erngplus2-rN  40813  cdlemk36  40914  erngdvlem3  40991  erngdvlem3-rN  40999  dvaplusgv  41011  tendospass  41020  tendospdi1  41021  dvalveclem  41026  dialss  41047  dvhvaddass  41098  dvhopvsca  41103  dvhlveclem  41109  diblss  41171  diclss  41194  diclspsn  41195  cdlemn11pre  41211  dihmeetlem12N  41319  dihmeetlem16N  41323  dihmeetlem17N  41324  dvh4dimN  41448  lpolsatN  41489  lpolpolsatN  41490  dochpolN  41491  lclkr  41534  lclkrs  41540  lcfr  41586  lcmineqlem13  42036  aks6d1c1  42111  irrapxlem6  42822  jm2.26lem3  42997  mpaamn  43152  mendring  43184  mendlmod  43185  mendassa  43186  nnoeomeqom  43308  omabs2  43328  neicvgel1  44115  rfcnpre4  45035  fmuldfeq  45588  stoweidlem43  46048  stoweidlem52  46057  stoweidlem53  46058  stoweidlem56  46061  issmfgt  46761  issmfge  46775  iccelpart  47438  prproropf1olem1  47508  fmtnoprmfac1  47570  fmtnoprmfac2  47572  isubgr3stgrlem2  47970  isubgr3stgrlem4  47972  grlimgrtrilem1  47997  copissgrp  48160  cznrng  48253  funcringcsetcALTV2lem9  48290  funcringcsetclem9ALTV  48313  linccl  48407  lincsumscmcl  48426  ldepsprlem  48465  lincresunit3lem1  48472  itsclc0yqe  48754  resipos  48967  topdlat  48996  catprs  49004  endmndlem  49008  idmon  49013  idepi  49014  thincmon  49426  thincepi  49427  functhinclem1  49437  grptcmon  49586  grptcepi  49587