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

Theorem 3adant2 974
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant2  |-  ( (
ph  /\  th  /\  ps )  ->  ch )

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 953 . 2  |-  ( (
ph  /\  th  /\  ps )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 15 1  |-  ( (
ph  /\  th  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2ant1  976  eupickb  2208  vtoclegft  2855  eqeu  2936  ordunel  4618  funopg  5286  fnco  5352  dff1o2  5477  fnimapr  5583  fvmptt  5615  fnreseql  5635  f1elima  5787  f1ocnvfvb  5795  oprssov  5989  poxp  6227  smoiso  6379  oaord  6545  oaword  6547  omcan  6567  omwordri  6570  odi  6577  omeulem1  6580  oeord  6586  oecan  6587  oewordri  6590  oeordsuc  6592  nnaord  6617  nnaordr  6618  nndi  6621  nnaword  6625  nnmwordri  6634  erov  6755  ecopovtrn  6761  xpdom3  6960  mapxpen  7027  findcard  7097  indexfi  7163  suppr  7219  r111  7447  tcrank  7554  acndom  7678  infdif2  7836  infxpdom  7837  cfeq0  7882  cfsuc  7883  cfflb  7885  cflim2  7889  cfsmolem  7896  axcc3  8064  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  pwcfsdom  8205  tsktrss  8383  tsksuc  8384  tskuni  8405  adderpqlem  8578  mulerpqlem  8579  mulcanenq  8584  distrnq  8585  ltsonq  8593  ltanq  8595  ltmnq  8596  distrlem1pr  8649  distrlem5pr  8651  ltsopr  8656  ltsosr  8716  ltasr  8722  adddir  8830  axlttrn  8895  letr  8914  ltneOLD  8918  nnncan1  9083  npncan3  9085  pnpcan2  9087  subdi  9213  subdir  9214  divmul  9427  div23  9443  div13  9445  divsubdir  9456  divcan7  9469  ltmul2  9607  lemul1  9608  lemul2  9609  lemul2a  9611  lediv1  9621  ltmuldiv2  9627  lemuldiv  9635  lemuldiv2  9636  ltdiv2  9641  lediv2  9646  infmrlb  9735  nndivtr  9787  bndndx  9964  fnn0ind  10111  lbzbi  10306  xrletr  10489  qsqueeze  10528  xleadd2a  10574  xleadd1  10575  xltadd2  10577  xltmul2  10613  supxrbnd  10647  iooneg  10756  iccneg  10757  icoshft  10758  icoshftf1o  10759  fzen  10811  fzrevral2  10867  fzshftral  10869  elfzo  10877  fzoaddel2  10907  fzosubel2  10909  modmulnn  10988  modcyc  10999  moddi  11007  modsubdir  11008  uzindi  11043  axdc4uzlem  11044  expneg2  11112  expdiv  11152  expubnd  11162  bernneq2  11228  ccatco  11490  swrds2  11560  shftuz  11564  shftval2  11570  abs3dif  11815  sin02gt0  12472  dvdsval2  12534  dvdscmul  12555  dvdsmulc  12556  dvdscmulr  12557  dvdsmulcr  12558  divalglem8  12599  ndvdssub  12606  rpmulgcd  12734  isprm3  12767  coprmdvds  12781  coprimeprodsq  12862  pythagtriplem12  12879  pythagtriplem14  12881  pcprendvds  12893  pcmul  12904  pcdiv  12905  pcqcl  12909  pcqdiv  12910  pcdvdsb  12921  pcgcd  12930  vdwnnlem1  13042  hashbcss  13051  mrcss  13518  mrcsscl  13522  mrcun  13524  cofulid  13764  catcisolem  13938  ple1  14150  latleeqj1  14169  clatl  14220  lubun  14227  clatleglb  14230  pslem  14315  dirtr  14358  pwspjmhm  14444  gsumccat  14464  grpinvid1  14530  grpinvid2  14531  grpinvadd  14544  grpsubf  14545  grpsubrcan  14547  grpinvsub  14548  grpsubeq0  14552  grppncan  14556  grpnpcan  14557  mulgnn0p1  14578  subgsubcl  14632  subgsub  14633  eqglact  14668  divssub  14677  ghmsub  14691  odval2  14866  oddvds2  14879  odsubdvds  14882  gexnnod  14899  slwn0  14926  gsumsn  15220  gsumdixp  15392  dvrcl  15468  unitdvcl  15469  dvrcan1  15473  dvrcan3  15474  dvreq1  15475  subrgdv  15562  abvsubtri  15600  lmodvsubval2  15680  lsmcl  15836  lsmsp2  15840  lspsntrim  15851  lidldvgen  16007  evlslem4  16245  chrcong  16483  zndvds  16503  zntoslem  16510  ocvsscon  16575  obselocv  16628  istps3OLD  16660  ntrin  16798  elnei  16848  neindisj2  16860  ordtopn3  16926  ordtcld3  16929  leordtval2  16942  lecldbas  16949  cnrest2  17014  cmpsublem  17126  ptrescn  17333  xkococn  17354  kqfeq  17415  snfbas  17561  neifil  17575  fclsrest  17719  xmetge0  17909  xmetsym  17912  nm2dif  18146  nmtri  18147  cnmet  18281  cnmpt2pc  18426  iihalf1  18429  iihalf2  18431  icoopnst  18437  iocopnst  18438  cphsqrcl3  18623  cph2ass  18648  caublcls  18734  bcthlem3  18748  bcthlem4  18749  srabn  18777  iblconst  19172  mpfsubrg  19424  tdeglem3  19445  mdegmullem  19464  dvdsq1p  19546  coeid3  19622  aannenlem2  19709  pserdvlem2  19804  tanord1  19899  efgh  19903  cxpef  20012  recxpcl  20022  lawcos  20114  pythag  20115  isosctrlem1  20118  isosctrlem2  20119  isgrpo  20863  grpoinvid1  20897  grpoinvid2  20898  grpoasscan1  20904  grpoasscan2  20905  grpoinvop  20908  grpodivinv  20911  grpoinvdiv  20912  grpodivf  20913  grpopncan  20918  grponpcan  20919  grpopnpcan2  20920  gxid  20940  resgrprn  20947  ablonncan  20961  vcnegsubdi2  21131  vcsub4  21132  nvmval  21200  nvmval2  21201  nvmfval  21202  nvmul0or  21210  nvsubadd  21213  nvpncan2  21214  nvaddsub4  21219  nvnncan  21221  nvmeq0  21222  nvdif  21231  nvpi  21232  nvmtri  21237  nvabs  21239  imsmetlem  21259  ipval2lem3  21278  ipval2  21280  4ipval2  21281  ipval3  21282  ipval2lem6  21284  nmooge0  21345  blometi  21381  hvaddsub12  21617  hvsubdistr1  21628  hvsubdistr2  21629  hvaddcan2  21650  hvmulcan  21651  hvmulcan2  21652  hvsubcan  21653  hvsubcan2  21654  his7  21669  his2sub  21671  his2sub2  21672  norm3dif2  21730  shsubcl  21800  hhssnv  21841  shlej2  21940  fh2  22198  cm2j  22199  pjoi0  22296  hodcl  22327  hosubdi  22388  unopf1o  22496  unopadj  22499  adj2  22514  adjvalval  22517  braadd  22525  bramul  22526  lnopaddmuli  22553  lnopsubmuli  22555  homco2  22557  lnfnaddmuli  22625  adjlnop  22666  leopmul  22714  leoptr  22717  pjimai  22756  atcv1  22960  atexch  22961  atcvatlem  22965  xdivmul  23108  relogbcl  23404  logblt  23408  hasheuni  23453  difelsiga  23494  cndprobin  23637  bayesth  23642  ghomf1olem  24001  modaddabs  24011  lediv2aALT  24013  mulcan1g  24084  mulcan2g  24085  subdivcomb1  24090  fununiq  24126  dfrdg2  24152  wfrlem4  24259  sltres  24318  nobndlem8  24353  ax5seglem1  24556  axcontlem2  24593  axcontlem8  24599  areacirc  24931  mapmapmap  25148  injsurinj  25149  preodom2  25226  preoran2  25230  altprs2  25236  abloinvop  25353  grpodlcan  25376  grpodivzer  25377  prsubrtr  25399  rltrran  25414  multinv  25422  zerdivemp1  25436  mulinvsca  25480  svli2  25484  nelioo5  25511  intcont  25543  istopxc  25548  islimrs3  25581  lvsovso  25626  supnuf  25629  addcomv  25655  negveud  25668  negveudr  25669  subclrvd  25674  distmlva  25688  distsava  25689  eqidob  25795  cmphmia  25798  tartarmap  25888  fnctartar  25907  fnctartar2  25908  cmppar3  25974  cmpmor  25975  indcls2  25996  isconcl6a  26103  lppotos  26144  pdiveql  26168  clsun  26246  neiin  26250  filbcmb  26432  ismtybnd  26531  grpoeqdivid  26571  ghomco  26573  rngonegrmul  26583  zerdivemp1x  26586  rngohomco  26605  rngoisoco  26613  riscer  26619  intidl  26654  isfldidl  26693  mzprename  26827  dvdsrabdioph  26891  pell14qrdivcl  26950  monotoddzz  27028  dvdsabsmod0  27079  jm2.19lem2  27083  jm2.19  27086  psgnunilem4  27420  dvconstbi  27551  stoweidlem3  27752  stoweidlem10  27759  stoweidlem19  27768  sigaraf  27843  sigarmf  27844  frgra3v  28180  reccot  28228  rectan  28229  chordthmALT  28710  lubunNEW  29163  lshpnelb  29174  opnlen0  29378  lub0N  29379  glb0N  29383  opcon3b  29386  opcon2b  29387  oplecon3b  29390  opltcon3b  29394  opltcon2b  29396  oldmm1  29407  oldmm4  29410  oldmj1  29411  oldmj4  29414  cvrval2  29464  cvrcon3b  29467  leatb  29482  atcmp  29501  atcvreq0  29504  atlatle  29510  athgt  29645  3dim2  29657  islln2a  29706  lplnnleat  29731  lvolnleat  29772  4atlem10  29795  4atlem11  29798  4atlem12  29801  dalem21  29883  dalem22  29884  dalem23  29885  dalem29  29890  dalem30  29891  dalem31N  29892  dalem32  29893  dalem33  29894  dalem34  29895  dalem35  29896  dalem36  29897  dalem37  29898  dalem40  29901  dalem46  29907  dalem47  29908  dalem51  29912  dalem52  29913  dalem58  29919  dalem59  29920  pmaple  29950  paddclN  30031  pmapjoin  30041  pmapjat1  30042  elpcliN  30082  pclssN  30083  pclun2N  30088  2polcon4bN  30107  paddunN  30116  poldmj1N  30117  pmapj2N  30118  pmapocjN  30119  psubclinN  30137  paddatclN  30138  poml4N  30142  lautco  30286  ldilco  30305  ltrneq2  30337  trljat1  30355  cdlemc1  30380  cdleme10  30443  ltrnco  30908  trlcocnv  30909  trljco  30929  trljco2  30930  cdlemi1  31007  tendocnv  31211  diaord  31237  dibord  31349  dihord3  31447  dihord4  31448  dihmeetlem2N  31489  dihmeetlem4preN  31496  dochdmj1  31580  hdmap10lem  32032
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  df-3an 936
  Copyright terms: Public domain W3C validator