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  1121  sbcom  2102  ax11eq  2206  ax11el  2207  po2nr  4430  sotric  4443  sotrieq  4444  tz7.7  4521  ordsucun  4719  fvtp1g  5842  fcof1o  5926  isocnv  5950  isores2  5953  isomin  5957  isoini  5958  f1oiso2  5972  ovmpt2df  6105  offval  6212  xp1st  6276  1stconst  6335  cnvf1olem  6344  fnse  6360  mpt2xopoveq  6367  oalim  6673  omlim  6674  oaass  6701  omordi  6706  omwordri  6712  odi  6719  oen0  6726  oewordri  6732  nnawordi  6761  nnmordi  6771  omabs  6787  erinxp  6875  dom2lem  7044  mapen  7168  ssenen  7178  ssfi  7226  domfi  7227  domunfican  7276  ordtypelem6  7385  ordtypelem7  7386  card2inf  7416  inf3lem6  7481  cantnfle  7519  cantnflem1b  7535  cantnflem1  7538  mapfien  7546  wemapwe  7547  rankxplim3  7698  fseqenlem2  7799  dfac5lem4  7900  dfac2  7904  cfsuc  8030  cfflb  8032  cofsmo  8042  infpssrlem4  8079  fin4en1  8082  ssfin4  8083  fin23lem26  8098  fin23lem22  8100  fin23lem27  8101  isf34lem4  8150  isf34lem5  8151  fin1a2lem12  8184  axdc3lem2  8224  axdc4lem  8228  ttukeylem6  8288  iundom2g  8309  pwcfsdom  8352  gchen2  8395  gchor  8396  fpwwe2lem7  8405  fpwwe2lem9  8407  fpwwe2lem11  8409  fpwwe2lem12  8410  fpwwe2  8412  pwfseqlem4  8431  gchina  8468  ltexprlem6  8812  prlem936  8818  mul4  9128  2addsub  9212  muladd  9359  ltleadd  9404  leord1  9447  eqord1  9448  ltord2  9449  leord2  9450  eqord2  9451  divmul3  9576  divcan7  9616  divadddiv  9622  lemul2a  9758  lemul12b  9760  ltmuldiv2  9774  ltdivmul  9775  ledivmul  9776  ltdivmul2  9778  lt2mul2div  9779  ledivmul2  9780  lemuldiv2  9783  lt2msq  9787  ltdiv23  9794  lediv23  9795  supmullem1  9867  infmrcl  9880  cju  9889  zextlt  10237  suprzcl  10242  zmax  10464  xrlttr  10626  xrre3  10652  qbtwnre  10678  xrsupsslem  10778  xrinfmsslem  10779  supxrunb1  10791  supxrunb2  10792  ixxdisj  10824  iooshf  10881  icodisj  10914  iccf1o  10931  modid  11157  modadd1  11165  modmul1  11166  seqf1o  11251  expsub  11314  sqlecan  11374  bcval5  11496  hashmap  11585  hashfacen  11590  seqcoll  11599  resqreu  11945  lenegsq  12011  limsupbnd2  12164  icco1  12221  rlimresb  12246  rlimsqzlem  12329  rlimsqz  12330  rlimsqz2  12331  caucvgrlem  12353  fsum0diag2  12453  o1fsum  12479  incexclem  12503  ruclem8  12723  dvdsmulcr  12766  ndvdsadd  12815  bitsshft  12874  hashdvds  13051  eulerthlem2  13058  pcqmul  13114  pcmpt  13148  prmreclem3  13173  4sqlem11  13210  0ram  13275  ramub1  13283  invfun  13876  coaval  14110  catcisolem  14148  prfcl  14187  prf1st  14188  prf2nd  14189  1st2ndprf  14190  evlfcl  14206  curfuncf  14222  curf2ndf  14231  isposd  14299  lubun  14437  isacs3lem  14479  pslem  14525  psss  14533  spwpr4  14550  pwsdiagmhm  14655  gsumccat  14674  grpinvid1  14740  grpinvid2  14741  grplcan  14744  grplactcnv  14774  0nsg  14872  eqger  14877  resghm  14909  conjghm  14923  subgga  14964  gaorber  14972  gastacl  14973  orbsta  14977  odid  15063  odmulg  15079  gexid  15102  odcau  15125  lsmssv  15164  lsmcom2  15176  pj1ghm  15222  frgpuptf  15289  frgpup1  15294  ghmplusg  15348  cyggex2  15393  gsumval3eu  15400  gsumval3  15401  ablfac1eu  15518  pgpfac1lem5  15524  isdrngd  15747  issrngd  15836  lmhmf1o  16013  lmhmima  16014  lmhmpreima  16015  lspextmo  16023  lspdisj  16088  islbs3  16118  lbsextlem4  16124  drngnidl  16191  lidldvgen  16217  issubassa2  16294  psrbagconf1o  16330  evlslem2  16459  ply1sclf1  16574  cnsubrg  16649  znunit  16734  cygznlem3  16740  eltg2  16913  ntrss  17009  opncldf1  17038  ssnei2  17070  neindisj  17071  restopnb  17123  restntr  17129  tgcmp  17345  hauscmplem  17350  2ndc1stc  17394  2ndcdisj  17399  2ndcomap  17401  restlly  17426  lly1stc  17439  txcls  17516  txdis1cn  17546  pthaus  17549  txlm  17559  qtoptop2  17607  qtopomap  17626  kqt0lem  17644  pt1hmeo  17714  ptuncnv  17715  xkocnv  17722  fbasfip  17776  fgabs  17787  fbasrn  17792  elfm2  17856  fmfnfmlem2  17863  fmfnfmlem4  17865  ptcmplem3  17961  ptcmplem4  17962  tsmsres  18039  tsmsxplem1  18048  elbl2  18163  blin  18183  xmeter  18192  xmetresbl  18196  stdbdxmet  18274  metrest  18283  dscmet  18308  nrmmetd  18310  tngngp2  18381  nmoi2  18452  icccmplem2  18542  reconnlem2  18546  metdstri  18569  metdsle  18570  metdsre  18571  metnrmlem3  18579  fsumcn  18588  icccvx  18663  bndth  18671  evth  18672  reparphti  18710  pi1blem  18752  tchcph  18882  iscfil2  18907  cfilfcls  18915  iscau4  18920  iscauf  18921  caucfil  18924  cncmet  18959  minveclem7  19014  ovoliunlem1  19076  ovolicc2lem2  19092  ovolicc2lem3  19093  ovolicc2lem4  19094  ovolicc2lem5  19095  ovolicc2  19096  voliunlem3  19124  voliun  19126  ioombl  19137  volivth  19177  ismbfd  19210  ismbf3d  19224  itg1addlem1  19262  i1fadd  19265  itg1addlem4  19269  itg2seq  19312  itg2split  19319  itg2monolem1  19320  itg2gt0  19330  ibllem  19334  itgvallem3  19355  iblposlem  19361  dvmptfsum  19537  rolle  19552  dvlip  19555  c1liplem1  19558  lhop1  19576  lhop2  19577  dvcvx  19582  dvfsumge  19584  dvfsumrlimge0  19592  dvfsumrlim  19593  dvfsum2  19596  mdegaddle  19675  mdegvscale  19676  mdegmullem  19679  ply1divex  19737  coeeulem  19821  plyco  19838  dgrlt  19862  vieta1  19907  ulmss  19991  ulmdvlem3  19996  iblulm  20001  tanord  20118  eff1olem  20128  logdivlt  20194  logccv  20232  lawcos  20336  leibpilem1  20458  xrlimcnp  20485  cxp2limlem  20492  cxp2lim  20493  cxploglim2  20495  divsqrsumo1  20500  ftalem2  20534  sqff1o  20643  dvdsppwf1o  20649  dvdsflf1o  20650  musum  20654  muinv  20656  fsumdvdsmul  20658  sgmmul  20663  fsumvma  20675  logfac2  20679  chpchtsum  20681  logfacrlim  20686  logexprlim  20687  dchrelbas3  20700  dchrmulcl  20711  bposlem1  20746  lgsdchr  20810  lgsquadlem1  20816  lgsquadlem2  20817  lgsquad2lem2  20821  chebbnd1lem1  20841  chpchtlim  20851  rplogsumlem2  20857  dchrmusum2  20866  dchrvmasumlem1  20867  dchrvmasum2lem  20868  dchrvmasumlem2  20870  dchrvmasumlem3  20871  dchrvmasumiflem2  20874  dchrisum0flb  20882  dchrisum0fno1  20883  rpvmasum2  20884  dchrisum0re  20885  dchrisum0lem1  20888  dchrisum0lem2a  20889  dchrisum0lem2  20890  dchrisum0lem3  20891  rplogsum  20899  mulogsum  20904  mulog2sumlem2  20907  vmalogdivsum2  20910  2vmadivsumlem  20912  selberglem2  20918  selberg3lem1  20929  selberg4lem1  20932  selberg4  20933  pntrsumo1  20937  selberg34r  20943  pntrlog2bndlem1  20949  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem4  20952  pntrlog2bndlem5  20953  pntrlog2bndlem6  20955  pntibndlem3  20964  pntlemp  20982  ostthlem1  20999  ostth3  21010  usgrasscusgra  21162  grpoidinv  21307  grporcan  21320  grpoinvid1  21329  grpoinvid2  21330  grpolcan  21332  isgrp2d  21334  gxadd  21374  ablo4  21386  ghgrp  21467  nvsubadd  21647  nvabs  21673  sspph  21867  minvecolem7  21896  htthlem  21931  hvadd4  22049  hvaddsub4  22091  shscli  22330  pjspansn  22590  fh1  22631  fh2  22632  cm2j  22633  chscllem2  22651  spansncvi  22665  5oalem2  22668  5oalem5  22671  5oalem6  22672  3oalem2  22676  hoadd4  22798  cnvunop  22932  bralnfn  22962  eighmorth  22978  hmops  23034  hmopm  23035  adjlnop  23100  adjmul  23106  adjadd  23107  nmopcoi  23109  kbass5  23134  kbass6  23135  hstle  23244  stlesi  23255  mdsl0  23324  mdexchi  23349  atom1d  23367  superpos  23368  cvexchlem  23382  atomli  23396  atcvatlem  23399  chirredlem2  23405  chirredlem3  23406  atcvat4i  23411  mdsymlem1  23417  mdsymlem3  23419  mdsymlem5  23421  mdsymlem6  23422  sumdmdlem  23432  sumdmdlem2  23433  cdj1i  23447  isoun  23613  xrre3FL  23642  utoptop  23858  metustexhalf  23920  blval2  23928  indf1ofs  24009  cntmeas  24164  itgeq12dv  24225  ballotlemfc0  24319  ballotlemfcc  24320  derangenlem  24426  subfacp1lem3  24437  subfacp1lem5  24439  cvmliftmolem2  24537  cvmliftlem6  24545  cvmlift2lem5  24562  cvmlift2lem7  24564  cvmlift2lem9  24566  relexpadd  24707  dfon2lem6  24970  wfrlem3  25084  sltres  25144  axlowdimlem15  25411  axlowdimlem16  25412  axcontlem10  25428  colinbtwnle  25568  onsuct0  25707  nndivsub  25723  supadd  25751  bddiblnc  25778  finminlem  25823  nn0prpwlem  25830  isfne  25860  isref  25871  islocfin  25888  comppfsc  25899  neibastop1  25900  neibastop2lem  25901  neibastop3  25903  tailfb  25918  frinfm  26008  filbcmb  26024  seqpo  26049  sstotbnd2  26089  isbndx  26097  ssbnd  26103  prdsbnd  26108  ismtycnv  26117  ismtyres  26123  heiborlem3  26128  heibor  26136  ghomdiv  26165  grpokerinj  26166  isdrngo2  26180  rngohomco  26196  rngoisocnv  26203  rngoisoco  26204  crngm4  26219  crngohomfo  26222  isidlc  26231  ispridl2  26254  ispridlc  26286  prtlem16  26328  ismrc  26367  eldioph2  26432  lzenom  26440  rexrabdioph  26466  fphpdo  26491  irrapxlem3  26500  elpell14qr2  26538  pell14qrreccl  26540  pell14qrdich  26545  pellfundglb  26561  monotoddzzfi  26618  2nn0ind  26621  jm2.21  26678  jm2.22  26679  dnnumch3  26735  dnwech  26736  fnwe2lem2  26739  pwssplit2  26780  pwssplit3  26781  dsmmsubg  26800  dsmmlss  26801  frlmsslsp  26839  frlmup1  26841  lindfrn  26882  f1lindf  26883  hbtlem6  26924  psgnunilem2  27009  mamuass  27051  phisum  27109  stoweidlem34  27374  stoweidlem48  27388  bnj607  28700  sbcomwAUX7  28998  sbcomOLD7  29146  lubunNEW  29222  lshpcmp  29237  omllaw3  29494  omlfh1N  29507  cvratlem  29669  cvrat3  29690  cvrat4  29691  ps-2  29726  elpaddn0  30048  paddasslem10  30077  cdleme0cp  30462  cdleme32a  30689  cdlemeg49lebilem  30787  cdleme50eq  30789  tendoeq2  31022  diaglbN  31304  diameetN  31305  diainN  31306  dvhopN  31365  djaclN  31385  djajN  31386  dihopelvalcpre  31497  dih1dimatlem  31578  dihmeetcl  31594  djhcl  31649  mapdpglem2  31922
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