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

Theorem 3adant2 1024
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 1003 . 2  |-  ( (
ph  /\  th  /\  ps )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 17 1  |-  ( (
ph  /\  th  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  3ad2ant1  1026  eupickb  2338  vtoclegft  3159  eqeu  3248  funopg  5633  fnco  5702  dff1o2  5836  fnimapr  5945  fvmptt  5981  fnreseql  6007  f1elima  6179  f13dfv  6188  f1ocnvfvb  6193  oprssov  6452  ordunel  6668  poxp  6919  wfrlem4  7047  smoiso  7089  oaord  7256  oaword  7258  omcan  7278  omwordri  7281  odi  7288  omeulem1  7291  oeord  7297  oecan  7298  oewordri  7301  oeordsuc  7303  nnaord  7328  nnaordr  7329  nndi  7332  nnaword  7336  nnmwordri  7345  erov  7468  ecopovtrn  7474  xpdom3  7676  mapxpen  7744  findcard  7816  indexfi  7888  suppr  7993  infpr  8019  r111  8245  tcrank  8354  acndom  8480  infdif2  8638  infxpdom  8639  cfeq0  8684  cfsuc  8685  cfflb  8687  cflim2  8691  cfsmolem  8698  axcc3  8866  domtriomlem  8870  axdc3lem2  8879  axdc3lem4  8881  axdc4lem  8883  axcclem  8885  pwcfsdom  9006  tsktrss  9185  tsksuc  9186  tskuni  9207  adderpqlem  9378  mulerpqlem  9379  mulcanenq  9384  distrnq  9385  ltsonq  9393  ltanq  9395  ltmnq  9396  distrlem1pr  9449  distrlem5pr  9451  ltsopr  9456  ltsosr  9517  ltasr  9523  adddir  9633  axlttrn  9705  letr  9726  ltneOLD  9730  nnncan1  9909  npncan3  9911  pnpcan2  9913  subdi  10051  subdir  10052  mulcan1g  10264  mulcan2g  10265  divmul  10272  div23  10288  div13  10290  divsubdir  10302  divcan7  10315  ltmul2  10455  lemul1  10456  lemul2  10457  lemul2a  10459  lediv1  10469  ltmuldiv2  10478  lemuldiv  10485  lemuldiv2  10486  ltdiv2  10491  lediv2  10496  fiminre  10555  infrelb  10596  infmrlbOLD  10597  nndivtr  10651  bndndx  10868  nn0n0n1ge2  10932  fnn0ind  11034  xrletr  11455  qsqueeze  11494  xleadd2a  11540  xleadd1  11541  xltadd2  11543  xltmul2  11579  supxrbnd  11614  iooneg  11750  iccneg  11751  icoshft  11752  icoshftf1o  11753  fzen  11814  uzsubsubfz  11819  fzrevral2  11878  fzshftral  11880  fz0fzdiffz0  11897  elfzmlbmOLD  11899  elfzmlbp  11900  elfzo  11920  nelfzo  11923  fzoaddel2  11967  fzosubel2  11971  elfzom1p1elfzo  11990  ssfzo12bi  12003  fzonfzoufzol  12009  flltdivnn0lt  12062  modmulnn  12111  modcyc  12129  modaddabs  12132  modaddmod  12133  modadd2mod  12137  modsubmod  12145  modsubmodmod  12146  modaddmodup  12150  modmulmod  12152  moddi  12154  modsubdir  12155  uzindi  12191  axdc4uzlem  12192  expneg2  12278  expdiv  12320  expubnd  12330  bernneq2  12396  hashinfxadd  12561  brfi1indlem  12640  ccatval3  12711  ccatsymb  12714  ccatfv0  12715  ccatval1lsw  12716  ccats1val2  12745  swrdnd  12773  2swrd1eqwrdeq  12795  swrdswrd  12801  wrd2ind  12819  swrdccatin1  12824  swrdccatin12lem2b  12827  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12lem3  12831  swrdccat  12834  swrdccat3a  12835  swrdccat3blem  12836  repswswrd  12872  repswccat  12873  cshwidxmod  12890  2cshw  12897  3cshw  12902  scshwfzeqfzo  12910  cshwcsh2id  12912  ccatco  12917  cshco  12918  swrdco  12919  lswco  12920  swrds2  12999  2swrd2eqwrdeq  13007  shftuz  13111  shftval2  13117  abs3dif  13373  modfsummods  13831  sin02gt0  14224  dvdsval2  14286  dvdscmul  14307  dvdsmulc  14308  dvdscmulr  14309  dvdsmulcr  14310  mulmoddvds  14341  divalglem8  14356  ndvdssub  14363  rpmulgcd  14494  isprm3  14595  coprmdvds  14621  coprmprod  14640  modprm0  14710  coprimeprodsq  14713  pythagtriplem12  14730  pythagtriplem14  14732  pcprendvds  14744  pcmul  14755  pcdiv  14756  pcqcl  14760  pcqdiv  14761  pcdvdsb  14772  pcgcd  14781  vdwnnlem1  14899  hashbcss  14910  cshwshashlem1  15020  fvsetsid  15102  mrcss  15464  mrcsscl  15468  mrcun  15470  cofulid  15737  catcisolem  15943  funcsetcestrclem9  15990  latleeqj1  16251  lubun  16311  clatleglb  16314  pslem  16394  dirtr  16424  mgmb1mgm1  16441  pwspjmhm  16557  gsumccat  16567  grpinvid1  16656  grpinvid2  16657  grpinvadd  16674  grpsubf  16675  grpsubrcan  16677  grpinvsub  16678  grpsubeq0  16682  grpsubadd0sub  16683  grppncan  16687  grpnpcan  16688  mulgnn0p1  16711  subgsubcl  16770  subgsub  16771  eqglact  16810  qussub  16819  ghmsub  16833  psgnunilem4  17080  oddvds2  17146  odsubdvds  17149  gexnnod  17166  slwn0  17193  gsumdixp  17763  dvrcl  17840  unitdvcl  17841  dvrcan1  17845  dvrcan3  17846  dvreq1  17847  subrgdv  17951  abvsubtri  17989  idsrngd  18016  lmodvsubval2  18069  lsmcl  18232  lsmsp2  18236  lspsntrim  18247  lidldvgen  18405  evlslem4  18657  mpfsubrg  18681  ply1tmcl  18791  eqcoe1ply1eq  18817  gsummoncoe1  18824  lply1binomsc  18827  chrcong  19022  zndvds  19042  zntoslem  19049  ocvsscon  19160  obselocv  19213  frlmphl  19261  mamudm  19335  mamufacex  19336  scmatf1  19478  scmatf1o  19479  scmatrngiso  19483  submabas  19525  mdetdiaglem  19545  mdetralt2  19556  mdetero  19557  mdetunilem2  19560  mdetunilem6  19564  m2detleiblem7  19574  maducoeval2  19587  gsummatr01lem3  19604  gsummatr01  19606  smadiadetglem2  19619  cramerlem1  19634  mply1topmatcl  19751  mp2pm2mplem4  19755  ntrin  19998  elnei  20049  neindisj2  20061  ordtopn3  20134  ordtcld3  20137  leordtval2  20150  lecldbas  20157  cnrest2  20224  cmpsublem  20336  ptrescn  20576  xkococn  20597  kqfeq  20661  snfbas  20803  neifil  20817  fclsrest  20961  utopsnnei  21186  neipcfilu  21233  psmetsym  21248  psmetge0  21250  xmetge0  21281  xmetsym  21284  metustto  21490  metustbl  21503  restmetu  21507  nm2dif  21560  nmtri  21561  cnmet  21694  cnmpt2pc  21843  iihalf1  21846  iihalf2  21848  iocopnst  21855  cphsqrtcl3  22049  cph2ass  22074  caublcls  22162  bcthlem3  22178  bcthlem4  22179  srabn  22211  rrxmet  22246  iblconst  22643  tdeglem3  22876  mdegmullem  22895  dvdsq1p  22977  coeid3  23053  aannenlem2  23141  pserdvlem2  23239  tanord1  23342  cxpef  23466  recxpcl  23476  logbchbase  23564  relogbcl  23566  relogbzcl  23567  logbleb  23576  logblt  23577  relogbcxpb  23580  lawcos  23601  pythag  23602  isosctrlem1  23603  isosctrlem2  23604  ax5seglem1  24795  axcontlem2  24832  axcontlem8  24838  fiusgraedgfi  24971  nbgraf1olem3  25007  nb3graprlem2  25016  cusgra3v  25028  cusgrasizeindslem3  25039  cusgrasizeinds  25040  iswlkon  25098  istrlon  25107  2trllemE  25119  usgrnloop  25129  ispthon  25142  isspthon  25149  usgra2adedgwlkonALT  25180  usgrcyclnl2  25205  3v3e3cycl1  25208  constr3lem4  25211  constr3lem5  25212  constr3lem6  25213  constr3trllem2  25215  constr3trllem3  25216  4cycl4dv  25231  wwlkextproplem3  25307  clwwlkgt0  25335  clwwlknndef  25337  clwwlknfi  25342  clwlkisclwwlklem2a4  25348  clwlkisclwwlklem2a  25349  clwwlkel  25357  clwwlkext2edg  25366  clwwisshclwwlem1  25369  clwwnisshclwwn  25373  erclwwlktr  25379  erclwwlkntr  25391  clwlkfclwwlk  25408  clwlkfoclwwlk  25409  usg2wotspth  25448  2spontn0vne  25451  nbhashnn0  25478  nbhashuvtx  25480  usgrauvtxvdbi  25484  rusgra0edg  25519  frgra3v  25566  usg2spot2nb  25629  numclwlk3lem3  25637  extwwlkfablem2  25642  numclwwlkovf2ex  25650  numclwwlkovgelim  25653  numclwwlk4  25674  numclwwlk5lem  25675  numclwwlk5  25676  numclwwlk6  25677  numclwwlk7  25678  isgrpo  25760  grpoinvid1  25794  grpoinvid2  25795  grpoasscan1  25801  grpoasscan2  25802  grpoinvop  25805  grpodivinv  25808  grpoinvdiv  25809  grpodivf  25810  grpopncan  25815  grponpcan  25816  grpopnpcan2  25817  gxid  25837  resgrprn  25844  ablonncan  25858  zerdivemp1  25998  vcnegsubdi2  26030  vcsub4  26031  nvmval  26099  nvmval2  26100  nvmfval  26101  nvmul0or  26109  nvsubadd  26112  nvpncan2  26113  nvaddsub4  26118  nvnncan  26120  nvmeq0  26121  nvdif  26130  nvpi  26131  nvmtri  26136  nvabs  26138  imsmetlem  26158  ipval2lem3  26177  ipval2  26179  4ipval2  26180  ipval3  26181  ipval2lem6  26183  nmooge0  26244  blometi  26280  hvaddsub12  26517  hvsubdistr1  26528  hvsubdistr2  26529  hvaddcan2  26550  hvmulcan  26551  hvmulcan2  26552  hvsubcan  26553  hvsubcan2  26554  his7  26569  his2sub  26571  his2sub2  26572  norm3dif2  26630  shsubcl  26699  hhssnv  26741  shlej2  26840  fh2  27098  cm2j  27099  pjoi0  27196  hodcl  27226  hosubdi  27287  unopf1o  27395  unopadj  27398  adj2  27413  braadd  27424  bramul  27425  lnopaddmuli  27452  lnopsubmuli  27454  homco2  27456  lnfnaddmuli  27524  adjlnop  27565  leopmul  27613  leoptr  27616  pjimai  27655  atcv1  27859  atexch  27860  atcvatlem  27864  fcoinvbr  28045  divnumden2  28210  xdivmul  28223  resvsca  28423  hasheuni  28736  difelsiga  28785  cndprobin  29084  bayesth  29089  sgn3da  29191  ghomf1olem  30091  lediv2aALT  30100  subdivcomb1  30138  fununiq  30188  dfrdg2  30220  sltres  30329  nobndlem8  30364  clsun  30760  neiin  30764  poimirlem32  31666  ftc1anclem4  31714  areacirc  31731  filbcmb  31761  ismtybnd  31833  grpoeqdivid  31873  ghomco  31875  rngonegrmul  31885  zerdivemp1x  31888  rngohomco  31907  rngoisoco  31915  riscer  31921  intidl  31956  isfldidl  31995  lshpnelb  32249  opnlen0  32453  opcon3b  32461  opcon2b  32462  oplecon3b  32465  opltcon3b  32469  opltcon2b  32471  oldmm1  32482  oldmm4  32485  oldmj1  32486  oldmj4  32489  cvrval2  32539  cvrcon3b  32542  leatb  32557  atcmp  32576  atcvreq0  32579  atlatle  32585  athgt  32720  3dim2  32732  islln2a  32781  lplnnleat  32806  lvolnleat  32847  4atlem10  32870  4atlem11  32873  4atlem12  32876  dalem21  32958  dalem22  32959  dalem23  32960  dalem29  32965  dalem30  32966  dalem31N  32967  dalem32  32968  dalem33  32969  dalem34  32970  dalem35  32971  dalem36  32972  dalem37  32973  dalem40  32976  dalem46  32982  dalem47  32983  dalem51  32987  dalem52  32988  dalem58  32994  dalem59  32995  pmaple  33025  paddclN  33106  pmapjoin  33116  pmapjat1  33117  elpcliN  33157  pclssN  33158  pclun2N  33163  2polcon4bN  33182  paddunN  33191  poldmj1N  33192  pmapj2N  33193  pmapocjN  33194  psubclinN  33212  paddatclN  33213  poml4N  33217  lautco  33361  ldilco  33380  ltrneq2  33412  trljat1  33431  cdlemc1  33456  cdleme10  33519  ltrnco  33985  trlcocnv  33986  trljco  34006  trljco2  34007  cdlemi1  34084  tendocnv  34288  diaord  34314  dibord  34426  dihord3  34524  dihord4  34525  dihmeetlem2N  34566  dihmeetlem4preN  34573  dochdmj1  34657  hdmap10lem  35109  mzprename  35290  dvdsrabdioph  35352  pell14qrdivcl  35409  monotoddzz  35487  dvdsabsmod0OLD  35537  jm2.19lem2  35541  jm2.19  35544  relexpaddss  35939  dvconstbi  36310  chordthmALT  36960  isosctrlem1ALT  36961  unima  37041  wessf1ornlem  37072  disjf1o  37079  disjinfi  37081  upbdrech  37122  iuneqfzuzlem  37156  suplesup  37161  cncfshift  37313  cncfperiod  37318  cncfuni  37326  icccncfext  37327  dvmptfprodlem  37378  dvnprodlem1  37380  itgspltprt  37415  stoweidlem3  37422  stoweidlem10  37429  stoweidlem19  37438  stoweidlem31  37451  stoweidlem34  37454  stoweidlem44  37464  fourierdlem41  37569  fourierdlem42  37570  fourierdlem51  37579  fourierdlem68  37596  fourierdlem89  37617  fourierdlem91  37619  fourierdlem92  37620  fourierdlem94  37622  etransclem24  37680  etransclem34  37690  salincl  37721  saldifcl2  37724  sge0pr  37760  sge0pnffigt  37762  nnfoctbdjlem  37792  nnfoctbdj  37793  meadjiunlem  37802  caratheodorylem2  37847  sigaraf  37852  sigarmf  37853  nltle2tri  38096  iccpartiltu  38116  icceuelpart  38130  bgoldbtbndlem2  38281  pfxsuffeqwrdeq  38327  pfxsuff1eqwrdeq  38328  ccatpfx  38330  pfxpfx  38336  pfxccatin12lem1  38344  pfxccatpfx1  38348  pfxccatpfx2  38349  repswpfx  38357  pfxco  38359  subsubelfzo0  38401  xpprsng  38863  nn0sumltlt  38881  invginvrid  38902  ply1sclrmsm  38925  linccl  38957  lincvalpr  38961  lincresunit3lem1  39022  lincresunit3  39024  fdivmpt  39102  nnolog2flm1  39152  dignnld  39165  digexp  39169  dignn0flhalflem1  39177  reccot  39229  rectan  39230
  Copyright terms: Public domain W3C validator