MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrr Unicode version

Theorem adantrr 697
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantrr  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 443 . 2  |-  ( ( ps  /\  th )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 460 1  |-  ( (
ph  /\  ( ps  /\ 
th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2ant2r  727  ad2ant2lr  728  consensus  925  3ad2antr1  1120  sbcom  2028  ax11eq  2133  ax11el  2134  po2nr  4326  sotric  4339  sotrieq  4340  tz7.7  4417  ordsucun  4615  fcof1o  5765  isocnv  5789  isores2  5792  isomin  5796  isoini  5797  f1oiso2  5811  ovmpt2df  5941  offval  6047  xp1st  6111  1stconst  6169  cnvf1olem  6178  fnse  6194  oalim  6527  omlim  6528  oaass  6555  omordi  6560  omwordri  6566  odi  6573  oen0  6580  oewordri  6586  nnawordi  6615  nnmordi  6625  omabs  6641  erinxp  6729  dom2lem  6897  mapen  7021  ssenen  7031  ssfi  7079  domfi  7080  domunfican  7125  ordtypelem6  7234  ordtypelem7  7235  card2inf  7265  inf3lem6  7330  cantnfle  7368  cantnflem1b  7384  cantnflem1  7387  mapfien  7395  wemapwe  7396  rankxplim3  7547  fseqenlem2  7648  dfac5lem4  7749  dfac2  7753  cfsuc  7879  cfflb  7881  cofsmo  7891  infpssrlem4  7928  fin4en1  7931  ssfin4  7932  fin23lem26  7947  fin23lem22  7949  fin23lem27  7950  isf34lem4  7999  isf34lem5  8000  fin1a2lem12  8033  axdc3lem2  8073  axdc4lem  8077  ttukeylem6  8137  iundom2g  8158  pwcfsdom  8201  gchen2  8244  gchor  8245  fpwwe2lem7  8254  fpwwe2lem9  8256  fpwwe2lem11  8258  fpwwe2lem12  8259  fpwwe2  8261  pwfseqlem4  8280  gchina  8317  ltexprlem6  8661  prlem936  8667  mul4  8977  2addsub  9061  muladd  9208  ltleadd  9253  leord1  9296  eqord1  9297  ltord2  9298  leord2  9299  eqord2  9300  divmul3  9425  divcan7  9465  divadddiv  9471  lemul2a  9607  lemul12b  9609  ltmuldiv2  9623  ltdivmul  9624  ledivmul  9625  ltdivmul2  9627  lt2mul2div  9628  ledivmul2  9629  lemuldiv2  9632  lt2msq  9636  ltdiv23  9643  lediv23  9644  supmullem1  9716  infmrcl  9729  cju  9738  zextlt  10082  suprzcl  10087  zmax  10309  xrlttr  10470  xrre3  10496  qbtwnre  10522  xrsupsslem  10621  xrinfmsslem  10622  supxrunb1  10634  supxrunb2  10635  ixxdisj  10667  iooshf  10724  icodisj  10757  iccf1o  10774  modid  10989  modadd1  10997  modmul1  10998  seqf1o  11083  expsub  11145  sqlecan  11205  bcval5  11326  hashmap  11383  hashfacen  11388  seqcoll  11397  resqreu  11734  lenegsq  11800  limsupbnd2  11953  icco1  12010  rlimresb  12035  rlimsqzlem  12118  rlimsqz  12119  rlimsqz2  12120  caucvgrlem  12141  fsum0diag2  12241  o1fsum  12267  incexclem  12291  ruclem8  12511  dvdsmulcr  12554  ndvdsadd  12603  bitsshft  12662  hashdvds  12839  eulerthlem2  12846  pcqmul  12902  pcmpt  12936  prmreclem3  12961  4sqlem11  12998  0ram  13063  ramub1  13071  invfun  13662  coaval  13896  catcisolem  13934  prfcl  13973  prf1st  13974  prf2nd  13975  1st2ndprf  13976  evlfcl  13992  curfuncf  14008  curf2ndf  14017  isposd  14085  lubun  14223  isacs3lem  14265  pslem  14311  psss  14319  spwpr4  14336  pwsdiagmhm  14441  gsumccat  14460  grpinvid1  14526  grpinvid2  14527  grplcan  14530  grplactcnv  14560  0nsg  14658  eqger  14663  resghm  14695  conjghm  14709  subgga  14750  gaorber  14758  gastacl  14759  orbsta  14763  odid  14849  odmulg  14865  gexid  14888  odcau  14911  lsmssv  14950  lsmcom2  14962  pj1ghm  15008  frgpuptf  15075  frgpup1  15080  ghmplusg  15134  cyggex2  15179  gsumval3eu  15186  gsumval3  15187  ablfac1eu  15304  pgpfac1lem5  15310  isdrngd  15533  issrngd  15622  lmhmf1o  15799  lmhmima  15800  lmhmpreima  15801  lspextmo  15809  lspdisj  15874  islbs3  15904  lbsextlem4  15910  drngnidl  15977  lidldvgen  16003  issubassa2  16080  psrbagconf1o  16116  evlslem2  16245  ply1sclf1  16360  cnsubrg  16428  znunit  16513  cygznlem3  16519  eltg2  16692  ntrss  16788  opncldf1  16817  ssnei2  16849  neindisj  16850  restopnb  16902  restntr  16908  tgcmp  17124  hauscmplem  17129  2ndc1stc  17173  2ndcdisj  17178  2ndcomap  17180  restlly  17205  lly1stc  17218  txcls  17295  txdis1cn  17325  pthaus  17328  txlm  17338  qtoptop2  17386  qtopomap  17405  kqt0lem  17423  pt1hmeo  17493  ptuncnv  17494  xkocnv  17501  fbasfip  17559  fgabs  17570  fbasrn  17575  elfm2  17639  fmfnfmlem2  17646  fmfnfmlem4  17648  ptcmplem3  17744  ptcmplem4  17745  tsmsres  17822  tsmsxplem1  17831  elbl2  17946  blin  17966  xmeter  17975  xmetresbl  17979  stdbdxmet  18057  metrest  18066  dscmet  18091  nrmmetd  18093  tngngp2  18164  nmoi2  18235  icccmplem2  18324  reconnlem2  18328  metdstri  18351  metdsle  18352  metdsre  18353  metnrmlem3  18361  fsumcn  18370  icccvx  18444  bndth  18452  evth  18453  reparphti  18491  pi1blem  18533  tchcph  18663  iscfil2  18688  cfilfcls  18696  iscau4  18701  iscauf  18702  caucfil  18705  cncmet  18740  minveclem7  18795  ovoliunlem1  18857  ovolicc2lem2  18873  ovolicc2lem3  18874  ovolicc2lem4  18875  ovolicc2lem5  18876  ovolicc2  18877  voliunlem3  18905  voliun  18907  ioombl  18918  volivth  18958  ismbfd  18991  ismbf3d  19005  itg1addlem1  19043  i1fadd  19046  itg1addlem4  19050  itg2seq  19093  itg2split  19100  itg2monolem1  19101  itg2gt0  19111  ibllem  19115  itgvallem3  19136  iblposlem  19142  dvmptfsum  19318  rolle  19333  dvlip  19336  c1liplem1  19339  lhop1  19357  lhop2  19358  dvcvx  19363  dvfsumge  19365  dvfsumrlimge0  19373  dvfsumrlim  19374  dvfsum2  19377  mdegaddle  19456  mdegvscale  19457  mdegmullem  19460  ply1divex  19518  coeeulem  19602  plyco  19619  dgrlt  19643  vieta1  19688  ulmss  19770  ulmdvlem3  19775  iblulm  19779  tanord  19896  eff1olem  19906  logdivlt  19968  logccv  20006  lawcos  20110  leibpilem1  20232  xrlimcnp  20259  cxp2limlem  20266  cxp2lim  20267  cxploglim2  20269  divsqrsumo1  20274  ftalem2  20307  sqff1o  20416  dvdsppwf1o  20422  dvdsflf1o  20423  musum  20427  muinv  20429  fsumdvdsmul  20431  sgmmul  20436  fsumvma  20448  logfac2  20452  chpchtsum  20454  logfacrlim  20459  logexprlim  20460  dchrelbas3  20473  dchrmulcl  20484  bposlem1  20519  lgsdchr  20583  lgsquadlem1  20589  lgsquadlem2  20590  lgsquad2lem2  20594  chebbnd1lem1  20614  chpchtlim  20624  rplogsumlem2  20630  dchrmusum2  20639  dchrvmasumlem1  20640  dchrvmasum2lem  20641  dchrvmasumlem2  20643  dchrvmasumlem3  20644  dchrvmasumiflem2  20647  dchrisum0flb  20655  dchrisum0fno1  20656  rpvmasum2  20657  dchrisum0re  20658  dchrisum0lem1  20661  dchrisum0lem2a  20662  dchrisum0lem2  20663  dchrisum0lem3  20664  rplogsum  20672  mulogsum  20677  mulog2sumlem2  20680  vmalogdivsum2  20683  2vmadivsumlem  20685  selberglem2  20691  selberg3lem1  20702  selberg4lem1  20705  selberg4  20706  pntrsumo1  20710  selberg34r  20716  pntrlog2bndlem1  20722  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntrlog2bndlem6  20728  pntibndlem3  20737  pntlemp  20755  ostthlem1  20772  ostth3  20783  grpoidinv  20869  grporcan  20882  grpoinvid1  20891  grpoinvid2  20892  grpolcan  20894  isgrp2d  20896  gxadd  20936  ablo4  20948  ghgrp  21029  nvsubadd  21207  nvabs  21233  sspph  21427  minvecolem7  21456  htthlem  21491  hvadd4  21611  hvaddsub4  21653  shscli  21892  pjspansn  22152  fh1  22193  fh2  22194  cm2j  22195  chscllem2  22213  spansncvi  22227  5oalem2  22230  5oalem5  22233  5oalem6  22234  3oalem2  22238  hoadd4  22360  cnvunop  22494  bralnfn  22524  eighmorth  22540  hmops  22596  hmopm  22597  adjlnop  22662  adjmul  22668  adjadd  22669  nmopcoi  22671  kbass5  22696  kbass6  22697  hstle  22806  stlesi  22817  mdsl0  22886  mdexchi  22911  atom1d  22929  superpos  22930  cvexchlem  22944  atomli  22958  atcvatlem  22961  chirredlem2  22967  chirredlem3  22968  atcvat4i  22973  mdsymlem1  22979  mdsymlem3  22981  mdsymlem5  22983  mdsymlem6  22984  sumdmdlem  22994  sumdmdlem2  22995  cdj1i  23009  ballotlemfc0  23047  ballotlemfcc  23048  derangenlem  23109  subfacp1lem3  23120  subfacp1lem5  23122  cvmliftmolem2  23220  cvmliftlem6  23228  cvmlift2lem5  23245  cvmlift2lem7  23247  cvmlift2lem9  23249  relexpadd  23442  dfon2lem6  23548  wfrlem3  23662  sltres  23721  axfelem18  23767  axlowdimlem15  23994  axlowdimlem16  23995  axcontlem10  24011  colinbtwnle  24151  onsuct0  24290  nndivsub  24306  dfoprab4pop  24447  npincppr  24570  preotr2  24646  fprodadd  24763  gapm2  24780  mulinvsca  24891  truni3  24918  limptlimpr  24987  mulmulvec  25098  iepiclem  25234  cmp2morp  25369  rocatval  25370  finminlem  25642  nn0prpwlem  25649  isfne  25679  isref  25690  islocfin  25707  comppfsc  25718  neibastop1  25719  neibastop2lem  25720  neibastop3  25722  tailfb  25737  frinfm  25827  filbcmb  25843  seqpo  25868  sstotbnd2  25909  isbndx  25917  ssbnd  25923  prdsbnd  25928  ismtycnv  25937  ismtyres  25943  heiborlem3  25948  heibor  25956  ghomdiv  25985  grpokerinj  25986  isdrngo2  26000  rngohomco  26016  rngoisocnv  26023  rngoisoco  26024  crngm4  26039  crngohomfo  26042  isidlc  26051  ispridl2  26074  ispridlc  26106  prtlem16  26148  ismrc  26187  eldioph2  26252  lzenom  26260  rexrabdioph  26286  fphpdo  26311  irrapxlem3  26320  elpell14qr2  26358  pell14qrreccl  26360  pell14qrdich  26365  pellfundglb  26381  monotoddzzfi  26438  2nn0ind  26441  jm2.21  26498  jm2.22  26499  dnnumch3  26555  dnwech  26556  fnwe2lem2  26559  pwssplit2  26600  pwssplit3  26601  dsmmsubg  26620  dsmmlss  26621  frlmsslsp  26659  frlmup1  26661  lindfrn  26702  f1lindf  26703  hbtlem6  26744  psgnunilem2  26829  mamuass  26871  phisum  26929  stoweidlem34  27194  stoweidlem48  27208  bnj607  28227  lubunNEW  28442  lshpcmp  28457  omllaw3  28714  omlfh1N  28727  cvratlem  28889  cvrat3  28910  cvrat4  28911  ps-2  28946  elpaddn0  29268  paddasslem10  29297  cdleme0cp  29682  cdleme32a  29909  cdlemeg49lebilem  30007  cdleme50eq  30009  tendoeq2  30242  diaglbN  30524  diameetN  30525  diainN  30526  dvhopN  30585  djaclN  30605  djajN  30606  dihopelvalcpre  30717  dih1dimatlem  30798  dihmeetcl  30814  djhcl  30869  mapdpglem2  31142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator