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

Theorem 3adant2 976
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 955 . 2  |-  ( (
ph  /\  th  /\  ps )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( (
ph  /\  th  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ad2ant1  978  eupickb  2346  vtoclegft  3023  eqeu  3105  ordunel  4807  funopg  5485  fnco  5553  dff1o2  5679  fnimapr  5787  fvmptt  5820  fnreseql  5840  f1elima  6009  f1ocnvfvb  6017  oprssov  6215  poxp  6458  smoiso  6624  oaord  6790  oaword  6792  omcan  6812  omwordri  6815  odi  6822  omeulem1  6825  oeord  6831  oecan  6832  oewordri  6835  oeordsuc  6837  nnaord  6862  nnaordr  6863  nndi  6866  nnaword  6870  nnmwordri  6879  erov  7001  ecopovtrn  7007  xpdom3  7206  mapxpen  7273  findcard  7347  indexfi  7414  suppr  7473  r111  7701  tcrank  7808  acndom  7932  infdif2  8090  infxpdom  8091  cfeq0  8136  cfsuc  8137  cfflb  8139  cflim2  8143  cfsmolem  8150  axcc3  8318  domtriomlem  8322  axdc3lem2  8331  axdc3lem4  8333  axdc4lem  8335  axcclem  8337  pwcfsdom  8458  tsktrss  8636  tsksuc  8637  tskuni  8658  adderpqlem  8831  mulerpqlem  8832  mulcanenq  8837  distrnq  8838  ltsonq  8846  ltanq  8848  ltmnq  8849  distrlem1pr  8902  distrlem5pr  8904  ltsopr  8909  ltsosr  8969  ltasr  8975  adddir  9083  axlttrn  9148  letr  9167  ltneOLD  9171  nnncan1  9337  npncan3  9339  pnpcan2  9341  subdi  9467  subdir  9468  divmul  9681  div23  9697  div13  9699  divsubdir  9710  divcan7  9723  ltmul2  9861  lemul1  9862  lemul2  9863  lemul2a  9865  lediv1  9875  ltmuldiv2  9881  lemuldiv  9889  lemuldiv2  9890  ltdiv2  9895  lediv2  9900  infmrlb  9989  nndivtr  10041  bndndx  10220  nn0n0n1ge2  10280  fnn0ind  10369  lbzbi  10564  xrletr  10748  qsqueeze  10787  xleadd2a  10833  xleadd1  10834  xltadd2  10836  xltmul2  10872  supxrbnd  10907  iooneg  11017  iccneg  11018  icoshft  11019  icoshftf1o  11020  fzen  11072  fzrevral2  11132  fzshftral  11134  elfzo  11142  fzoaddel2  11176  fzosubel2  11178  modmulnn  11265  modcyc  11276  moddi  11284  modsubdir  11285  uzindi  11320  axdc4uzlem  11321  expneg2  11390  expdiv  11430  expubnd  11440  bernneq2  11506  hashinfxadd  11659  brfi1indlem  11714  ccatco  11804  swrds2  11880  shftuz  11884  shftval2  11890  abs3dif  12135  sin02gt0  12793  dvdsval2  12855  dvdscmul  12876  dvdsmulc  12877  dvdscmulr  12878  dvdsmulcr  12879  divalglem8  12920  ndvdssub  12927  rpmulgcd  13055  isprm3  13088  coprmdvds  13102  coprimeprodsq  13183  pythagtriplem12  13200  pythagtriplem14  13202  pcprendvds  13214  pcmul  13225  pcdiv  13226  pcqcl  13230  pcqdiv  13231  pcdvdsb  13242  pcgcd  13251  vdwnnlem1  13363  hashbcss  13372  mrcss  13841  mrcsscl  13845  mrcun  13847  cofulid  14087  catcisolem  14261  ple1  14473  latleeqj1  14492  clatl  14543  lubun  14550  clatleglb  14553  pslem  14638  dirtr  14681  pwspjmhm  14767  gsumccat  14787  grpinvid1  14853  grpinvid2  14854  grpinvadd  14867  grpsubf  14868  grpsubrcan  14870  grpinvsub  14871  grpsubeq0  14875  grppncan  14879  grpnpcan  14880  mulgnn0p1  14901  subgsubcl  14955  subgsub  14956  eqglact  14991  divssub  15000  ghmsub  15014  odval2  15189  oddvds2  15202  odsubdvds  15205  gexnnod  15222  slwn0  15249  gsumsn  15543  gsumdixp  15715  dvrcl  15791  unitdvcl  15792  dvrcan1  15796  dvrcan3  15797  dvreq1  15798  subrgdv  15885  abvsubtri  15923  lmodvsubval2  15999  lsmcl  16155  lsmsp2  16159  lspsntrim  16170  lidldvgen  16326  evlslem4  16564  chrcong  16810  zndvds  16830  zntoslem  16837  ocvsscon  16902  obselocv  16955  istps3OLD  16987  ntrin  17125  elnei  17175  neindisj2  17187  ordtopn3  17260  ordtcld3  17263  leordtval2  17276  lecldbas  17283  cnrest2  17350  cmpsublem  17462  ptrescn  17671  xkococn  17692  kqfeq  17756  snfbas  17898  neifil  17912  fclsrest  18056  utopsnnei  18279  neipcfilu  18326  psmetsym  18341  psmetge0  18343  xmetge0  18374  xmetsym  18377  metusttoOLD  18587  metustto  18588  metustblOLD  18610  metustbl  18611  restmetu  18617  nm2dif  18671  nmtri  18672  cnmet  18806  cnmpt2pc  18953  iihalf1  18956  iihalf2  18958  icoopnst  18964  iocopnst  18965  cphsqrcl3  19150  cph2ass  19175  caublcls  19261  bcthlem3  19279  bcthlem4  19280  srabn  19314  iblconst  19709  mpfsubrg  19961  tdeglem3  19982  mdegmullem  20001  dvdsq1p  20083  coeid3  20159  aannenlem2  20246  pserdvlem2  20344  tanord1  20439  efgh  20443  cxpef  20556  recxpcl  20566  lawcos  20658  pythag  20659  isosctrlem1  20662  isosctrlem2  20663  fiusgraedgfi  21421  nbgraf1olem3  21453  nb3graprlem2  21461  cusgra3v  21473  cusgrasizeindslem3  21484  cusgrasizeinds  21485  iswlkon  21531  istrlon  21541  2trllemE  21553  usgrnloop  21563  ispthon  21576  isspthon  21583  usgrcyclnl2  21628  3v3e3cycl1  21631  constr3lem4  21634  constr3lem5  21635  constr3lem6  21636  constr3trllem2  21638  constr3trllem3  21639  4cycl4dv  21654  isgrpo  21784  grpoinvid1  21818  grpoinvid2  21819  grpoasscan1  21825  grpoasscan2  21826  grpoinvop  21829  grpodivinv  21832  grpoinvdiv  21833  grpodivf  21834  grpopncan  21839  grponpcan  21840  grpopnpcan2  21841  gxid  21861  resgrprn  21868  ablonncan  21882  zerdivemp1  22022  vcnegsubdi2  22054  vcsub4  22055  nvmval  22123  nvmval2  22124  nvmfval  22125  nvmul0or  22133  nvsubadd  22136  nvpncan2  22137  nvaddsub4  22142  nvnncan  22144  nvmeq0  22145  nvdif  22154  nvpi  22155  nvmtri  22160  nvabs  22162  imsmetlem  22182  ipval2lem3  22201  ipval2  22203  4ipval2  22204  ipval3  22205  ipval2lem6  22207  nmooge0  22268  blometi  22304  hvaddsub12  22540  hvsubdistr1  22551  hvsubdistr2  22552  hvaddcan2  22573  hvmulcan  22574  hvmulcan2  22575  hvsubcan  22576  hvsubcan2  22577  his7  22592  his2sub  22594  his2sub2  22595  norm3dif2  22653  shsubcl  22723  hhssnv  22764  shlej2  22863  fh2  23121  cm2j  23122  pjoi0  23219  hodcl  23250  hosubdi  23311  unopf1o  23419  unopadj  23422  adj2  23437  braadd  23448  bramul  23449  lnopaddmuli  23476  lnopsubmuli  23478  homco2  23480  lnfnaddmuli  23548  adjlnop  23589  leopmul  23637  leoptr  23640  pjimai  23679  atcv1  23883  atexch  23884  atcvatlem  23888  divnumden2  24161  xdivmul  24171  relogbcl  24402  logblt  24406  hasheuni  24475  difelsiga  24516  cndprobin  24692  bayesth  24697  ghomf1olem  25105  modaddabs  25115  lediv2aALT  25117  mulcan1g  25189  mulcan2g  25190  subdivcomb1  25195  fununiq  25394  dfrdg2  25423  wfrlem4  25541  sltres  25619  nobndlem8  25654  ax5seglem1  25867  axcontlem2  25904  axcontlem8  25910  ltflcei  26239  ftc1anclem4  26283  areacirc  26297  clsun  26331  neiin  26335  filbcmb  26442  ismtybnd  26516  grpoeqdivid  26556  ghomco  26558  rngonegrmul  26568  zerdivemp1x  26571  rngohomco  26590  rngoisoco  26598  riscer  26604  intidl  26639  isfldidl  26678  mzprename  26806  dvdsrabdioph  26870  pell14qrdivcl  26928  monotoddzz  27006  dvdsabsmod0  27057  jm2.19lem2  27061  jm2.19  27064  psgnunilem4  27397  dvconstbi  27528  stoweidlem3  27728  stoweidlem10  27735  stoweidlem19  27744  stoweidlem31  27756  stoweidlem34  27759  stoweidlem44  27769  sigaraf  27819  sigarmf  27820  f13dfv  28081  elfzmlbm  28106  elfzmlbp  28107  fz0fzdiffz0  28119  subsubelfzo0  28135  flltdivnn0lt  28147  modaddmod  28153  modadd2mod  28154  modsubmod  28155  modsubmodmod  28156  modmulmod  28157  ccatsymb  28179  swrdnd  28182  swrdvalodm2  28188  swrd0swrd  28197  swrdswrd  28199  swrdccatin1  28205  swrdccatin12lem3b  28209  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12lem4  28213  swrdccat  28216  swrdccat3a  28217  swrdccat3blem  28218  modprm0  28228  cshwidxmod  28243  2cshw2lem2  28253  2cshwmod  28257  3cshw  28269  cshweqdif2  28270  cshw1  28275  cshw1v  28276  cshwssizelem3  28282  usg2wlkonot  28350  usg2wotspth  28351  2spontn0vne  28354  frgra3v  28392  usg2spot2nb  28454  reccot  28501  rectan  28502  chordthmALT  29045  isosctrlem1ALT  29046  lubunNEW  29771  lshpnelb  29782  opnlen0  29986  lub0N  29987  glb0N  29991  opcon3b  29994  opcon2b  29995  oplecon3b  29998  opltcon3b  30002  opltcon2b  30004  oldmm1  30015  oldmm4  30018  oldmj1  30019  oldmj4  30022  cvrval2  30072  cvrcon3b  30075  leatb  30090  atcmp  30109  atcvreq0  30112  atlatle  30118  athgt  30253  3dim2  30265  islln2a  30314  lplnnleat  30339  lvolnleat  30380  4atlem10  30403  4atlem11  30406  4atlem12  30409  dalem21  30491  dalem22  30492  dalem23  30493  dalem29  30498  dalem30  30499  dalem31N  30500  dalem32  30501  dalem33  30502  dalem34  30503  dalem35  30504  dalem36  30505  dalem37  30506  dalem40  30509  dalem46  30515  dalem47  30516  dalem51  30520  dalem52  30521  dalem58  30527  dalem59  30528  pmaple  30558  paddclN  30639  pmapjoin  30649  pmapjat1  30650  elpcliN  30690  pclssN  30691  pclun2N  30696  2polcon4bN  30715  paddunN  30724  poldmj1N  30725  pmapj2N  30726  pmapocjN  30727  psubclinN  30745  paddatclN  30746  poml4N  30750  lautco  30894  ldilco  30913  ltrneq2  30945  trljat1  30963  cdlemc1  30988  cdleme10  31051  ltrnco  31516  trlcocnv  31517  trljco  31537  trljco2  31538  cdlemi1  31615  tendocnv  31819  diaord  31845  dibord  31957  dihord3  32055  dihord4  32056  dihmeetlem2N  32097  dihmeetlem4preN  32104  dochdmj1  32188  hdmap10lem  32640
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator