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

Theorem 3adant2 977
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 956 . 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 360    /\ w3a 937
This theorem is referenced by:  3ad2ant1  979  eupickb  2348  vtoclegft  3025  eqeu  3107  ordunel  4809  funopg  5487  fnco  5555  dff1o2  5681  fnimapr  5789  fvmptt  5822  fnreseql  5842  f1elima  6011  f1ocnvfvb  6019  oprssov  6217  poxp  6460  smoiso  6626  oaord  6792  oaword  6794  omcan  6814  omwordri  6817  odi  6824  omeulem1  6827  oeord  6833  oecan  6834  oewordri  6837  oeordsuc  6839  nnaord  6864  nnaordr  6865  nndi  6868  nnaword  6872  nnmwordri  6881  erov  7003  ecopovtrn  7009  xpdom3  7208  mapxpen  7275  findcard  7349  indexfi  7416  suppr  7475  r111  7703  tcrank  7810  acndom  7934  infdif2  8092  infxpdom  8093  cfeq0  8138  cfsuc  8139  cfflb  8141  cflim2  8145  cfsmolem  8152  axcc3  8320  domtriomlem  8324  axdc3lem2  8333  axdc3lem4  8335  axdc4lem  8337  axcclem  8339  pwcfsdom  8460  tsktrss  8638  tsksuc  8639  tskuni  8660  adderpqlem  8833  mulerpqlem  8834  mulcanenq  8839  distrnq  8840  ltsonq  8848  ltanq  8850  ltmnq  8851  distrlem1pr  8904  distrlem5pr  8906  ltsopr  8911  ltsosr  8971  ltasr  8977  adddir  9085  axlttrn  9150  letr  9169  ltneOLD  9173  nnncan1  9339  npncan3  9341  pnpcan2  9343  subdi  9469  subdir  9470  divmul  9683  div23  9699  div13  9701  divsubdir  9712  divcan7  9725  ltmul2  9863  lemul1  9864  lemul2  9865  lemul2a  9867  lediv1  9877  ltmuldiv2  9883  lemuldiv  9891  lemuldiv2  9892  ltdiv2  9897  lediv2  9902  infmrlb  9991  nndivtr  10043  bndndx  10222  nn0n0n1ge2  10282  fnn0ind  10371  lbzbi  10566  xrletr  10750  qsqueeze  10789  xleadd2a  10835  xleadd1  10836  xltadd2  10838  xltmul2  10874  supxrbnd  10909  iooneg  11019  iccneg  11020  icoshft  11021  icoshftf1o  11022  fzen  11074  fzrevral2  11134  fzshftral  11136  elfzo  11144  fzoaddel2  11178  fzosubel2  11180  modmulnn  11267  modcyc  11278  moddi  11286  modsubdir  11287  uzindi  11322  axdc4uzlem  11323  expneg2  11392  expdiv  11432  expubnd  11442  bernneq2  11508  hashinfxadd  11661  brfi1indlem  11716  ccatco  11806  swrds2  11882  shftuz  11886  shftval2  11892  abs3dif  12137  sin02gt0  12795  dvdsval2  12857  dvdscmul  12878  dvdsmulc  12879  dvdscmulr  12880  dvdsmulcr  12881  divalglem8  12922  ndvdssub  12929  rpmulgcd  13057  isprm3  13090  coprmdvds  13104  coprimeprodsq  13185  pythagtriplem12  13202  pythagtriplem14  13204  pcprendvds  13216  pcmul  13227  pcdiv  13228  pcqcl  13232  pcqdiv  13233  pcdvdsb  13244  pcgcd  13253  vdwnnlem1  13365  hashbcss  13374  mrcss  13843  mrcsscl  13847  mrcun  13849  cofulid  14089  catcisolem  14263  ple1  14475  latleeqj1  14494  clatl  14545  lubun  14552  clatleglb  14555  pslem  14640  dirtr  14683  pwspjmhm  14769  gsumccat  14789  grpinvid1  14855  grpinvid2  14856  grpinvadd  14869  grpsubf  14870  grpsubrcan  14872  grpinvsub  14873  grpsubeq0  14877  grppncan  14881  grpnpcan  14882  mulgnn0p1  14903  subgsubcl  14957  subgsub  14958  eqglact  14993  divssub  15002  ghmsub  15016  odval2  15191  oddvds2  15204  odsubdvds  15207  gexnnod  15224  slwn0  15251  gsumsn  15545  gsumdixp  15717  dvrcl  15793  unitdvcl  15794  dvrcan1  15798  dvrcan3  15799  dvreq1  15800  subrgdv  15887  abvsubtri  15925  lmodvsubval2  16001  lsmcl  16157  lsmsp2  16161  lspsntrim  16172  lidldvgen  16328  evlslem4  16566  chrcong  16812  zndvds  16832  zntoslem  16839  ocvsscon  16904  obselocv  16957  istps3OLD  16989  ntrin  17127  elnei  17177  neindisj2  17189  ordtopn3  17262  ordtcld3  17265  leordtval2  17278  lecldbas  17285  cnrest2  17352  cmpsublem  17464  ptrescn  17673  xkococn  17694  kqfeq  17758  snfbas  17900  neifil  17914  fclsrest  18058  utopsnnei  18281  neipcfilu  18328  psmetsym  18343  psmetge0  18345  xmetge0  18376  xmetsym  18379  metusttoOLD  18589  metustto  18590  metustblOLD  18612  metustbl  18613  restmetu  18619  nm2dif  18673  nmtri  18674  cnmet  18808  cnmpt2pc  18955  iihalf1  18958  iihalf2  18960  icoopnst  18966  iocopnst  18967  cphsqrcl3  19152  cph2ass  19177  caublcls  19263  bcthlem3  19281  bcthlem4  19282  srabn  19316  iblconst  19711  mpfsubrg  19963  tdeglem3  19984  mdegmullem  20003  dvdsq1p  20085  coeid3  20161  aannenlem2  20248  pserdvlem2  20346  tanord1  20441  efgh  20445  cxpef  20558  recxpcl  20568  lawcos  20660  pythag  20661  isosctrlem1  20664  isosctrlem2  20665  fiusgraedgfi  21423  nbgraf1olem3  21455  nb3graprlem2  21463  cusgra3v  21475  cusgrasizeindslem3  21486  cusgrasizeinds  21487  iswlkon  21533  istrlon  21543  2trllemE  21555  usgrnloop  21565  ispthon  21578  isspthon  21585  usgrcyclnl2  21630  3v3e3cycl1  21633  constr3lem4  21636  constr3lem5  21637  constr3lem6  21638  constr3trllem2  21640  constr3trllem3  21641  4cycl4dv  21656  isgrpo  21786  grpoinvid1  21820  grpoinvid2  21821  grpoasscan1  21827  grpoasscan2  21828  grpoinvop  21831  grpodivinv  21834  grpoinvdiv  21835  grpodivf  21836  grpopncan  21841  grponpcan  21842  grpopnpcan2  21843  gxid  21863  resgrprn  21870  ablonncan  21884  zerdivemp1  22024  vcnegsubdi2  22056  vcsub4  22057  nvmval  22125  nvmval2  22126  nvmfval  22127  nvmul0or  22135  nvsubadd  22138  nvpncan2  22139  nvaddsub4  22144  nvnncan  22146  nvmeq0  22147  nvdif  22156  nvpi  22157  nvmtri  22162  nvabs  22164  imsmetlem  22184  ipval2lem3  22203  ipval2  22205  4ipval2  22206  ipval3  22207  ipval2lem6  22209  nmooge0  22270  blometi  22306  hvaddsub12  22542  hvsubdistr1  22553  hvsubdistr2  22554  hvaddcan2  22575  hvmulcan  22576  hvmulcan2  22577  hvsubcan  22578  hvsubcan2  22579  his7  22594  his2sub  22596  his2sub2  22597  norm3dif2  22655  shsubcl  22725  hhssnv  22766  shlej2  22865  fh2  23123  cm2j  23124  pjoi0  23221  hodcl  23252  hosubdi  23313  unopf1o  23421  unopadj  23424  adj2  23439  braadd  23450  bramul  23451  lnopaddmuli  23478  lnopsubmuli  23480  homco2  23482  lnfnaddmuli  23550  adjlnop  23591  leopmul  23639  leoptr  23642  pjimai  23681  atcv1  23885  atexch  23886  atcvatlem  23890  divnumden2  24163  xdivmul  24173  relogbcl  24404  logblt  24408  hasheuni  24477  difelsiga  24518  cndprobin  24694  bayesth  24699  ghomf1olem  25107  modaddabs  25117  lediv2aALT  25119  mulcan1g  25191  mulcan2g  25192  subdivcomb1  25197  fununiq  25396  dfrdg2  25425  wfrlem4  25543  sltres  25621  nobndlem8  25656  ax5seglem1  25869  axcontlem2  25906  axcontlem8  25912  ltflcei  26241  ftc1anclem4  26285  areacirc  26299  clsun  26333  neiin  26337  filbcmb  26444  ismtybnd  26518  grpoeqdivid  26558  ghomco  26560  rngonegrmul  26570  zerdivemp1x  26573  rngohomco  26592  rngoisoco  26600  riscer  26606  intidl  26641  isfldidl  26680  mzprename  26808  dvdsrabdioph  26872  pell14qrdivcl  26930  monotoddzz  27008  dvdsabsmod0  27059  jm2.19lem2  27063  jm2.19  27066  psgnunilem4  27399  dvconstbi  27530  stoweidlem3  27730  stoweidlem10  27737  stoweidlem19  27746  stoweidlem31  27758  stoweidlem34  27761  stoweidlem44  27771  sigaraf  27821  sigarmf  27822  f13dfv  28083  elfzmlbm  28108  elfzmlbp  28109  fz0fzdiffz0  28121  subsubelfzo0  28137  flltdivnn0lt  28149  modaddmod  28155  modadd2mod  28156  modsubmod  28157  modsubmodmod  28158  modmulmod  28159  ccatsymb  28181  swrdnd  28184  swrdvalodm2  28190  swrd0swrd  28199  swrdswrd  28201  swrdccatin1  28207  swrdccatin12lem3b  28211  swrdccatin2  28212  swrdccatin12lem3  28214  swrdccatin12lem4  28215  swrdccat  28218  swrdccat3a  28219  swrdccat3blem  28220  modprm0  28230  cshwidxmod  28245  2cshw2lem2  28255  2cshwmod  28259  3cshw  28271  cshweqdif2  28272  cshw1  28277  cshw1v  28278  cshwssizelem3  28284  usg2wlkonot  28352  usg2wotspth  28353  2spontn0vne  28356  frgra3v  28394  usg2spot2nb  28456  reccot  28503  rectan  28504  chordthmALT  29047  isosctrlem1ALT  29048  lubunNEW  29773  lshpnelb  29784  opnlen0  29988  lub0N  29989  glb0N  29993  opcon3b  29996  opcon2b  29997  oplecon3b  30000  opltcon3b  30004  opltcon2b  30006  oldmm1  30017  oldmm4  30020  oldmj1  30021  oldmj4  30024  cvrval2  30074  cvrcon3b  30077  leatb  30092  atcmp  30111  atcvreq0  30114  atlatle  30120  athgt  30255  3dim2  30267  islln2a  30316  lplnnleat  30341  lvolnleat  30382  4atlem10  30405  4atlem11  30408  4atlem12  30411  dalem21  30493  dalem22  30494  dalem23  30495  dalem29  30500  dalem30  30501  dalem31N  30502  dalem32  30503  dalem33  30504  dalem34  30505  dalem35  30506  dalem36  30507  dalem37  30508  dalem40  30511  dalem46  30517  dalem47  30518  dalem51  30522  dalem52  30523  dalem58  30529  dalem59  30530  pmaple  30560  paddclN  30641  pmapjoin  30651  pmapjat1  30652  elpcliN  30692  pclssN  30693  pclun2N  30698  2polcon4bN  30717  paddunN  30726  poldmj1N  30727  pmapj2N  30728  pmapocjN  30729  psubclinN  30747  paddatclN  30748  poml4N  30752  lautco  30896  ldilco  30915  ltrneq2  30947  trljat1  30965  cdlemc1  30990  cdleme10  31053  ltrnco  31518  trlcocnv  31519  trljco  31539  trljco2  31540  cdlemi1  31617  tendocnv  31821  diaord  31847  dibord  31959  dihord3  32057  dihord4  32058  dihmeetlem2N  32099  dihmeetlem4preN  32106  dochdmj1  32190  hdmap10lem  32642
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator