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  2031  ax11eq  2134  ax11el  2135  po2nr  4329  sotric  4342  sotrieq  4343  tz7.7  4420  ordsucun  4618  fcof1o  5805  isocnv  5829  isores2  5832  isomin  5836  isoini  5837  f1oiso2  5851  ovmpt2df  5981  offval  6087  xp1st  6151  1stconst  6209  cnvf1olem  6218  fnse  6234  oalim  6533  omlim  6534  oaass  6561  omordi  6566  omwordri  6572  odi  6579  oen0  6586  oewordri  6592  nnawordi  6621  nnmordi  6631  omabs  6647  erinxp  6735  dom2lem  6903  mapen  7027  ssenen  7037  ssfi  7085  domfi  7086  domunfican  7131  ordtypelem6  7240  ordtypelem7  7241  card2inf  7271  inf3lem6  7336  cantnfle  7374  cantnflem1b  7390  cantnflem1  7393  mapfien  7401  wemapwe  7402  rankxplim3  7553  fseqenlem2  7654  dfac5lem4  7755  dfac2  7759  cfsuc  7885  cfflb  7887  cofsmo  7897  infpssrlem4  7934  fin4en1  7937  ssfin4  7938  fin23lem26  7953  fin23lem22  7955  fin23lem27  7956  isf34lem4  8005  isf34lem5  8006  fin1a2lem12  8039  axdc3lem2  8079  axdc4lem  8083  ttukeylem6  8143  iundom2g  8164  pwcfsdom  8207  gchen2  8250  gchor  8251  fpwwe2lem7  8260  fpwwe2lem9  8262  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2  8267  pwfseqlem4  8286  gchina  8323  ltexprlem6  8667  prlem936  8673  mul4  8983  2addsub  9067  muladd  9214  ltleadd  9259  leord1  9302  eqord1  9303  ltord2  9304  leord2  9305  eqord2  9306  divmul3  9431  divcan7  9471  divadddiv  9477  lemul2a  9613  lemul12b  9615  ltmuldiv2  9629  ltdivmul  9630  ledivmul  9631  ltdivmul2  9633  lt2mul2div  9634  ledivmul2  9635  lemuldiv2  9638  lt2msq  9642  ltdiv23  9649  lediv23  9650  supmullem1  9722  infmrcl  9735  cju  9744  zextlt  10088  suprzcl  10093  zmax  10315  xrlttr  10476  xrre3  10502  qbtwnre  10528  xrsupsslem  10627  xrinfmsslem  10628  supxrunb1  10640  supxrunb2  10641  ixxdisj  10673  iooshf  10730  icodisj  10763  iccf1o  10780  modid  10995  modadd1  11003  modmul1  11004  seqf1o  11089  expsub  11151  sqlecan  11211  bcval5  11332  hashmap  11389  hashfacen  11394  seqcoll  11403  resqreu  11740  lenegsq  11806  limsupbnd2  11959  icco1  12016  rlimresb  12041  rlimsqzlem  12124  rlimsqz  12125  rlimsqz2  12126  caucvgrlem  12147  fsum0diag2  12247  o1fsum  12273  incexclem  12297  ruclem8  12517  dvdsmulcr  12560  ndvdsadd  12609  bitsshft  12668  hashdvds  12845  eulerthlem2  12852  pcqmul  12908  pcmpt  12942  prmreclem3  12967  4sqlem11  13004  0ram  13069  ramub1  13077  invfun  13668  coaval  13902  catcisolem  13940  prfcl  13979  prf1st  13980  prf2nd  13981  1st2ndprf  13982  evlfcl  13998  curfuncf  14014  curf2ndf  14023  isposd  14091  lubun  14229  isacs3lem  14271  pslem  14317  psss  14325  spwpr4  14342  pwsdiagmhm  14447  gsumccat  14466  grpinvid1  14532  grpinvid2  14533  grplcan  14536  grplactcnv  14566  0nsg  14664  eqger  14669  resghm  14701  conjghm  14715  subgga  14756  gaorber  14764  gastacl  14765  orbsta  14769  odid  14855  odmulg  14871  gexid  14894  odcau  14917  lsmssv  14956  lsmcom2  14968  pj1ghm  15014  frgpuptf  15081  frgpup1  15086  ghmplusg  15140  cyggex2  15185  gsumval3eu  15192  gsumval3  15193  ablfac1eu  15310  pgpfac1lem5  15316  isdrngd  15539  issrngd  15628  lmhmf1o  15805  lmhmima  15806  lmhmpreima  15807  lspextmo  15815  lspdisj  15880  islbs3  15910  lbsextlem4  15916  drngnidl  15983  lidldvgen  16009  issubassa2  16086  psrbagconf1o  16122  evlslem2  16251  ply1sclf1  16366  cnsubrg  16434  znunit  16519  cygznlem3  16525  eltg2  16698  ntrss  16794  opncldf1  16823  ssnei2  16855  neindisj  16856  restopnb  16908  restntr  16914  tgcmp  17130  hauscmplem  17135  2ndc1stc  17179  2ndcdisj  17184  2ndcomap  17186  restlly  17211  lly1stc  17224  txcls  17301  txdis1cn  17331  pthaus  17334  txlm  17344  qtoptop2  17392  qtopomap  17411  kqt0lem  17429  pt1hmeo  17499  ptuncnv  17500  xkocnv  17507  fbasfip  17565  fgabs  17576  fbasrn  17581  elfm2  17645  fmfnfmlem2  17652  fmfnfmlem4  17654  ptcmplem3  17750  ptcmplem4  17751  tsmsres  17828  tsmsxplem1  17837  elbl2  17952  blin  17972  xmeter  17981  xmetresbl  17985  stdbdxmet  18063  metrest  18072  dscmet  18097  nrmmetd  18099  tngngp2  18170  nmoi2  18241  icccmplem2  18330  reconnlem2  18334  metdstri  18357  metdsle  18358  metdsre  18359  metnrmlem3  18367  fsumcn  18376  icccvx  18450  bndth  18458  evth  18459  reparphti  18497  pi1blem  18539  tchcph  18669  iscfil2  18694  cfilfcls  18702  iscau4  18707  iscauf  18708  caucfil  18711  cncmet  18746  minveclem7  18801  ovoliunlem1  18863  ovolicc2lem2  18879  ovolicc2lem3  18880  ovolicc2lem4  18881  ovolicc2lem5  18882  ovolicc2  18883  voliunlem3  18911  voliun  18913  ioombl  18924  volivth  18964  ismbfd  18997  ismbf3d  19011  itg1addlem1  19049  i1fadd  19052  itg1addlem4  19056  itg2seq  19099  itg2split  19106  itg2monolem1  19107  itg2gt0  19117  ibllem  19121  itgvallem3  19142  iblposlem  19148  dvmptfsum  19324  rolle  19339  dvlip  19342  c1liplem1  19345  lhop1  19363  lhop2  19364  dvcvx  19369  dvfsumge  19371  dvfsumrlimge0  19379  dvfsumrlim  19380  dvfsum2  19383  mdegaddle  19462  mdegvscale  19463  mdegmullem  19466  ply1divex  19524  coeeulem  19608  plyco  19625  dgrlt  19649  vieta1  19694  ulmss  19776  ulmdvlem3  19781  iblulm  19785  tanord  19902  eff1olem  19912  logdivlt  19974  logccv  20012  lawcos  20116  leibpilem1  20238  xrlimcnp  20265  cxp2limlem  20272  cxp2lim  20273  cxploglim2  20275  divsqrsumo1  20280  ftalem2  20313  sqff1o  20422  dvdsppwf1o  20428  dvdsflf1o  20429  musum  20433  muinv  20435  fsumdvdsmul  20437  sgmmul  20442  fsumvma  20454  logfac2  20458  chpchtsum  20460  logfacrlim  20465  logexprlim  20466  dchrelbas3  20479  dchrmulcl  20490  bposlem1  20525  lgsdchr  20589  lgsquadlem1  20595  lgsquadlem2  20596  lgsquad2lem2  20600  chebbnd1lem1  20620  chpchtlim  20630  rplogsumlem2  20636  dchrmusum2  20645  dchrvmasumlem1  20646  dchrvmasum2lem  20647  dchrvmasumlem2  20649  dchrvmasumlem3  20650  dchrvmasumiflem2  20653  dchrisum0flb  20661  dchrisum0fno1  20662  rpvmasum2  20663  dchrisum0re  20664  dchrisum0lem1  20667  dchrisum0lem2a  20668  dchrisum0lem2  20669  dchrisum0lem3  20670  rplogsum  20678  mulogsum  20683  mulog2sumlem2  20686  vmalogdivsum2  20689  2vmadivsumlem  20691  selberglem2  20697  selberg3lem1  20708  selberg4lem1  20711  selberg4  20712  pntrsumo1  20716  selberg34r  20722  pntrlog2bndlem1  20728  pntrlog2bndlem2  20729  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntrlog2bndlem5  20732  pntrlog2bndlem6  20734  pntibndlem3  20743  pntlemp  20761  ostthlem1  20778  ostth3  20789  grpoidinv  20877  grporcan  20890  grpoinvid1  20899  grpoinvid2  20900  grpolcan  20902  isgrp2d  20904  gxadd  20944  ablo4  20956  ghgrp  21037  nvsubadd  21215  nvabs  21241  sspph  21435  minvecolem7  21464  htthlem  21499  hvadd4  21617  hvaddsub4  21659  shscli  21898  pjspansn  22158  fh1  22199  fh2  22200  cm2j  22201  chscllem2  22219  spansncvi  22233  5oalem2  22236  5oalem5  22239  5oalem6  22240  3oalem2  22244  hoadd4  22366  cnvunop  22500  bralnfn  22530  eighmorth  22546  hmops  22602  hmopm  22603  adjlnop  22668  adjmul  22674  adjadd  22675  nmopcoi  22677  kbass5  22702  kbass6  22703  hstle  22812  stlesi  22823  mdsl0  22892  mdexchi  22917  atom1d  22935  superpos  22936  cvexchlem  22950  atomli  22964  atcvatlem  22967  chirredlem2  22973  chirredlem3  22974  atcvat4i  22979  mdsymlem1  22985  mdsymlem3  22987  mdsymlem5  22989  mdsymlem6  22990  sumdmdlem  23000  sumdmdlem2  23001  cdj1i  23015  ballotlemfc0  23053  ballotlemfcc  23054  itgeq12dv  23198  isoun  23244  xrre3FL  23253  cntmeas  23555  indf1ofs  23611  derangenlem  23704  subfacp1lem3  23715  subfacp1lem5  23717  cvmliftmolem2  23815  cvmliftlem6  23823  cvmlift2lem5  23840  cvmlift2lem7  23842  cvmlift2lem9  23844  relexpadd  24037  dfon2lem6  24146  wfrlem3  24260  sltres  24320  axlowdimlem15  24586  axlowdimlem16  24587  axcontlem10  24603  colinbtwnle  24743  onsuct0  24882  nndivsub  24898  supadd  24928  dfoprab4pop  25048  npincppr  25170  preotr2  25246  fprodadd  25363  gapm2  25380  mulinvsca  25491  truni3  25518  limptlimpr  25587  mulmulvec  25698  iepiclem  25834  cmp2morp  25969  rocatval  25970  finminlem  26242  nn0prpwlem  26249  isfne  26279  isref  26290  islocfin  26307  comppfsc  26318  neibastop1  26319  neibastop2lem  26320  neibastop3  26322  tailfb  26337  frinfm  26427  filbcmb  26443  seqpo  26468  sstotbnd2  26509  isbndx  26517  ssbnd  26523  prdsbnd  26528  ismtycnv  26537  ismtyres  26543  heiborlem3  26548  heibor  26556  ghomdiv  26585  grpokerinj  26586  isdrngo2  26600  rngohomco  26616  rngoisocnv  26623  rngoisoco  26624  crngm4  26639  crngohomfo  26642  isidlc  26651  ispridl2  26674  ispridlc  26706  prtlem16  26748  ismrc  26787  eldioph2  26852  lzenom  26860  rexrabdioph  26886  fphpdo  26911  irrapxlem3  26920  elpell14qr2  26958  pell14qrreccl  26960  pell14qrdich  26965  pellfundglb  26981  monotoddzzfi  27038  2nn0ind  27041  jm2.21  27098  jm2.22  27099  dnnumch3  27155  dnwech  27156  fnwe2lem2  27159  pwssplit2  27200  pwssplit3  27201  dsmmsubg  27220  dsmmlss  27221  frlmsslsp  27259  frlmup1  27261  lindfrn  27302  f1lindf  27303  hbtlem6  27344  psgnunilem2  27429  mamuass  27471  phisum  27529  stoweidlem34  27794  stoweidlem48  27808  mpt2xopoveq  28096  bnj607  29021  lubunNEW  29236  lshpcmp  29251  omllaw3  29508  omlfh1N  29521  cvratlem  29683  cvrat3  29704  cvrat4  29705  ps-2  29740  elpaddn0  30062  paddasslem10  30091  cdleme0cp  30476  cdleme32a  30703  cdlemeg49lebilem  30801  cdleme50eq  30803  tendoeq2  31036  diaglbN  31318  diameetN  31319  diainN  31320  dvhopN  31379  djaclN  31399  djajN  31400  dihopelvalcpre  31511  dih1dimatlem  31592  dihmeetcl  31608  djhcl  31663  mapdpglem2  31936
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