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  2241  vtoclegft  2889  eqeu  2970  ordunel  4655  funopg  5323  fnco  5389  dff1o2  5515  fnimapr  5621  fvmptt  5653  fnreseql  5673  f1elima  5829  f1ocnvfvb  5837  oprssov  6031  poxp  6269  smoiso  6421  oaord  6587  oaword  6589  omcan  6609  omwordri  6612  odi  6619  omeulem1  6622  oeord  6628  oecan  6629  oewordri  6632  oeordsuc  6634  nnaord  6659  nnaordr  6660  nndi  6663  nnaword  6667  nnmwordri  6676  erov  6798  ecopovtrn  6804  xpdom3  7003  mapxpen  7070  findcard  7142  indexfi  7208  suppr  7264  r111  7492  tcrank  7599  acndom  7723  infdif2  7881  infxpdom  7882  cfeq0  7927  cfsuc  7928  cfflb  7930  cflim2  7934  cfsmolem  7941  axcc3  8109  domtriomlem  8113  axdc3lem2  8122  axdc3lem4  8124  axdc4lem  8126  axcclem  8128  pwcfsdom  8250  tsktrss  8428  tsksuc  8429  tskuni  8450  adderpqlem  8623  mulerpqlem  8624  mulcanenq  8629  distrnq  8630  ltsonq  8638  ltanq  8640  ltmnq  8641  distrlem1pr  8694  distrlem5pr  8696  ltsopr  8701  ltsosr  8761  ltasr  8767  adddir  8875  axlttrn  8940  letr  8959  ltneOLD  8963  nnncan1  9128  npncan3  9130  pnpcan2  9132  subdi  9258  subdir  9259  divmul  9472  div23  9488  div13  9490  divsubdir  9501  divcan7  9514  ltmul2  9652  lemul1  9653  lemul2  9654  lemul2a  9656  lediv1  9666  ltmuldiv2  9672  lemuldiv  9680  lemuldiv2  9681  ltdiv2  9686  lediv2  9691  infmrlb  9780  nndivtr  9832  bndndx  10011  fnn0ind  10158  lbzbi  10353  xrletr  10536  qsqueeze  10575  xleadd2a  10621  xleadd1  10622  xltadd2  10624  xltmul2  10660  supxrbnd  10694  iooneg  10803  iccneg  10804  icoshft  10805  icoshftf1o  10806  fzen  10858  fzrevral2  10914  fzshftral  10916  elfzo  10924  fzoaddel2  10954  fzosubel2  10956  modmulnn  11035  modcyc  11046  moddi  11054  modsubdir  11055  uzindi  11090  axdc4uzlem  11091  expneg2  11159  expdiv  11199  expubnd  11209  bernneq2  11275  ccatco  11537  swrds2  11607  shftuz  11611  shftval2  11617  abs3dif  11862  sin02gt0  12519  dvdsval2  12581  dvdscmul  12602  dvdsmulc  12603  dvdscmulr  12604  dvdsmulcr  12605  divalglem8  12646  ndvdssub  12653  rpmulgcd  12781  isprm3  12814  coprmdvds  12828  coprimeprodsq  12909  pythagtriplem12  12926  pythagtriplem14  12928  pcprendvds  12940  pcmul  12951  pcdiv  12952  pcqcl  12956  pcqdiv  12957  pcdvdsb  12968  pcgcd  12977  vdwnnlem1  13089  hashbcss  13098  mrcss  13567  mrcsscl  13571  mrcun  13573  cofulid  13813  catcisolem  13987  ple1  14199  latleeqj1  14218  clatl  14269  lubun  14276  clatleglb  14279  pslem  14364  dirtr  14407  pwspjmhm  14493  gsumccat  14513  grpinvid1  14579  grpinvid2  14580  grpinvadd  14593  grpsubf  14594  grpsubrcan  14596  grpinvsub  14597  grpsubeq0  14601  grppncan  14605  grpnpcan  14606  mulgnn0p1  14627  subgsubcl  14681  subgsub  14682  eqglact  14717  divssub  14726  ghmsub  14740  odval2  14915  oddvds2  14928  odsubdvds  14931  gexnnod  14948  slwn0  14975  gsumsn  15269  gsumdixp  15441  dvrcl  15517  unitdvcl  15518  dvrcan1  15522  dvrcan3  15523  dvreq1  15524  subrgdv  15611  abvsubtri  15649  lmodvsubval2  15729  lsmcl  15885  lsmsp2  15889  lspsntrim  15900  lidldvgen  16056  evlslem4  16294  chrcong  16539  zndvds  16559  zntoslem  16566  ocvsscon  16631  obselocv  16684  istps3OLD  16716  ntrin  16854  elnei  16904  neindisj2  16916  ordtopn3  16982  ordtcld3  16985  leordtval2  16998  lecldbas  17005  cnrest2  17070  cmpsublem  17182  ptrescn  17389  xkococn  17410  kqfeq  17471  snfbas  17613  neifil  17627  fclsrest  17771  xmetge0  17961  xmetsym  17964  nm2dif  18198  nmtri  18199  cnmet  18333  cnmpt2pc  18479  iihalf1  18482  iihalf2  18484  icoopnst  18490  iocopnst  18491  cphsqrcl3  18676  cph2ass  18701  caublcls  18787  bcthlem3  18801  bcthlem4  18802  srabn  18830  iblconst  19225  mpfsubrg  19477  tdeglem3  19498  mdegmullem  19517  dvdsq1p  19599  coeid3  19675  aannenlem2  19762  pserdvlem2  19857  tanord1  19952  efgh  19956  cxpef  20065  recxpcl  20075  lawcos  20167  pythag  20168  isosctrlem1  20171  isosctrlem2  20172  isgrpo  20916  grpoinvid1  20950  grpoinvid2  20951  grpoasscan1  20957  grpoasscan2  20958  grpoinvop  20961  grpodivinv  20964  grpoinvdiv  20965  grpodivf  20966  grpopncan  20971  grponpcan  20972  grpopnpcan2  20973  gxid  20993  resgrprn  21000  ablonncan  21014  zerdivemp1  21154  vcnegsubdi2  21186  vcsub4  21187  nvmval  21255  nvmval2  21256  nvmfval  21257  nvmul0or  21265  nvsubadd  21268  nvpncan2  21269  nvaddsub4  21274  nvnncan  21276  nvmeq0  21277  nvdif  21286  nvpi  21287  nvmtri  21292  nvabs  21294  imsmetlem  21314  ipval2lem3  21333  ipval2  21335  4ipval2  21336  ipval3  21337  ipval2lem6  21339  nmooge0  21400  blometi  21436  hvaddsub12  21672  hvsubdistr1  21683  hvsubdistr2  21684  hvaddcan2  21705  hvmulcan  21706  hvmulcan2  21707  hvsubcan  21708  hvsubcan2  21709  his7  21724  his2sub  21726  his2sub2  21727  norm3dif2  21785  shsubcl  21855  hhssnv  21896  shlej2  21995  fh2  22253  cm2j  22254  pjoi0  22351  hodcl  22382  hosubdi  22443  unopf1o  22551  unopadj  22554  adj2  22569  adjvalval  22572  braadd  22580  bramul  22581  lnopaddmuli  22608  lnopsubmuli  22610  homco2  22612  lnfnaddmuli  22680  adjlnop  22721  leopmul  22769  leoptr  22772  pjimai  22811  atcv1  23015  atexch  23016  atcvatlem  23020  divnumden2  23313  xdivmul  23323  metustto  23495  metustbl  23508  restmetu  23513  relogbcl  23594  logblt  23598  hasheuni  23651  difelsiga  23692  cndprobin  23866  bayesth  23871  ghomf1olem  24285  modaddabs  24295  lediv2aALT  24297  mulcan1g  24370  mulcan2g  24371  subdivcomb1  24376  fununiq  24511  dfrdg2  24537  wfrlem4  24644  sltres  24703  nobndlem8  24738  ax5seglem1  24942  axcontlem2  24979  axcontlem8  24985  ltflcei  25312  areacirc  25348  clsun  25395  neiin  25399  filbcmb  25581  ismtybnd  25679  grpoeqdivid  25719  ghomco  25721  rngonegrmul  25731  zerdivemp1x  25734  rngohomco  25753  rngoisoco  25761  riscer  25767  intidl  25802  isfldidl  25841  mzprename  25975  dvdsrabdioph  26039  pell14qrdivcl  26098  monotoddzz  26176  dvdsabsmod0  26227  jm2.19lem2  26231  jm2.19  26234  psgnunilem4  26568  dvconstbi  26699  stoweidlem3  26900  stoweidlem10  26907  stoweidlem19  26916  sigaraf  26991  sigarmf  26992  nn0n0n1ge2  27267  hashinfxadd  27291  nbgraf1olem3  27390  nb3graprlem2  27398  cusgra3v  27409  iswlkon  27443  istrlon  27453  usgrnloop  27467  ispthon  27478  usgrcyclnl2  27525  3v3e3cycl1  27528  constr3lem4  27531  constr3lem5  27532  constr3lem6  27533  constr3trllem2  27535  constr3trllem3  27536  4cycl4dv  27551  frgra3v  27594  reccot  27677  rectan  27678  chordthmALT  28221  lubunNEW  28981  lshpnelb  28992  opnlen0  29196  lub0N  29197  glb0N  29201  opcon3b  29204  opcon2b  29205  oplecon3b  29208  opltcon3b  29212  opltcon2b  29214  oldmm1  29225  oldmm4  29228  oldmj1  29229  oldmj4  29232  cvrval2  29282  cvrcon3b  29285  leatb  29300  atcmp  29319  atcvreq0  29322  atlatle  29328  athgt  29463  3dim2  29475  islln2a  29524  lplnnleat  29549  lvolnleat  29590  4atlem10  29613  4atlem11  29616  4atlem12  29619  dalem21  29701  dalem22  29702  dalem23  29703  dalem29  29708  dalem30  29709  dalem31N  29710  dalem32  29711  dalem33  29712  dalem34  29713  dalem35  29714  dalem36  29715  dalem37  29716  dalem40  29719  dalem46  29725  dalem47  29726  dalem51  29730  dalem52  29731  dalem58  29737  dalem59  29738  pmaple  29768  paddclN  29849  pmapjoin  29859  pmapjat1  29860  elpcliN  29900  pclssN  29901  pclun2N  29906  2polcon4bN  29925  paddunN  29934  poldmj1N  29935  pmapj2N  29936  pmapocjN  29937  psubclinN  29955  paddatclN  29956  poml4N  29960  lautco  30104  ldilco  30123  ltrneq2  30155  trljat1  30173  cdlemc1  30198  cdleme10  30261  ltrnco  30726  trlcocnv  30727  trljco  30747  trljco2  30748  cdlemi1  30825  tendocnv  31029  diaord  31055  dibord  31167  dihord3  31265  dihord4  31266  dihmeetlem2N  31307  dihmeetlem4preN  31314  dochdmj1  31398  hdmap10lem  31850
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