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  2042  ax11eq  2145  ax11el  2146  po2nr  4343  sotric  4356  sotrieq  4357  tz7.7  4434  ordsucun  4632  fcof1o  5819  isocnv  5843  isores2  5846  isomin  5850  isoini  5851  f1oiso2  5865  ovmpt2df  5995  offval  6101  xp1st  6165  1stconst  6223  cnvf1olem  6232  fnse  6248  oalim  6547  omlim  6548  oaass  6575  omordi  6580  omwordri  6586  odi  6593  oen0  6600  oewordri  6606  nnawordi  6635  nnmordi  6645  omabs  6661  erinxp  6749  dom2lem  6917  mapen  7041  ssenen  7051  ssfi  7099  domfi  7100  domunfican  7145  ordtypelem6  7254  ordtypelem7  7255  card2inf  7285  inf3lem6  7350  cantnfle  7388  cantnflem1b  7404  cantnflem1  7407  mapfien  7415  wemapwe  7416  rankxplim3  7567  fseqenlem2  7668  dfac5lem4  7769  dfac2  7773  cfsuc  7899  cfflb  7901  cofsmo  7911  infpssrlem4  7948  fin4en1  7951  ssfin4  7952  fin23lem26  7967  fin23lem22  7969  fin23lem27  7970  isf34lem4  8019  isf34lem5  8020  fin1a2lem12  8053  axdc3lem2  8093  axdc4lem  8097  ttukeylem6  8157  iundom2g  8178  pwcfsdom  8221  gchen2  8264  gchor  8265  fpwwe2lem7  8274  fpwwe2lem9  8276  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2  8281  pwfseqlem4  8300  gchina  8337  ltexprlem6  8681  prlem936  8687  mul4  8997  2addsub  9081  muladd  9228  ltleadd  9273  leord1  9316  eqord1  9317  ltord2  9318  leord2  9319  eqord2  9320  divmul3  9445  divcan7  9485  divadddiv  9491  lemul2a  9627  lemul12b  9629  ltmuldiv2  9643  ltdivmul  9644  ledivmul  9645  ltdivmul2  9647  lt2mul2div  9648  ledivmul2  9649  lemuldiv2  9652  lt2msq  9656  ltdiv23  9663  lediv23  9664  supmullem1  9736  infmrcl  9749  cju  9758  zextlt  10102  suprzcl  10107  zmax  10329  xrlttr  10490  xrre3  10516  qbtwnre  10542  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  ixxdisj  10687  iooshf  10744  icodisj  10777  iccf1o  10794  modid  11009  modadd1  11017  modmul1  11018  seqf1o  11103  expsub  11165  sqlecan  11225  bcval5  11346  hashmap  11403  hashfacen  11408  seqcoll  11417  resqreu  11754  lenegsq  11820  limsupbnd2  11973  icco1  12030  rlimresb  12055  rlimsqzlem  12138  rlimsqz  12139  rlimsqz2  12140  caucvgrlem  12161  fsum0diag2  12261  o1fsum  12287  incexclem  12311  ruclem8  12531  dvdsmulcr  12574  ndvdsadd  12623  bitsshft  12682  hashdvds  12859  eulerthlem2  12866  pcqmul  12922  pcmpt  12956  prmreclem3  12981  4sqlem11  13018  0ram  13083  ramub1  13091  invfun  13682  coaval  13916  catcisolem  13954  prfcl  13993  prf1st  13994  prf2nd  13995  1st2ndprf  13996  evlfcl  14012  curfuncf  14028  curf2ndf  14037  isposd  14105  lubun  14243  isacs3lem  14285  pslem  14331  psss  14339  spwpr4  14356  pwsdiagmhm  14461  gsumccat  14480  grpinvid1  14546  grpinvid2  14547  grplcan  14550  grplactcnv  14580  0nsg  14678  eqger  14683  resghm  14715  conjghm  14729  subgga  14770  gaorber  14778  gastacl  14779  orbsta  14783  odid  14869  odmulg  14885  gexid  14908  odcau  14931  lsmssv  14970  lsmcom2  14982  pj1ghm  15028  frgpuptf  15095  frgpup1  15100  ghmplusg  15154  cyggex2  15199  gsumval3eu  15206  gsumval3  15207  ablfac1eu  15324  pgpfac1lem5  15330  isdrngd  15553  issrngd  15642  lmhmf1o  15819  lmhmima  15820  lmhmpreima  15821  lspextmo  15829  lspdisj  15894  islbs3  15924  lbsextlem4  15930  drngnidl  15997  lidldvgen  16023  issubassa2  16100  psrbagconf1o  16136  evlslem2  16265  ply1sclf1  16380  cnsubrg  16448  znunit  16533  cygznlem3  16539  eltg2  16712  ntrss  16808  opncldf1  16837  ssnei2  16869  neindisj  16870  restopnb  16922  restntr  16928  tgcmp  17144  hauscmplem  17149  2ndc1stc  17193  2ndcdisj  17198  2ndcomap  17200  restlly  17225  lly1stc  17238  txcls  17315  txdis1cn  17345  pthaus  17348  txlm  17358  qtoptop2  17406  qtopomap  17425  kqt0lem  17443  pt1hmeo  17513  ptuncnv  17514  xkocnv  17521  fbasfip  17579  fgabs  17590  fbasrn  17595  elfm2  17659  fmfnfmlem2  17666  fmfnfmlem4  17668  ptcmplem3  17764  ptcmplem4  17765  tsmsres  17842  tsmsxplem1  17851  elbl2  17966  blin  17986  xmeter  17995  xmetresbl  17999  stdbdxmet  18077  metrest  18086  dscmet  18111  nrmmetd  18113  tngngp2  18184  nmoi2  18255  icccmplem2  18344  reconnlem2  18348  metdstri  18371  metdsle  18372  metdsre  18373  metnrmlem3  18381  fsumcn  18390  icccvx  18464  bndth  18472  evth  18473  reparphti  18511  pi1blem  18553  tchcph  18683  iscfil2  18708  cfilfcls  18716  iscau4  18721  iscauf  18722  caucfil  18725  cncmet  18760  minveclem7  18815  ovoliunlem1  18877  ovolicc2lem2  18893  ovolicc2lem3  18894  ovolicc2lem4  18895  ovolicc2lem5  18896  ovolicc2  18897  voliunlem3  18925  voliun  18927  ioombl  18938  volivth  18978  ismbfd  19011  ismbf3d  19025  itg1addlem1  19063  i1fadd  19066  itg1addlem4  19070  itg2seq  19113  itg2split  19120  itg2monolem1  19121  itg2gt0  19131  ibllem  19135  itgvallem3  19156  iblposlem  19162  dvmptfsum  19338  rolle  19353  dvlip  19356  c1liplem1  19359  lhop1  19377  lhop2  19378  dvcvx  19383  dvfsumge  19385  dvfsumrlimge0  19393  dvfsumrlim  19394  dvfsum2  19397  mdegaddle  19476  mdegvscale  19477  mdegmullem  19480  ply1divex  19538  coeeulem  19622  plyco  19639  dgrlt  19663  vieta1  19708  ulmss  19790  ulmdvlem3  19795  iblulm  19799  tanord  19916  eff1olem  19926  logdivlt  19988  logccv  20026  lawcos  20130  leibpilem1  20252  xrlimcnp  20279  cxp2limlem  20286  cxp2lim  20287  cxploglim2  20289  divsqrsumo1  20294  ftalem2  20327  sqff1o  20436  dvdsppwf1o  20442  dvdsflf1o  20443  musum  20447  muinv  20449  fsumdvdsmul  20451  sgmmul  20456  fsumvma  20468  logfac2  20472  chpchtsum  20474  logfacrlim  20479  logexprlim  20480  dchrelbas3  20493  dchrmulcl  20504  bposlem1  20539  lgsdchr  20603  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2lem2  20614  chebbnd1lem1  20634  chpchtlim  20644  rplogsumlem2  20650  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrvmasumiflem2  20667  dchrisum0flb  20675  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  rplogsum  20692  mulogsum  20697  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  selberglem2  20711  selberg3lem1  20722  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  selberg34r  20736  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntibndlem3  20757  pntlemp  20775  ostthlem1  20792  ostth3  20803  grpoidinv  20891  grporcan  20904  grpoinvid1  20913  grpoinvid2  20914  grpolcan  20916  isgrp2d  20918  gxadd  20958  ablo4  20970  ghgrp  21051  nvsubadd  21229  nvabs  21255  sspph  21449  minvecolem7  21478  htthlem  21513  hvadd4  21631  hvaddsub4  21673  shscli  21912  pjspansn  22172  fh1  22213  fh2  22214  cm2j  22215  chscllem2  22233  spansncvi  22247  5oalem2  22250  5oalem5  22253  5oalem6  22254  3oalem2  22258  hoadd4  22380  cnvunop  22514  bralnfn  22544  eighmorth  22560  hmops  22616  hmopm  22617  adjlnop  22682  adjmul  22688  adjadd  22689  nmopcoi  22691  kbass5  22716  kbass6  22717  hstle  22826  stlesi  22837  mdsl0  22906  mdexchi  22931  atom1d  22949  superpos  22950  cvexchlem  22964  atomli  22978  atcvatlem  22981  chirredlem2  22987  chirredlem3  22988  atcvat4i  22993  mdsymlem1  22999  mdsymlem3  23001  mdsymlem5  23003  mdsymlem6  23004  sumdmdlem  23014  sumdmdlem2  23015  cdj1i  23029  ballotlemfc0  23067  ballotlemfcc  23068  itgeq12dv  23211  isoun  23257  xrre3FL  23266  cntmeas  23568  indf1ofs  23624  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  cvmliftmolem2  23828  cvmliftlem6  23836  cvmlift2lem5  23853  cvmlift2lem7  23855  cvmlift2lem9  23857  relexpadd  24050  dfon2lem6  24215  wfrlem3  24329  sltres  24389  axlowdimlem15  24656  axlowdimlem16  24657  axcontlem10  24673  colinbtwnle  24813  onsuct0  24952  nndivsub  24968  supadd  24996  bddiblnc  25021  dfoprab4pop  25140  npincppr  25262  preotr2  25338  fprodadd  25455  gapm2  25472  mulinvsca  25583  truni3  25610  limptlimpr  25679  mulmulvec  25790  iepiclem  25926  cmp2morp  26061  rocatval  26062  finminlem  26334  nn0prpwlem  26341  isfne  26371  isref  26382  islocfin  26399  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  neibastop3  26414  tailfb  26429  frinfm  26519  filbcmb  26535  seqpo  26560  sstotbnd2  26601  isbndx  26609  ssbnd  26615  prdsbnd  26620  ismtycnv  26629  ismtyres  26635  heiborlem3  26640  heibor  26648  ghomdiv  26677  grpokerinj  26678  isdrngo2  26692  rngohomco  26708  rngoisocnv  26715  rngoisoco  26716  crngm4  26731  crngohomfo  26734  isidlc  26743  ispridl2  26766  ispridlc  26798  prtlem16  26840  ismrc  26879  eldioph2  26944  lzenom  26952  rexrabdioph  26978  fphpdo  27003  irrapxlem3  27012  elpell14qr2  27050  pell14qrreccl  27052  pell14qrdich  27057  pellfundglb  27073  monotoddzzfi  27130  2nn0ind  27133  jm2.21  27190  jm2.22  27191  dnnumch3  27247  dnwech  27248  fnwe2lem2  27251  pwssplit2  27292  pwssplit3  27293  dsmmsubg  27312  dsmmlss  27313  frlmsslsp  27351  frlmup1  27353  lindfrn  27394  f1lindf  27395  hbtlem6  27436  psgnunilem2  27521  mamuass  27563  phisum  27621  stoweidlem34  27886  stoweidlem48  27900  mpt2xopoveq  28201  bnj607  29264  sbcomwAUX7  29562  sbcomOLD7  29709  lubunNEW  29785  lshpcmp  29800  omllaw3  30057  omlfh1N  30070  cvratlem  30232  cvrat3  30253  cvrat4  30254  ps-2  30289  elpaddn0  30611  paddasslem10  30640  cdleme0cp  31025  cdleme32a  31252  cdlemeg49lebilem  31350  cdleme50eq  31352  tendoeq2  31585  diaglbN  31867  diameetN  31868  diainN  31869  dvhopN  31928  djaclN  31948  djajN  31949  dihopelvalcpre  32060  dih1dimatlem  32141  dihmeetcl  32157  djhcl  32212  mapdpglem2  32485
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