Theorem simpr3 1196

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 1190	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃)

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

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 1089

This theorem is referenced by:  simpr13  1259  simpr23  1262  simpr33  1265  simp1r3  1271  simp2r3  1277  simp3r3  1283  3anandis  1471  funopsn  7052  fpr2g  7119  isopolem  7248  fr3nr  7654  suppfnss  8036  elfir  9218  intrnfi  9219  fisupcl  9272  cnfcomlem  9501  ttrclss  9522  dmttrcl  9523  rnttrcl  9524  ttrclselem2  9528  ackbij1lem15  10036  pwfseqlem4a  10463  pwfseqlem4  10464  eluzuzle  12637  xlesubadd  13043  elioc2  13188  elico2  13189  elicc2  13190  fseq1p1m1  13376  ccatswrd  14426  pfxccat3a  14496  2cshw  14571  tanadd  15921  dvds2ln  16043  prmgaplem5  16801  prmgaplem8  16804  cshwsidrepsw  16840  ressress  17003  f1ovscpbl  17282  mreexexlem4d  17401  mreexexd  17402  2oppccomf  17481  fthmon  17688  fuccocl  17727  fucidcl  17728  invfuc  17737  initoeu2lem1  17774  curf2cl  17994  yonedalem4c  18040  yonedalem3  18043  pospo  18108  latjle12  18213  latjlej1  18216  latnlej2  18222  latlem12  18229  latmlem1  18232  latledi  18240  latjass  18246  latj12  18247  latj32  18248  latj13  18249  latj31  18250  latjrot  18251  latjjdi  18254  latjjdir  18255  latdisdlem  18259  prdsmndd  18463  imasmnd2  18467  imasmnd  18468  frmdmnd  18543  grpsubadd  18708  grpaddsubass  18710  grpsubsub4  18713  grppnpcan2  18714  grpnpncan  18715  grpnnncan2  18717  imasgrp2  18735  imasgrp  18736  mulgnndir  18777  mulgnn0dir  18778  mulgnnass  18783  mulgnn0ass  18784  mulgass  18785  pwsmulg  18793  issubg2  18815  qusgrp  18856  galcan  18955  gacan  18956  oppgmnd  19006  pmtrprfv  19106  pmtr3ncom  19128  psgnunilem3  19149  frgp0  19411  cmn32  19450  cmn12  19452  abladdsub  19461  ablsubsub23  19471  mulgdi  19473  mulgsubdi  19476  dprdss  19677  dprdf1o  19680  dprdsn  19684  dmdprdsplit  19695  pgpfac1lem5  19727  srgdilem  19792  ringi  19844  prdsringd  19896  imasring  19903  opprring  19918  mulgass3  19924  dvrass  19977  kerf1ghm  20032  subrgunit  20087  issubrg2  20089  abvdiv  20142  lss1  20245  lsssn0  20254  islss3  20266  prdslmodd  20276  islmhm2  20345  lspsolv  20450  lbsextlem4  20468  sralmod  20502  ipdi  20890  ipsubdir  20892  ipsubdi  20893  ipassr  20896  ipassr2  20897  isphld  20904  ocvlss  20922  sraassa  21119  psrbaglesuppOLD  21173  psrbagconOLD  21179  psrgrp  21212  psrlmod  21215  psrring  21225  psrassa  21228  mpllsslem  21251  mamudm  21582  matring  21637  matassa  21638  ofco2  21645  scmatlss  21719  ma1repveval  21765  mdetunilem1  21806  mdetunilem9  21814  monmatcollpw  21973  iinopn  22096  restopnb  22371  subbascn  22450  hausnei2  22549  nrmsep2  22552  isnrm3  22555  t1sep  22566  regsep2  22572  dnsconst  22574  dfconn2  22615  dislly  22693  tx1stc  22846  qtophmeo  23013  filss  23049  infil  23059  fsubbas  23063  filssufilg  23107  hauspwpwf1  23183  cnextcn  23263  tmdcn2  23285  psmettri  23509  isxmet2d  23525  xmettri  23549  xmetres2  23559  bldisj  23596  blss2ps  23601  blss2  23602  xmstri2  23664  mstri2  23665  xmstri  23666  mstri  23667  xmstri3  23668  mstri3  23669  msrtri  23670  comet  23714  met2ndci  23723  ngprcan  23811  ngplcan  23812  ngpsubcan  23815  nmtri2  23828  nrgdsdi  23874  nrgdsdir  23875  nlmdsdi  23890  nlmdsdir  23891  blcvx  24006  iocopnst  24148  icccvx  24158  pi1grplem  24257  pi1xfrf  24261  pi1cof  24267  clmpm1dir  24311  cmodscmulexp  24330  cvsdiv  24340  cvsdivcl  24341  cphdivcl  24391  cphsubdir  24417  cphsubdi  24418  bcthlem5  24537  rrxcph  24601  volfiniun  24756  volcn  24815  itg1val2  24893  dvconst  25126  dvlip  25202  ftc1a  25246  ulmdvlem3  25606  ang180  26009  cvxcl  26179  scvxcvx  26180  sgmmul  26394  logexprlim  26418  dchrabl  26447  motgrp  26949  iscgra1  27216  cgrane2  27219  cgrane4  27221  cgrahl1  27222  cgrahl2  27223  cgracgr  27224  cgratr  27229  cgrabtwn  27232  cgrahl  27233  dfcgra2  27236  sacgr  27237  f1otrge  27278  xmstrkgc  27298  colinearalglem1  27319  colinearalg  27323  axcgrtr  27328  axlowdimlem16  27370  axeuclidlem  27375  axcontlem4  27380  axcontlem7  27383  axcontlem12  27388  eengtrkg  27399  eengtrkge  27400  edglnl  27558  subgruhgredgd  27696  nbfusgrlevtxm2  27790  upgrwlkdvde  28150  crctcshwlkn0lem5  28224  crctcshwlkn0  28231  umgrwwlks2on  28367  rusgrnumwwlks  28384  clwlkclwwlkfo  28418  3spthd  28585  frgr2wwlkeqm  28740  dlwwlknondlwlknonf1o  28774  numclwwlk5  28797  friendship  28808  grpomuldivass  28948  ablodivdiv4  28961  dipdi  29250  dipsubdi  29256  disjdsct  31080  omndmul2  31383  archiabllem2c  31494  dvrdir  31532  dvrcan5  31535  reofld  31589  eqgvscpbl  31595  qusscaval  31597  quslmod  31599  quslmhm  31600  prmidlc  31669  ssmxidl  31687  drgextlsp  31726  ccfldsrarelvec  31786  pstmfval  31891  qqhval2lem  31976  qqhvq  31982  esumcvg  32099  sigaclcu  32130  measdivcst  32237  measdivcstALTV  32238  carsggect  32330  tgoldbachgtd  32687  bnj970  32972  bnj910  32973  erdszelem9  33206  cvmseu  33283  elmrsubrn  33527  xpord3pred  33843  sexp3  33844  nosupbnd1  33962  noinfbnd1lem5  33975  noinfbnd1  33977  ssltsep  34030  addscom  34174  cgrid2  34350  btwncomim  34360  btwnswapid  34364  trisegint  34375  cgrxfr  34402  btwnxfr  34403  brofs2  34424  brifs2  34425  endofsegid  34432  btwnconn1lem11  34444  btwnconn2  34449  segcon2  34452  seglemin  34460  segletr  34461  btwnsegle  34464  colinbtwnle  34465  broutsideof2  34469  btwnoutside  34472  broutsideof3  34473  outsideoftr  34476  outsidele  34479  ellines  34499  linethrueu  34503  unbdqndv2  34736  poimirlem28  35849  ftc1anc  35902  sdclem1  35945  sstotbnd2  35976  ismndo1  36075  zerdivemp1x  36149  isdrngo2  36160  iscringd  36200  lsmsat  37064  lfladdcl  37127  lflnegcl  37131  lflvscl  37133  lshpkrlem4  37169  lshpkrlem6  37171  ldualgrplem  37201  lduallmodlem  37208  latmassOLD  37285  latm12  37286  latm32  37287  latmrot  37288  latmmdiN  37290  latmmdir  37291  omlfh1N  37314  omlfh3N  37315  cvrnbtwn2  37331  cvlexchb1  37386  cvlexch3  37388  cvlexch4N  37389  cvlatexchb1  37390  cvlsupr2  37399  hlatjass  37426  hlatj12  37427  hlatj32  37428  cvrat  37478  atcvrj0  37484  cvrat2  37485  atltcvr  37491  atexchltN  37497  cvrat3  37498  cvrat4  37499  atbtwnexOLDN  37503  atbtwnex  37504  3dimlem3  37517  3dimlem3OLDN  37518  3at  37546  2atneat  37571  llncmp  37578  2at0mat0  37581  2atmat0  37582  islpln2a  37604  llncvrlpln  37614  lplncmp  37618  3atnelvolN  37642  4atlem11  37665  lplncvrlvol  37672  lvolcmp  37673  2atm2atN  37841  elpaddatriN  37859  elpadd2at2  37863  paddasslem8  37883  paddasslem17  37892  paddass  37894  padd12N  37895  paddssw1  37899  pmodlem2  37903  pmodN  37906  pmapjlln1  37911  atmod1i2  37915  pexmidlem2N  38027  pexmidlem7N  38032  pl42lem2N  38036  pl42lem3N  38037  pl42lem4N  38038  pl42N  38039  lhp2lt  38057  lhpm0atN  38085  lautlt  38147  lautcvr  38148  lautj  38149  lautm  38150  ltrneq2  38204  cdleme1b  38282  cdleme3b  38285  cdleme3c  38286  cdleme9b  38308  cdlemefs27cl  38469  cdleme42mN  38543  cdlemg4c  38668  trljco  38796  tgrpgrplem  38805  tendoplass  38839  tendodi1  38840  tendodi2  38841  erngplus2  38860  erngplus2-rN  38868  cdlemk36  38969  erngdvlem3  39046  erngdvlem3-rN  39054  dvaplusgv  39066  tendospass  39075  tendospdi1  39076  dvalveclem  39081  dialss  39102  dvhvaddass  39153  dvhopvsca  39158  dvhlveclem  39164  diblss  39226  diclss  39249  diclspsn  39250  cdlemn11pre  39266  dihmeetlem12N  39374  dihmeetlem16N  39378  dihmeetlem17N  39379  dvh4dimN  39503  lpolsatN  39544  lpolpolsatN  39545  dochpolN  39546  lclkr  39589  lclkrs  39595  lcfr  39641  lcmineqlem13  40091  isdomn4  40214  irrapxlem6  40686  jm2.26lem3  40861  mpaamn  41019  mendring  41055  mendlmod  41056  mendassa  41057  neicvgel1  41767  rfcnpre4  42615  fmuldfeq  43173  stoweidlem43  43633  stoweidlem52  43642  stoweidlem53  43643  stoweidlem56  43646  issmfgt  44344  issmfge  44358  iccelpart  44943  prproropf1olem1  45013  fmtnoprmfac1  45075  fmtnoprmfac2  45077  copissgrp  45420  ringrng  45495  cznrng  45571  funcringcsetcALTV2lem9  45660  funcringcsetclem9ALTV  45683  linccl  45813  lincsumscmcl  45832  ldepsprlem  45871  lincresunit3lem1  45878  itsclc0yqe  46165  topdlat  46348  catprs  46350  endmndlem  46354  idmon  46355  idepi  46356  thincmon  46373  thincepi  46374  functhinclem1  46380  grptcmon  46435  grptcepi  46436