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

Theorem simpr3 1193
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 488 . 2 ((𝜑𝜃) → 𝜃)
213ad2antr3 1187 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simpr13  1256  simpr23  1259  simpr33  1262  simp1r3  1268  simp2r3  1274  simp3r3  1280  3anandis  1468  funopsn  6892  fpr2g  6956  isopolem  7082  fr3nr  7479  suppfnss  7842  elfir  8867  intrnfi  8868  fisupcl  8921  cnfcomlem  9150  ackbij1lem15  9645  pwfseqlem4a  10072  pwfseqlem4  10073  eluzuzle  12240  xlesubadd  12644  elioc2  12788  elico2  12789  elicc2  12790  fseq1p1m1  12976  ccatswrd  14021  pfxccat3a  14091  2cshw  14166  tanadd  15511  dvds2ln  15633  prmgaplem5  16380  prmgaplem8  16383  cshwsidrepsw  16418  ressress  16553  f1ovscpbl  16790  mreexexlem4d  16909  mreexexd  16910  2oppccomf  16986  fthmon  17188  fuccocl  17225  fucidcl  17226  invfuc  17235  initoeu2lem1  17265  curf2cl  17472  yonedalem4c  17518  yonedalem3  17521  pospo  17574  latjle12  17663  latjlej1  17666  latnlej2  17672  latlem12  17679  latmlem1  17682  latledi  17690  latjass  17696  latj12  17697  latj32  17698  latj13  17699  latj31  17700  latjrot  17701  latjjdi  17704  latjjdir  17705  latdisdlem  17790  prdsmndd  17935  imasmnd2  17939  imasmnd  17940  frmdmnd  18015  grpsubadd  18178  grpaddsubass  18180  grpsubsub4  18183  grppnpcan2  18184  grpnpncan  18185  grpnnncan2  18187  imasgrp2  18205  imasgrp  18206  mulgnndir  18247  mulgnn0dir  18248  mulgnnass  18253  mulgnn0ass  18254  mulgass  18255  pwsmulg  18263  issubg2  18285  qusgrp  18326  galcan  18425  gacan  18426  oppgmnd  18473  pmtrprfv  18572  pmtr3ncom  18594  psgnunilem3  18615  frgp0  18877  cmn32  18916  cmn12  18918  abladdsub  18926  ablsubsub23  18936  mulgdi  18938  mulgsubdi  18941  dprdss  19142  dprdf1o  19145  dprdsn  19149  dmdprdsplit  19160  pgpfac1lem5  19192  srgi  19252  ringi  19304  prdsringd  19356  imasring  19363  opprring  19375  mulgass3  19381  dvrass  19434  kerf1ghm  19489  subrgunit  19544  issubrg2  19546  abvdiv  19599  lss1  19701  lsssn0  19710  islss3  19722  prdslmodd  19732  islmhm2  19801  lspsolv  19906  lbsextlem4  19924  sralmod  19950  ipdi  20327  ipsubdir  20329  ipsubdi  20330  ipassr  20333  ipassr2  20334  isphld  20341  ocvlss  20359  sraassa  20554  psrbaglesupp  20604  psrbagcon  20607  psrgrp  20634  psrlmod  20637  psrring  20647  psrassa  20650  mpllsslem  20671  mamudm  20993  matring  21046  matassa  21047  ofco2  21054  scmatlss  21128  ma1repveval  21174  mdetunilem1  21215  mdetunilem9  21223  monmatcollpw  21382  iinopn  21505  restopnb  21778  subbascn  21857  hausnei2  21956  nrmsep2  21959  isnrm3  21962  t1sep  21973  regsep2  21979  dnsconst  21981  dfconn2  22022  dislly  22100  tx1stc  22253  qtophmeo  22420  filss  22456  infil  22466  fsubbas  22470  filssufilg  22514  hauspwpwf1  22590  cnextcn  22670  tmdcn2  22692  psmettri  22916  isxmet2d  22932  xmettri  22956  xmetres2  22966  bldisj  23003  blss2ps  23008  blss2  23009  xmstri2  23071  mstri2  23072  xmstri  23073  mstri  23074  xmstri3  23075  mstri3  23076  msrtri  23077  comet  23118  met2ndci  23127  ngprcan  23214  ngplcan  23215  ngpsubcan  23218  nmtri2  23231  nrgdsdi  23269  nrgdsdir  23270  nlmdsdi  23285  nlmdsdir  23286  blcvx  23401  iocopnst  23543  icccvx  23553  pi1grplem  23652  pi1xfrf  23656  pi1cof  23662  clmpm1dir  23706  cmodscmulexp  23725  cvsdiv  23735  cvsdivcl  23736  cphdivcl  23785  cphsubdir  23811  cphsubdi  23812  bcthlem5  23930  rrxcph  23994  volfiniun  24149  volcn  24208  itg1val2  24286  dvconst  24518  dvlip  24594  ftc1a  24638  ulmdvlem3  24995  ang180  25398  cvxcl  25568  scvxcvx  25569  sgmmul  25783  logexprlim  25807  dchrabl  25836  motgrp  26335  iscgra1  26602  cgrane2  26605  cgrane4  26607  cgrahl1  26608  cgrahl2  26609  cgracgr  26610  cgratr  26615  cgrabtwn  26618  cgrahl  26619  dfcgra2  26622  sacgr  26623  f1otrge  26664  xmstrkgc  26678  colinearalglem1  26698  colinearalg  26702  axcgrtr  26707  axlowdimlem16  26749  axeuclidlem  26754  axcontlem4  26759  axcontlem7  26762  axcontlem12  26767  eengtrkg  26778  eengtrkge  26779  edglnl  26934  subgruhgredgd  27072  nbfusgrlevtxm2  27166  upgrwlkdvde  27524  crctcshwlkn0lem5  27598  crctcshwlkn0  27605  umgrwwlks2on  27741  rusgrnumwwlks  27758  clwlkclwwlkfo  27792  3spthd  27959  frgr2wwlkeqm  28114  dlwwlknondlwlknonf1o  28148  numclwwlk5  28171  friendship  28182  grpomuldivass  28322  ablodivdiv4  28335  dipdi  28624  dipsubdi  28630  disjdsct  30446  omndmul2  30744  archiabllem2c  30855  dvrdir  30893  dvrcan5  30896  reofld  30945  eqgvscpbl  30951  qusscaval  30953  quslmod  30955  quslmhm  30956  prmidlc  31006  ssmxidl  31021  drgextlsp  31053  ccfldsrarelvec  31113  pstmfval  31213  qqhval2lem  31296  qqhvq  31302  esumcvg  31419  sigaclcu  31450  measdivcst  31557  measdivcstALTV  31558  carsggect  31650  tgoldbachgtd  32007  bnj970  32293  bnj910  32294  erdszelem9  32520  cvmseu  32597  elmrsubrn  32841  noprefixmo  33276  nosupbnd1  33288  ssltsep  33333  cgrid2  33538  btwncomim  33548  btwnswapid  33552  trisegint  33563  cgrxfr  33590  btwnxfr  33591  brofs2  33612  brifs2  33613  endofsegid  33620  btwnconn1lem11  33632  btwnconn2  33637  segcon2  33640  seglemin  33648  segletr  33649  btwnsegle  33652  colinbtwnle  33653  broutsideof2  33657  btwnoutside  33660  broutsideof3  33661  outsideoftr  33664  outsidele  33667  ellines  33687  linethrueu  33691  unbdqndv2  33924  poimirlem28  35044  ftc1anc  35097  sdclem1  35140  sstotbnd2  35171  ismndo1  35270  zerdivemp1x  35344  isdrngo2  35355  iscringd  35395  lsmsat  36263  lfladdcl  36326  lflnegcl  36330  lflvscl  36332  lshpkrlem4  36368  lshpkrlem6  36370  ldualgrplem  36400  lduallmodlem  36407  latmassOLD  36484  latm12  36485  latm32  36486  latmrot  36487  latmmdiN  36489  latmmdir  36490  omlfh1N  36513  omlfh3N  36514  cvrnbtwn2  36530  cvlexchb1  36585  cvlexch3  36587  cvlexch4N  36588  cvlatexchb1  36589  cvlsupr2  36598  hlatjass  36625  hlatj12  36626  hlatj32  36627  cvrat  36677  atcvrj0  36683  cvrat2  36684  atltcvr  36690  atexchltN  36696  cvrat3  36697  cvrat4  36698  atbtwnexOLDN  36702  atbtwnex  36703  3dimlem3  36716  3dimlem3OLDN  36717  3at  36745  2atneat  36770  llncmp  36777  2at0mat0  36780  2atmat0  36781  islpln2a  36803  llncvrlpln  36813  lplncmp  36817  3atnelvolN  36841  4atlem11  36864  lplncvrlvol  36871  lvolcmp  36872  2atm2atN  37040  elpaddatriN  37058  elpadd2at2  37062  paddasslem8  37082  paddasslem17  37091  paddass  37093  padd12N  37094  paddssw1  37098  pmodlem2  37102  pmodN  37105  pmapjlln1  37110  atmod1i2  37114  pexmidlem2N  37226  pexmidlem7N  37231  pl42lem2N  37235  pl42lem3N  37236  pl42lem4N  37237  pl42N  37238  lhp2lt  37256  lhpm0atN  37284  lautlt  37346  lautcvr  37347  lautj  37348  lautm  37349  ltrneq2  37403  cdleme1b  37481  cdleme3b  37484  cdleme3c  37485  cdleme9b  37507  cdlemefs27cl  37668  cdleme42mN  37742  cdlemg4c  37867  trljco  37995  tgrpgrplem  38004  tendoplass  38038  tendodi1  38039  tendodi2  38040  erngplus2  38059  erngplus2-rN  38067  cdlemk36  38168  erngdvlem3  38245  erngdvlem3-rN  38253  dvaplusgv  38265  tendospass  38274  tendospdi1  38275  dvalveclem  38280  dialss  38301  dvhvaddass  38352  dvhopvsca  38357  dvhlveclem  38363  diblss  38425  diclss  38448  diclspsn  38449  cdlemn11pre  38465  dihmeetlem12N  38573  dihmeetlem16N  38577  dihmeetlem17N  38578  dvh4dimN  38702  lpolsatN  38743  lpolpolsatN  38744  dochpolN  38745  lclkr  38788  lclkrs  38794  lcfr  38840  lcmineqlem13  39291  irrapxlem6  39699  jm2.26lem3  39873  mpaamn  40031  mendring  40067  mendlmod  40068  mendassa  40069  neicvgel1  40756  rfcnpre4  41598  fmuldfeq  42165  stoweidlem43  42625  stoweidlem52  42634  stoweidlem53  42635  stoweidlem56  42638  issmfgt  43330  issmfge  43343  iccelpart  43890  prproropf1olem1  43960  fmtnoprmfac1  44022  fmtnoprmfac2  44024  copissgrp  44368  ringrng  44443  cznrng  44519  funcringcsetcALTV2lem9  44608  funcringcsetclem9ALTV  44631  linccl  44763  lincsumscmcl  44782  ldepsprlem  44821  lincresunit3lem1  44828  itsclc0yqe  45115
  Copyright terms: Public domain W3C validator