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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simpr13  1260  simpr23  1263  simpr33  1266  simp1r3  1272  simp2r3  1278  simp3r3  1284  3anandis  1472  funopsn  7146  fpr2g  7213  isopolem  7342  fr3nr  7759  sexp3  8139  suppfnss  8174  naddass  8695  dif1en  9160  elfir  9410  intrnfi  9411  fisupcl  9464  cnfcomlem  9694  ttrclss  9715  dmttrcl  9716  rnttrcl  9717  ttrclselem2  9721  ackbij1lem15  10229  pwfseqlem4a  10656  pwfseqlem4  10657  eluzuzle  12831  xlesubadd  13242  elioc2  13387  elico2  13388  elicc2  13389  fseq1p1m1  13575  ccatswrd  14618  pfxccat3a  14688  2cshw  14763  tanadd  16110  dvds2ln  16232  prmgaplem5  16988  prmgaplem8  16991  cshwsidrepsw  17027  ressress  17193  f1ovscpbl  17472  mreexexlem4d  17591  mreexexd  17592  2oppccomf  17671  fthmon  17878  fuccocl  17917  fucidcl  17918  invfuc  17927  initoeu2lem1  17964  curf2cl  18184  yonedalem4c  18230  yonedalem3  18233  pospo  18298  latjle12  18403  latjlej1  18406  latnlej2  18412  latlem12  18419  latmlem1  18422  latledi  18430  latjass  18436  latj12  18437  latj32  18438  latj13  18439  latj31  18440  latjrot  18441  latjjdi  18444  latjjdir  18445  latdisdlem  18449  prdssgrpd  18624  prdsmndd  18658  imasmnd2  18662  imasmnd  18663  frmdmnd  18740  grpsubadd  18911  grpaddsubass  18913  grpsubsub4  18916  grppnpcan2  18917  grpnpncan  18918  grpnnncan2  18920  imasgrp2  18938  imasgrp  18939  mulgnndir  18983  mulgnn0dir  18984  mulgnnass  18989  mulgnn0ass  18990  mulgass  18991  pwsmulg  18999  issubg2  19021  qusgrp  19065  galcan  19168  gacan  19169  oppgmnd  19221  pmtrprfv  19321  pmtr3ncom  19343  psgnunilem3  19364  frgp0  19628  cmn32  19668  cmn12  19670  abladdsub  19680  ablsubaddsub  19682  ablsubsub23  19692  mulgdi  19694  mulgsubdi  19697  dprdss  19899  dprdf1o  19902  dprdsn  19906  dmdprdsplit  19917  pgpfac1lem5  19949  srgdilem  20015  ringdilem  20072  prdsringd  20134  imasring  20143  opprring  20161  mulgass3  20167  dvrass  20222  dvrdir  20226  kerf1ghm  20282  subrgunit  20337  issubrg2  20339  abvdiv  20445  lss1  20549  lsssn0  20558  islss3  20570  prdslmodd  20580  islmhm2  20649  lspsolv  20756  lbsextlem4  20774  sralmod  20809  isdomn4  20918  ipdi  21193  ipsubdir  21195  ipsubdi  21196  ipassr  21199  ipassr2  21200  isphld  21207  ocvlss  21225  sraassab  21422  sraassaOLD  21424  psrbaglesuppOLD  21478  psrbagconOLD  21484  psrgrpOLD  21518  psrlmod  21521  psrring  21531  psrassa  21534  mpllsslem  21559  mamudm  21890  matring  21945  matassa  21946  ofco2  21953  scmatlss  22027  ma1repveval  22073  mdetunilem1  22114  mdetunilem9  22122  monmatcollpw  22281  iinopn  22404  restopnb  22679  subbascn  22758  hausnei2  22857  nrmsep2  22860  isnrm3  22863  t1sep  22874  regsep2  22880  dnsconst  22882  dfconn2  22923  dislly  23001  tx1stc  23154  qtophmeo  23321  filss  23357  infil  23367  fsubbas  23371  filssufilg  23415  hauspwpwf1  23491  cnextcn  23571  tmdcn2  23593  psmettri  23817  isxmet2d  23833  xmettri  23857  xmetres2  23867  bldisj  23904  blss2ps  23909  blss2  23910  xmstri2  23972  mstri2  23973  xmstri  23974  mstri  23975  xmstri3  23976  mstri3  23977  msrtri  23978  comet  24022  met2ndci  24031  ngprcan  24119  ngplcan  24120  ngpsubcan  24123  nmtri2  24136  nrgdsdi  24182  nrgdsdir  24183  nlmdsdi  24198  nlmdsdir  24199  blcvx  24314  iocopnst  24456  icccvx  24466  pi1grplem  24565  pi1xfrf  24569  pi1cof  24575  clmpm1dir  24619  cmodscmulexp  24638  cvsdiv  24648  cvsdivcl  24649  cphdivcl  24699  cphsubdir  24725  cphsubdi  24726  bcthlem5  24845  rrxcph  24909  volfiniun  25064  volcn  25123  itg1val2  25201  dvconst  25434  dvlip  25510  ftc1a  25554  ulmdvlem3  25914  ang180  26319  cvxcl  26489  scvxcvx  26490  sgmmul  26704  logexprlim  26728  dchrabl  26757  nosupbnd1  27217  noinfbnd1lem5  27230  noinfbnd1  27232  ssltsep  27292  addscom  27452  addsdi  27613  mulsass  27624  motgrp  27825  iscgra1  28092  cgrane2  28095  cgrane4  28097  cgrahl1  28098  cgrahl2  28099  cgracgr  28100  cgratr  28105  cgrabtwn  28108  cgrahl  28109  dfcgra2  28112  sacgr  28113  f1otrge  28154  xmstrkgc  28174  colinearalglem1  28195  colinearalg  28199  axcgrtr  28204  axlowdimlem16  28246  axeuclidlem  28251  axcontlem4  28256  axcontlem7  28259  axcontlem12  28264  eengtrkg  28275  eengtrkge  28276  edglnl  28434  subgruhgredgd  28572  nbfusgrlevtxm2  28666  upgrwlkdvde  29025  crctcshwlkn0lem5  29099  crctcshwlkn0  29106  umgrwwlks2on  29242  rusgrnumwwlks  29259  clwlkclwwlkfo  29293  3spthd  29460  frgr2wwlkeqm  29615  dlwwlknondlwlknonf1o  29649  numclwwlk5  29672  friendship  29683  grpomuldivass  29825  ablodivdiv4  29838  dipdi  30127  dipsubdi  30133  disjdsct  31955  omndmul2  32261  archiabllem2c  32372  dvrcan5  32416  reofld  32490  eqgvscpbl  32496  qusvsval  32498  quslmod  32500  quslmhm  32501  prmidlc  32598  ssmxidl  32621  ply1degltlss  32698  drgextlsp  32712  ccfldsrarelvec  32776  pstmfval  32907  qqhval2lem  32992  qqhvq  32998  esumcvg  33115  sigaclcu  33146  measdivcst  33253  measdivcstALTV  33254  carsggect  33348  tgoldbachgtd  33705  bnj970  33989  bnj910  33990  erdszelem9  34221  cvmseu  34298  elmrsubrn  34542  cgrid2  35006  btwncomim  35016  btwnswapid  35020  trisegint  35031  cgrxfr  35058  btwnxfr  35059  brofs2  35080  brifs2  35081  endofsegid  35088  btwnconn1lem11  35100  btwnconn2  35105  segcon2  35108  seglemin  35116  segletr  35117  btwnsegle  35120  colinbtwnle  35121  broutsideof2  35125  btwnoutside  35128  broutsideof3  35129  outsideoftr  35132  outsidele  35135  ellines  35155  linethrueu  35159  unbdqndv2  35435  poimirlem28  36564  ftc1anc  36617  sdclem1  36659  sstotbnd2  36690  ismndo1  36789  zerdivemp1x  36863  isdrngo2  36874  iscringd  36914  lsmsat  37926  lfladdcl  37989  lflnegcl  37993  lflvscl  37995  lshpkrlem4  38031  lshpkrlem6  38033  ldualgrplem  38063  lduallmodlem  38070  latmassOLD  38147  latm12  38148  latm32  38149  latmrot  38150  latmmdiN  38152  latmmdir  38153  omlfh1N  38176  omlfh3N  38177  cvrnbtwn2  38193  cvlexchb1  38248  cvlexch3  38250  cvlexch4N  38251  cvlatexchb1  38252  cvlsupr2  38261  hlatjass  38288  hlatj12  38289  hlatj32  38290  cvrat  38341  atcvrj0  38347  cvrat2  38348  atltcvr  38354  atexchltN  38360  cvrat3  38361  cvrat4  38362  atbtwnexOLDN  38366  atbtwnex  38367  3dimlem3  38380  3dimlem3OLDN  38381  3at  38409  2atneat  38434  llncmp  38441  2at0mat0  38444  2atmat0  38445  islpln2a  38467  llncvrlpln  38477  lplncmp  38481  3atnelvolN  38505  4atlem11  38528  lplncvrlvol  38535  lvolcmp  38536  2atm2atN  38704  elpaddatriN  38722  elpadd2at2  38726  paddasslem8  38746  paddasslem17  38755  paddass  38757  padd12N  38758  paddssw1  38762  pmodlem2  38766  pmodN  38769  pmapjlln1  38774  atmod1i2  38778  pexmidlem2N  38890  pexmidlem7N  38895  pl42lem2N  38899  pl42lem3N  38900  pl42lem4N  38901  pl42N  38902  lhp2lt  38920  lhpm0atN  38948  lautlt  39010  lautcvr  39011  lautj  39012  lautm  39013  ltrneq2  39067  cdleme1b  39145  cdleme3b  39148  cdleme3c  39149  cdleme9b  39171  cdlemefs27cl  39332  cdleme42mN  39406  cdlemg4c  39531  trljco  39659  tgrpgrplem  39668  tendoplass  39702  tendodi1  39703  tendodi2  39704  erngplus2  39723  erngplus2-rN  39731  cdlemk36  39832  erngdvlem3  39909  erngdvlem3-rN  39917  dvaplusgv  39929  tendospass  39938  tendospdi1  39939  dvalveclem  39944  dialss  39965  dvhvaddass  40016  dvhopvsca  40021  dvhlveclem  40027  diblss  40089  diclss  40112  diclspsn  40113  cdlemn11pre  40129  dihmeetlem12N  40237  dihmeetlem16N  40241  dihmeetlem17N  40242  dvh4dimN  40366  lpolsatN  40407  lpolpolsatN  40408  dochpolN  40409  lclkr  40452  lclkrs  40458  lcfr  40504  lcmineqlem13  40954  irrapxlem6  41613  jm2.26lem3  41788  mpaamn  41946  mendring  41982  mendlmod  41983  mendassa  41984  nnoeomeqom  42110  omabs2  42130  neicvgel1  42918  rfcnpre4  43766  fmuldfeq  44347  stoweidlem43  44807  stoweidlem52  44816  stoweidlem53  44817  stoweidlem56  44820  issmfgt  45520  issmfge  45534  iccelpart  46149  prproropf1olem1  46219  fmtnoprmfac1  46281  fmtnoprmfac2  46283  copissgrp  46626  ringrng  46703  opprrng  46722  prdsrngd  46725  imasrng  46726  rnglidl1  46801  cznrng  46901  funcringcsetcALTV2lem9  46990  funcringcsetclem9ALTV  47013  linccl  47143  lincsumscmcl  47162  ldepsprlem  47201  lincresunit3lem1  47208  itsclc0yqe  47495  topdlat  47677  catprs  47679  endmndlem  47683  idmon  47684  idepi  47685  thincmon  47702  thincepi  47703  functhinclem1  47709  grptcmon  47764  grptcepi  47765