MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpr3 Structured version   Visualization version   GIF version

Theorem simpr3 1188
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
StepHypRef Expression
1 simpr 485 . 2 ((𝜑𝜃) → 𝜃)
213ad2antr3 1182 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simpr13  1251  simpr23  1254  simpr33  1257  simp1r3  1263  simp2r3  1269  simp3r3  1275  3anandis  1462  funopsn  6903  fpr2g  6966  isopolem  7087  fr3nr  7482  suppfnss  7846  elfir  8868  intrnfi  8869  fisupcl  8922  cnfcomlem  9151  ackbij1lem15  9645  pwfseqlem4a  10072  pwfseqlem4  10073  eluzuzle  12241  xlesubadd  12646  elioc2  12789  elico2  12790  elicc2  12791  fseq1p1m1  12971  ccatswrd  14020  pfxccat3a  14090  2cshw  14165  tanadd  15510  dvds2ln  15632  prmgaplem5  16381  prmgaplem8  16384  cshwsidrepsw  16417  ressress  16552  f1ovscpbl  16789  mreexexlem4d  16908  mreexexd  16909  2oppccomf  16985  fthmon  17187  fuccocl  17224  fucidcl  17225  invfuc  17234  initoeu2lem1  17264  curf2cl  17471  yonedalem4c  17517  yonedalem3  17520  pospo  17573  latjle12  17662  latjlej1  17665  latnlej2  17671  latlem12  17678  latmlem1  17681  latledi  17689  latjass  17695  latj12  17696  latj32  17697  latj13  17698  latj31  17699  latjrot  17700  latjjdi  17703  latjjdir  17704  latdisdlem  17789  prdsmndd  17934  imasmnd2  17938  imasmnd  17939  frmdmnd  18014  grpsubadd  18127  grpaddsubass  18129  grpsubsub4  18132  grppnpcan2  18133  grpnpncan  18134  grpnnncan2  18136  imasgrp2  18154  imasgrp  18155  mulgnndir  18196  mulgnn0dir  18197  mulgnnass  18202  mulgnn0ass  18203  mulgass  18204  pwsmulg  18212  issubg2  18234  qusgrp  18275  galcan  18374  gacan  18375  oppgmnd  18422  pmtrprfv  18512  pmtr3ncom  18534  psgnunilem3  18555  frgp0  18817  cmn32  18856  cmn12  18858  abladdsub  18866  ablsubsub23  18876  mulgdi  18878  mulgsubdi  18881  dprdss  19082  dprdf1o  19085  dprdsn  19089  dmdprdsplit  19100  pgpfac1lem5  19132  srgi  19192  ringi  19241  prdsringd  19293  imasring  19300  opprring  19312  mulgass3  19318  dvrass  19371  kerf1ghm  19428  kerf1hrmOLD  19429  subrgunit  19484  issubrg2  19486  abvdiv  19539  lss1  19641  lsssn0  19650  islss3  19662  prdslmodd  19672  islmhm2  19741  lspsolv  19846  lbsextlem4  19864  sralmod  19890  sraassa  20029  psrbaglesupp  20078  psrbagcon  20081  psrgrp  20108  psrlmod  20111  psrring  20121  psrassa  20124  mpllsslem  20145  ipdi  20714  ipsubdir  20716  ipsubdi  20717  ipassr  20720  ipassr2  20721  isphld  20728  ocvlss  20746  mamudm  20929  matring  20982  matassa  20983  ofco2  20990  scmatlss  21064  ma1repveval  21110  mdetunilem1  21151  mdetunilem9  21159  monmatcollpw  21317  iinopn  21440  restopnb  21713  subbascn  21792  hausnei2  21891  nrmsep2  21894  isnrm3  21897  t1sep  21908  regsep2  21914  dnsconst  21916  dfconn2  21957  dislly  22035  tx1stc  22188  qtophmeo  22355  filss  22391  infil  22401  fsubbas  22405  filssufilg  22449  hauspwpwf1  22525  cnextcn  22605  tmdcn2  22627  psmettri  22850  isxmet2d  22866  xmettri  22890  xmetres2  22900  bldisj  22937  blss2ps  22942  blss2  22943  xmstri2  23005  mstri2  23006  xmstri  23007  mstri  23008  xmstri3  23009  mstri3  23010  msrtri  23011  comet  23052  met2ndci  23061  ngprcan  23148  ngplcan  23149  ngpsubcan  23152  nmtri2  23165  nrgdsdi  23203  nrgdsdir  23204  nlmdsdi  23219  nlmdsdir  23220  blcvx  23335  iocopnst  23473  icccvx  23483  pi1grplem  23582  pi1xfrf  23586  pi1cof  23592  clmpm1dir  23636  cmodscmulexp  23655  cvsdiv  23665  cvsdivcl  23666  cphdivcl  23715  cphsubdir  23741  cphsubdi  23742  bcthlem5  23860  rrxcph  23924  volfiniun  24077  volcn  24136  itg1val2  24214  dvconst  24443  dvlip  24519  ftc1a  24563  ulmdvlem3  24919  ang180  25319  cvxcl  25490  scvxcvx  25491  sgmmul  25705  logexprlim  25729  dchrabl  25758  motgrp  26257  iscgra1  26524  cgrane2  26527  cgrane4  26529  cgrahl1  26530  cgrahl2  26531  cgracgr  26532  cgratr  26537  cgrabtwn  26540  cgrahl  26541  dfcgra2  26544  sacgr  26545  f1otrge  26586  xmstrkgc  26600  colinearalglem1  26620  colinearalg  26624  axcgrtr  26629  axlowdimlem16  26671  axeuclidlem  26676  axcontlem4  26681  axcontlem7  26684  axcontlem12  26689  eengtrkg  26700  eengtrkge  26701  edglnl  26856  subgruhgredgd  26994  nbfusgrlevtxm2  27088  upgrwlkdvde  27446  crctcshwlkn0lem5  27520  crctcshwlkn0  27527  umgrwwlks2on  27664  rusgrnumwwlks  27681  clwlkclwwlkfo  27715  3spthd  27883  frgr2wwlkeqm  28038  dlwwlknondlwlknonf1o  28072  numclwwlk5  28095  friendship  28106  grpomuldivass  28246  ablodivdiv4  28259  dipdi  28548  dipsubdi  28554  disjdsct  30365  omndmul2  30641  archiabllem2c  30752  dvrdir  30789  dvrcan5  30792  reofld  30841  eqgvscpbl  30847  qusscaval  30849  quslmod  30851  quslmhm  30852  drgextlsp  30896  ccfldsrarelvec  30956  pstmfval  31036  qqhval2lem  31122  qqhvq  31128  esumcvg  31245  sigaclcu  31276  measdivcst  31383  measdivcstALTV  31384  carsggect  31476  tgoldbachgtd  31833  bnj970  32119  bnj910  32120  erdszelem9  32344  cvmseu  32421  elmrsubrn  32665  noprefixmo  33100  nosupbnd1  33112  ssltsep  33157  cgrid2  33362  btwncomim  33372  btwnswapid  33376  trisegint  33387  cgrxfr  33414  btwnxfr  33415  brofs2  33436  brifs2  33437  endofsegid  33444  btwnconn1lem11  33456  btwnconn2  33461  segcon2  33464  seglemin  33472  segletr  33473  btwnsegle  33476  colinbtwnle  33477  broutsideof2  33481  btwnoutside  33484  broutsideof3  33485  outsideoftr  33488  outsidele  33491  ellines  33511  linethrueu  33515  unbdqndv2  33748  poimirlem28  34802  ftc1anc  34857  sdclem1  34901  sstotbnd2  34935  ismndo1  35034  zerdivemp1x  35108  isdrngo2  35119  iscringd  35159  lsmsat  36026  lfladdcl  36089  lflnegcl  36093  lflvscl  36095  lshpkrlem4  36131  lshpkrlem6  36133  ldualgrplem  36163  lduallmodlem  36170  latmassOLD  36247  latm12  36248  latm32  36249  latmrot  36250  latmmdiN  36252  latmmdir  36253  omlfh1N  36276  omlfh3N  36277  cvrnbtwn2  36293  cvlexchb1  36348  cvlexch3  36350  cvlexch4N  36351  cvlatexchb1  36352  cvlsupr2  36361  hlatjass  36388  hlatj12  36389  hlatj32  36390  cvrat  36440  atcvrj0  36446  cvrat2  36447  atltcvr  36453  atexchltN  36459  cvrat3  36460  cvrat4  36461  atbtwnexOLDN  36465  atbtwnex  36466  3dimlem3  36479  3dimlem3OLDN  36480  3at  36508  2atneat  36533  llncmp  36540  2at0mat0  36543  2atmat0  36544  islpln2a  36566  llncvrlpln  36576  lplncmp  36580  3atnelvolN  36604  4atlem11  36627  lplncvrlvol  36634  lvolcmp  36635  2atm2atN  36803  elpaddatriN  36821  elpadd2at2  36825  paddasslem8  36845  paddasslem17  36854  paddass  36856  padd12N  36857  paddssw1  36861  pmodlem2  36865  pmodN  36868  pmapjlln1  36873  atmod1i2  36877  pexmidlem2N  36989  pexmidlem7N  36994  pl42lem2N  36998  pl42lem3N  36999  pl42lem4N  37000  pl42N  37001  lhp2lt  37019  lhpm0atN  37047  lautlt  37109  lautcvr  37110  lautj  37111  lautm  37112  ltrneq2  37166  cdleme1b  37244  cdleme3b  37247  cdleme3c  37248  cdleme9b  37270  cdlemefs27cl  37431  cdleme42mN  37505  cdlemg4c  37630  trljco  37758  tgrpgrplem  37767  tendoplass  37801  tendodi1  37802  tendodi2  37803  erngplus2  37822  erngplus2-rN  37830  cdlemk36  37931  erngdvlem3  38008  erngdvlem3-rN  38016  dvaplusgv  38028  tendospass  38037  tendospdi1  38038  dvalveclem  38043  dialss  38064  dvhvaddass  38115  dvhopvsca  38120  dvhlveclem  38126  diblss  38188  diclss  38211  diclspsn  38212  cdlemn11pre  38228  dihmeetlem12N  38336  dihmeetlem16N  38340  dihmeetlem17N  38341  dvh4dimN  38465  lpolsatN  38506  lpolpolsatN  38507  dochpolN  38508  lclkr  38551  lclkrs  38557  lcfr  38603  irrapxlem6  39304  jm2.26lem3  39478  mpaamn  39636  mendring  39672  mendlmod  39673  mendassa  39674  neicvgel1  40349  rfcnpre4  41171  fmuldfeq  41744  stoweidlem43  42209  stoweidlem52  42218  stoweidlem53  42219  stoweidlem56  42222  issmfgt  42914  issmfge  42927  iccelpart  43440  prproropf1olem1  43512  fmtnoprmfac1  43574  fmtnoprmfac2  43576  copissgrp  43922  ringrng  44048  cznrng  44124  funcringcsetcALTV2lem9  44213  funcringcsetclem9ALTV  44236  linccl  44367  lincsumscmcl  44386  ldepsprlem  44425  lincresunit3lem1  44432  itsclc0yqe  44646
  Copyright terms: Public domain W3C validator