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  2221  vtoclegft  2868  eqeu  2949  ordunel  4634  funopg  5302  fnco  5368  dff1o2  5493  fnimapr  5599  fvmptt  5631  fnreseql  5651  f1elima  5803  f1ocnvfvb  5811  oprssov  6005  poxp  6243  smoiso  6395  oaord  6561  oaword  6563  omcan  6583  omwordri  6586  odi  6593  omeulem1  6596  oeord  6602  oecan  6603  oewordri  6606  oeordsuc  6608  nnaord  6633  nnaordr  6634  nndi  6637  nnaword  6641  nnmwordri  6650  erov  6771  ecopovtrn  6777  xpdom3  6976  mapxpen  7043  findcard  7113  indexfi  7179  suppr  7235  r111  7463  tcrank  7570  acndom  7694  infdif2  7852  infxpdom  7853  cfeq0  7898  cfsuc  7899  cfflb  7901  cflim2  7905  cfsmolem  7912  axcc3  8080  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  pwcfsdom  8221  tsktrss  8399  tsksuc  8400  tskuni  8421  adderpqlem  8594  mulerpqlem  8595  mulcanenq  8600  distrnq  8601  ltsonq  8609  ltanq  8611  ltmnq  8612  distrlem1pr  8665  distrlem5pr  8667  ltsopr  8672  ltsosr  8732  ltasr  8738  adddir  8846  axlttrn  8911  letr  8930  ltneOLD  8934  nnncan1  9099  npncan3  9101  pnpcan2  9103  subdi  9229  subdir  9230  divmul  9443  div23  9459  div13  9461  divsubdir  9472  divcan7  9485  ltmul2  9623  lemul1  9624  lemul2  9625  lemul2a  9627  lediv1  9637  ltmuldiv2  9643  lemuldiv  9651  lemuldiv2  9652  ltdiv2  9657  lediv2  9662  infmrlb  9751  nndivtr  9803  bndndx  9980  fnn0ind  10127  lbzbi  10322  xrletr  10505  qsqueeze  10544  xleadd2a  10590  xleadd1  10591  xltadd2  10593  xltmul2  10629  supxrbnd  10663  iooneg  10772  iccneg  10773  icoshft  10774  icoshftf1o  10775  fzen  10827  fzrevral2  10883  fzshftral  10885  elfzo  10893  fzoaddel2  10923  fzosubel2  10925  modmulnn  11004  modcyc  11015  moddi  11023  modsubdir  11024  uzindi  11059  axdc4uzlem  11060  expneg2  11128  expdiv  11168  expubnd  11178  bernneq2  11244  ccatco  11506  swrds2  11576  shftuz  11580  shftval2  11586  abs3dif  11831  sin02gt0  12488  dvdsval2  12550  dvdscmul  12571  dvdsmulc  12572  dvdscmulr  12573  dvdsmulcr  12574  divalglem8  12615  ndvdssub  12622  rpmulgcd  12750  isprm3  12783  coprmdvds  12797  coprimeprodsq  12878  pythagtriplem12  12895  pythagtriplem14  12897  pcprendvds  12909  pcmul  12920  pcdiv  12921  pcqcl  12925  pcqdiv  12926  pcdvdsb  12937  pcgcd  12946  vdwnnlem1  13058  hashbcss  13067  mrcss  13534  mrcsscl  13538  mrcun  13540  cofulid  13780  catcisolem  13954  ple1  14166  latleeqj1  14185  clatl  14236  lubun  14243  clatleglb  14246  pslem  14331  dirtr  14374  pwspjmhm  14460  gsumccat  14480  grpinvid1  14546  grpinvid2  14547  grpinvadd  14560  grpsubf  14561  grpsubrcan  14563  grpinvsub  14564  grpsubeq0  14568  grppncan  14572  grpnpcan  14573  mulgnn0p1  14594  subgsubcl  14648  subgsub  14649  eqglact  14684  divssub  14693  ghmsub  14707  odval2  14882  oddvds2  14895  odsubdvds  14898  gexnnod  14915  slwn0  14942  gsumsn  15236  gsumdixp  15408  dvrcl  15484  unitdvcl  15485  dvrcan1  15489  dvrcan3  15490  dvreq1  15491  subrgdv  15578  abvsubtri  15616  lmodvsubval2  15696  lsmcl  15852  lsmsp2  15856  lspsntrim  15867  lidldvgen  16023  evlslem4  16261  chrcong  16499  zndvds  16519  zntoslem  16526  ocvsscon  16591  obselocv  16644  istps3OLD  16676  ntrin  16814  elnei  16864  neindisj2  16876  ordtopn3  16942  ordtcld3  16945  leordtval2  16958  lecldbas  16965  cnrest2  17030  cmpsublem  17142  ptrescn  17349  xkococn  17370  kqfeq  17431  snfbas  17577  neifil  17591  fclsrest  17735  xmetge0  17925  xmetsym  17928  nm2dif  18162  nmtri  18163  cnmet  18297  cnmpt2pc  18442  iihalf1  18445  iihalf2  18447  icoopnst  18453  iocopnst  18454  cphsqrcl3  18639  cph2ass  18664  caublcls  18750  bcthlem3  18764  bcthlem4  18765  srabn  18793  iblconst  19188  mpfsubrg  19440  tdeglem3  19461  mdegmullem  19480  dvdsq1p  19562  coeid3  19638  aannenlem2  19725  pserdvlem2  19820  tanord1  19915  efgh  19919  cxpef  20028  recxpcl  20038  lawcos  20130  pythag  20131  isosctrlem1  20134  isosctrlem2  20135  isgrpo  20879  grpoinvid1  20913  grpoinvid2  20914  grpoasscan1  20920  grpoasscan2  20921  grpoinvop  20924  grpodivinv  20927  grpoinvdiv  20928  grpodivf  20929  grpopncan  20934  grponpcan  20935  grpopnpcan2  20936  gxid  20956  resgrprn  20963  ablonncan  20977  vcnegsubdi2  21147  vcsub4  21148  nvmval  21216  nvmval2  21217  nvmfval  21218  nvmul0or  21226  nvsubadd  21229  nvpncan2  21230  nvaddsub4  21235  nvnncan  21237  nvmeq0  21238  nvdif  21247  nvpi  21248  nvmtri  21253  nvabs  21255  imsmetlem  21275  ipval2lem3  21294  ipval2  21296  4ipval2  21297  ipval3  21298  ipval2lem6  21300  nmooge0  21361  blometi  21397  hvaddsub12  21633  hvsubdistr1  21644  hvsubdistr2  21645  hvaddcan2  21666  hvmulcan  21667  hvmulcan2  21668  hvsubcan  21669  hvsubcan2  21670  his7  21685  his2sub  21687  his2sub2  21688  norm3dif2  21746  shsubcl  21816  hhssnv  21857  shlej2  21956  fh2  22214  cm2j  22215  pjoi0  22312  hodcl  22343  hosubdi  22404  unopf1o  22512  unopadj  22515  adj2  22530  adjvalval  22533  braadd  22541  bramul  22542  lnopaddmuli  22569  lnopsubmuli  22571  homco2  22573  lnfnaddmuli  22641  adjlnop  22682  leopmul  22730  leoptr  22733  pjimai  22772  atcv1  22976  atexch  22977  atcvatlem  22981  xdivmul  23124  relogbcl  23419  logblt  23423  hasheuni  23468  difelsiga  23509  cndprobin  23652  bayesth  23657  ghomf1olem  24016  modaddabs  24026  lediv2aALT  24028  mulcan1g  24099  mulcan2g  24100  subdivcomb1  24105  faclimlem5  24121  fununiq  24197  dfrdg2  24223  wfrlem4  24330  sltres  24389  nobndlem8  24424  ax5seglem1  24628  axcontlem2  24665  axcontlem8  24671  ltflcei  24998  areacirc  25034  mapmapmap  25251  injsurinj  25252  preodom2  25329  preoran2  25333  altprs2  25339  abloinvop  25456  grpodlcan  25479  grpodivzer  25480  prsubrtr  25502  rltrran  25517  multinv  25525  zerdivemp1  25539  mulinvsca  25583  svli2  25587  nelioo5  25614  intcont  25646  istopxc  25651  islimrs3  25684  lvsovso  25729  supnuf  25732  addcomv  25758  negveud  25771  negveudr  25772  subclrvd  25777  distmlva  25791  distsava  25792  eqidob  25898  cmphmia  25901  tartarmap  25991  fnctartar  26010  fnctartar2  26011  cmppar3  26077  cmpmor  26078  indcls2  26099  isconcl6a  26206  lppotos  26247  pdiveql  26271  clsun  26349  neiin  26353  filbcmb  26535  ismtybnd  26634  grpoeqdivid  26674  ghomco  26676  rngonegrmul  26686  zerdivemp1x  26689  rngohomco  26708  rngoisoco  26716  riscer  26722  intidl  26757  isfldidl  26796  mzprename  26930  dvdsrabdioph  26994  pell14qrdivcl  27053  monotoddzz  27131  dvdsabsmod0  27182  jm2.19lem2  27186  jm2.19  27189  psgnunilem4  27523  dvconstbi  27654  stoweidlem3  27855  stoweidlem10  27862  stoweidlem19  27871  sigaraf  27946  sigarmf  27947  nb3graprlem2  28288  cusgra3v  28299  usgrnloop  28351  ispthon  28362  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3lem4  28393  constr3lem5  28394  constr3lem6  28395  constr3trllem2  28397  constr3trllem3  28398  4cycl4dv  28413  frgra3v  28426  reccot  28482  rectan  28483  chordthmALT  29026  lubunNEW  29785  lshpnelb  29796  opnlen0  30000  lub0N  30001  glb0N  30005  opcon3b  30008  opcon2b  30009  oplecon3b  30012  opltcon3b  30016  opltcon2b  30018  oldmm1  30029  oldmm4  30032  oldmj1  30033  oldmj4  30036  cvrval2  30086  cvrcon3b  30089  leatb  30104  atcmp  30123  atcvreq0  30126  atlatle  30132  athgt  30267  3dim2  30279  islln2a  30328  lplnnleat  30353  lvolnleat  30394  4atlem10  30417  4atlem11  30420  4atlem12  30423  dalem21  30505  dalem22  30506  dalem23  30507  dalem29  30512  dalem30  30513  dalem31N  30514  dalem32  30515  dalem33  30516  dalem34  30517  dalem35  30518  dalem36  30519  dalem37  30520  dalem40  30523  dalem46  30529  dalem47  30530  dalem51  30534  dalem52  30535  dalem58  30541  dalem59  30542  pmaple  30572  paddclN  30653  pmapjoin  30663  pmapjat1  30664  elpcliN  30704  pclssN  30705  pclun2N  30710  2polcon4bN  30729  paddunN  30738  poldmj1N  30739  pmapj2N  30740  pmapocjN  30741  psubclinN  30759  paddatclN  30760  poml4N  30764  lautco  30908  ldilco  30927  ltrneq2  30959  trljat1  30977  cdlemc1  31002  cdleme10  31065  ltrnco  31530  trlcocnv  31531  trljco  31551  trljco2  31552  cdlemi1  31629  tendocnv  31833  diaord  31859  dibord  31971  dihord3  32069  dihord4  32070  dihmeetlem2N  32111  dihmeetlem4preN  32118  dochdmj1  32202  hdmap10lem  32654
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