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

Theorem 3adant2 1033
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 1012 . 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 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  3ad2ant1  1035  eupickb  2378  vtoclegft  3133  eqeu  3221  funopg  5637  fnco  5710  dff1o2  5846  fnimapr  5957  fvmptt  5993  fnreseql  6020  f1elima  6194  f13dfv  6203  f1ocnvfvb  6208  oprssov  6470  ordunel  6686  poxp  6940  wfrlem4  7070  smoiso  7112  oaord  7279  oaword  7281  omcan  7301  omwordri  7304  odi  7311  omeulem1  7314  oeord  7320  oecan  7321  oewordri  7324  oeordsuc  7326  nnaord  7351  nnaordr  7352  nndi  7355  nnaword  7359  nnmwordri  7368  erov  7491  ecopovtrn  7497  xpdom3  7701  mapxpen  7769  findcard  7841  indexfi  7913  suppr  8018  infpr  8050  r111  8277  tcrank  8386  acndom  8513  infdif2  8671  infxpdom  8672  cfeq0  8717  cfsuc  8718  cfflb  8720  cflim2  8724  cfsmolem  8731  axcc3  8899  domtriomlem  8903  axdc3lem2  8912  axdc3lem4  8914  axdc4lem  8916  axcclem  8918  pwcfsdom  9039  tsktrss  9217  tsksuc  9218  tskuni  9239  adderpqlem  9410  mulerpqlem  9411  mulcanenq  9416  distrnq  9417  ltsonq  9425  ltanq  9427  ltmnq  9428  distrlem1pr  9481  distrlem5pr  9483  ltsopr  9488  ltsosr  9549  ltasr  9555  adddir  9665  axlttrn  9737  letr  9758  ltneOLD  9762  nnncan1  9941  npncan3  9943  pnpcan2  9945  subdi  10085  subdir  10086  mulcan1g  10298  mulcan2g  10299  divmul  10306  div23  10322  div13  10324  divsubdir  10336  divcan7  10349  ltmul2  10489  lemul1  10490  lemul2  10491  lemul2a  10493  lediv1  10503  ltmuldiv2  10512  lemuldiv  10519  lemuldiv2  10520  ltdiv2  10525  lediv2  10529  fiminre  10588  infrelb  10629  infmrlbOLD  10630  nndivtr  10684  bndndx  10902  nn0n0n1ge2  10966  fnn0ind  11068  xrletr  11489  qsqueeze  11528  xleadd2a  11574  xleadd1  11575  xltadd2  11577  xltmul2  11613  supxrbnd  11648  iooneg  11787  iccneg  11788  icoshft  11789  icoshftf1o  11790  fzen  11851  uzsubsubfz  11856  fzrevral2  11915  fzshftral  11917  fz0fzdiffz0  11935  elfzmlbmOLD  11937  elfzmlbp  11938  elfzo  11959  nelfzo  11962  fzoaddel2  12007  fzosubel2  12011  elfzom1p1elfzo  12030  ssfzo12bi  12043  fzonfzoufzol  12049  flltdivnn0lt  12103  modmulnn  12152  modcyc  12170  modaddabs  12173  modaddmod  12174  modadd2mod  12178  modsubmod  12186  modsubmodmod  12187  modaddmodup  12191  modmulmod  12193  moddi  12195  modsubdir  12196  uzindi  12232  axdc4uzlem  12233  expneg2  12319  expdiv  12361  expubnd  12371  bernneq2  12437  hashinfxadd  12602  brfi1indlem  12688  ccatval3  12766  ccatsymb  12769  ccatfv0  12770  ccatval1lsw  12771  ccats1val2  12803  swrdnd  12831  2swrd1eqwrdeq  12853  swrdswrd  12859  wrd2ind  12877  swrdccatin1  12882  swrdccatin12lem2b  12885  swrdccatin2  12886  swrdccatin12lem2  12888  swrdccatin12lem3  12889  swrdccat  12892  swrdccat3a  12893  swrdccat3blem  12894  repswswrd  12930  repswccat  12931  cshwidxmod  12948  2cshw  12955  3cshw  12960  scshwfzeqfzo  12968  cshwcsh2id  12970  ccatco  12975  cshco  12976  swrdco  12977  lswco  12978  swrds2  13072  2swrd2eqwrdeq  13083  shftuz  13187  shftval2  13193  abs3dif  13449  modfsummods  13908  sin02gt0  14301  dvdsval2  14363  dvdscmul  14384  dvdsmulc  14385  dvdscmulr  14386  dvdsmulcr  14387  mulmoddvds  14418  divalglem8  14435  ndvdssub  14443  rpmulgcd  14578  isprm3  14688  coprmdvds  14714  coprmprod  14733  modprm0  14811  coprimeprodsq  14814  pythagtriplem12  14831  pythagtriplem14  14833  pcprendvds  14845  pcmul  14856  pcdiv  14857  pcqcl  14861  pcqdiv  14862  pcdvdsb  14873  pcgcd  14882  vdwnnlem1  15000  hashbcss  15011  cshwshashlem1  15121  fvsetsid  15203  mrcss  15577  mrcsscl  15581  mrcun  15583  cofulid  15850  catcisolem  16056  funcsetcestrclem9  16103  latleeqj1  16364  lubun  16424  clatleglb  16427  pslem  16507  dirtr  16537  mgmb1mgm1  16554  pwspjmhm  16670  gsumccat  16680  grpinvid1  16769  grpinvid2  16770  grpinvadd  16787  grpsubf  16788  grpsubrcan  16790  grpinvsub  16791  grpsubeq0  16795  grpsubadd0sub  16796  grppncan  16800  grpnpcan  16801  mulgnn0p1  16824  subgsubcl  16883  subgsub  16884  eqglact  16923  qussub  16932  ghmsub  16946  psgnunilem4  17193  oddvds2  17272  odsubdvds  17275  gexnnod  17295  slwn0  17322  gsumdixp  17892  dvrcl  17969  unitdvcl  17970  dvrcan1  17974  dvrcan3  17975  dvreq1  17976  subrgdv  18080  abvsubtri  18118  idsrngd  18145  lmodvsubval2  18198  lsmcl  18361  lsmsp2  18365  lspsntrim  18376  lidldvgen  18534  evlslem4  18786  mpfsubrg  18810  ply1tmcl  18920  eqcoe1ply1eq  18946  gsummoncoe1  18953  lply1binomsc  18956  chrcong  19155  zndvds  19175  zntoslem  19182  ocvsscon  19293  obselocv  19346  frlmphl  19394  mamudm  19468  mamufacex  19469  scmatf1  19611  scmatf1o  19612  scmatrngiso  19616  submabas  19658  mdetdiaglem  19678  mdetralt2  19689  mdetero  19690  mdetunilem2  19693  mdetunilem6  19697  m2detleiblem7  19707  maducoeval2  19720  gsummatr01lem3  19737  gsummatr01  19739  smadiadetglem2  19752  cramerlem1  19767  mply1topmatcl  19884  mp2pm2mplem4  19888  ntrin  20131  elnei  20182  neindisj2  20194  ordtopn3  20267  ordtcld3  20270  leordtval2  20283  lecldbas  20290  cnrest2  20357  cmpsublem  20469  ptrescn  20709  xkococn  20730  kqfeq  20794  snfbas  20936  neifil  20950  fclsrest  21094  utopsnnei  21319  neipcfilu  21366  psmetsym  21381  psmetge0  21383  xmetge0  21414  xmetsym  21417  metustto  21623  metustbl  21636  restmetu  21640  nm2dif  21693  nmtri  21694  cnmet  21847  cnmpt2pc  22011  iihalf1  22014  iihalf2  22016  iocopnst  22023  cphsqrtcl3  22220  cph2ass  22245  caublcls  22333  bcthlem3  22349  bcthlem4  22350  srabn  22382  rrxmet  22417  iblconst  22831  tdeglem3  23064  mdegmullem  23083  dvdsq1p  23167  coeid3  23250  aannenlem2  23341  pserdvlem2  23439  tanord1  23542  cxpef  23666  recxpcl  23676  logbchbase  23764  relogbcl  23766  relogbzcl  23767  logbleb  23776  logblt  23777  relogbcxpb  23780  lawcos  23801  pythag  23802  isosctrlem1  23803  isosctrlem2  23804  ax5seglem1  25014  axcontlem2  25051  axcontlem8  25057  fiusgraedgfi  25191  nbgraf1olem3  25227  nb3graprlem2  25236  cusgra3v  25248  cusgrasizeindslem3  25259  cusgrasizeinds  25260  iswlkon  25318  istrlon  25327  2trllemE  25339  usgrwlknloop  25349  ispthon  25362  isspthon  25369  usgra2adedgwlkonALT  25400  usgrcyclnl2  25425  3v3e3cycl1  25428  constr3lem4  25431  constr3lem5  25432  constr3lem6  25433  constr3trllem2  25435  constr3trllem3  25436  4cycl4dv  25451  wwlkextproplem3  25527  clwwlkgt0  25555  clwwlknndef  25557  clwwlknfi  25562  clwlkisclwwlklem2a4  25568  clwlkisclwwlklem2a  25569  clwwlkel  25577  clwwlkext2edg  25586  clwwisshclwwlem1  25589  clwwnisshclwwn  25593  erclwwlktr  25599  erclwwlkntr  25611  clwlkfclwwlk  25628  clwlkfoclwwlk  25629  usg2wotspth  25668  2spontn0vne  25671  nbhashnn0  25698  nbhashuvtx  25700  usgrauvtxvdbi  25704  rusgra0edg  25739  frgra3v  25786  usg2spot2nb  25849  numclwlk3lem3  25857  extwwlkfablem2  25862  numclwwlkovf2ex  25870  numclwwlkovgelim  25873  numclwwlk4  25894  numclwwlk5lem  25895  numclwwlk5  25896  numclwwlk6  25897  numclwwlk7  25898  isgrpo  25980  grpoinvid1  26014  grpoinvid2  26015  grpoasscan1  26021  grpoasscan2  26022  grpoinvop  26025  grpodivinv  26028  grpoinvdiv  26029  grpodivf  26030  grpopncan  26035  grponpcan  26036  grpopnpcan2  26037  gxid  26057  resgrprn  26064  ablonncan  26078  zerdivemp1  26218  vcnegsubdi2  26250  vcsub4  26251  nvmval  26319  nvmval2  26320  nvmfval  26321  nvmul0or  26329  nvsubadd  26332  nvpncan2  26333  nvaddsub4  26338  nvnncan  26340  nvmeq0  26341  nvdif  26350  nvpi  26351  nvmtri  26356  nvabs  26358  imsmetlem  26378  ipval2lem3  26397  ipval2  26399  4ipval2  26400  ipval3  26401  ipval2lem6  26403  nmooge0  26464  blometi  26500  hvaddsub12  26747  hvsubdistr1  26758  hvsubdistr2  26759  hvaddcan2  26780  hvmulcan  26781  hvmulcan2  26782  hvsubcan  26783  hvsubcan2  26784  his7  26799  his2sub  26801  his2sub2  26802  norm3dif2  26860  shsubcl  26929  hhssnv  26971  shlej2  27070  fh2  27328  cm2j  27329  pjoi0  27426  hodcl  27456  hosubdi  27517  unopf1o  27625  unopadj  27628  adj2  27643  braadd  27654  bramul  27655  lnopaddmuli  27682  lnopsubmuli  27684  homco2  27686  lnfnaddmuli  27754  adjlnop  27795  leopmul  27843  leoptr  27846  pjimai  27885  atcv1  28089  atexch  28090  atcvatlem  28094  fcoinvbr  28268  divnumden2  28433  xdivmul  28446  resvsca  28644  hasheuni  28957  difelsiga  29006  cndprobin  29317  bayesth  29322  sgn3da  29462  ghomf1olem  30362  lediv2aALT  30371  subdivcomb1  30410  fununiq  30460  dfrdg2  30492  sltres  30601  nobndlem8  30638  clsun  31034  neiin  31038  rdgeqoa  31819  poimirlem32  32018  ftc1anclem4  32066  areacirc  32083  filbcmb  32113  ismtybnd  32185  grpoeqdivid  32225  ghomco  32227  rngonegrmul  32237  zerdivemp1x  32240  rngohomco  32259  rngoisoco  32267  riscer  32273  intidl  32308  isfldidl  32347  lshpnelb  32596  opnlen0  32800  opcon3b  32808  opcon2b  32809  oplecon3b  32812  opltcon3b  32816  opltcon2b  32818  oldmm1  32829  oldmm4  32832  oldmj1  32833  oldmj4  32836  cvrval2  32886  cvrcon3b  32889  leatb  32904  atcmp  32923  atcvreq0  32926  atlatle  32932  athgt  33067  3dim2  33079  islln2a  33128  lplnnleat  33153  lvolnleat  33194  4atlem10  33217  4atlem11  33220  4atlem12  33223  dalem21  33305  dalem22  33306  dalem23  33307  dalem29  33312  dalem30  33313  dalem31N  33314  dalem32  33315  dalem33  33316  dalem34  33317  dalem35  33318  dalem36  33319  dalem37  33320  dalem40  33323  dalem46  33329  dalem47  33330  dalem51  33334  dalem52  33335  dalem58  33341  dalem59  33342  pmaple  33372  paddclN  33453  pmapjoin  33463  pmapjat1  33464  elpcliN  33504  pclssN  33505  pclun2N  33510  2polcon4bN  33529  paddunN  33538  poldmj1N  33539  pmapj2N  33540  pmapocjN  33541  psubclinN  33559  paddatclN  33560  poml4N  33564  lautco  33708  ldilco  33727  ltrneq2  33759  trljat1  33778  cdlemc1  33803  cdleme10  33866  ltrnco  34332  trlcocnv  34333  trljco  34353  trljco2  34354  cdlemi1  34431  tendocnv  34635  diaord  34661  dibord  34773  dihord3  34871  dihord4  34872  dihmeetlem2N  34913  dihmeetlem4preN  34920  dochdmj1  35004  hdmap10lem  35456  mzprename  35637  dvdsrabdioph  35699  pell14qrdivcl  35757  monotoddzz  35837  dvdsabsmod0OLD  35887  jm2.19lem2  35891  jm2.19  35894  relexpaddss  36356  dvconstbi  36728  chordthmALT  37371  isosctrlem1ALT  37372  unima  37483  wessf1ornlem  37513  disjf1o  37520  disjinfi  37522  ssnnf1octb  37524  projf1o  37528  mapsnd  37530  mapssbi  37551  iunmapsn  37555  upbdrech  37598  iuneqfzuzlem  37632  suplesup  37637  cncfshift  37837  cncfperiod  37842  cncfuni  37850  icccncfext  37851  dvmptfprodlem  37905  dvnprodlem1  37907  itgspltprt  37942  ismbl3  37950  stoweidlem3  37964  stoweidlem10  37971  stoweidlem19  37980  stoweidlem31  37993  stoweidlem34  37996  stoweidlem44  38006  fourierdlem41  38112  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem51  38122  fourierdlem68  38139  fourierdlem89  38160  fourierdlem91  38162  fourierdlem92  38163  fourierdlem94  38165  etransclem24  38224  etransclem34  38234  rrxdsfi  38255  qndenserrnbllem  38264  salincl  38285  saldifcl2  38288  sge0pr  38339  sge0pnffigt  38341  nnfoctbdjlem  38398  nnfoctbdj  38399  meadjiunlem  38408  caratheodorylem2  38456  hoidmv1le  38523  hoidmvlelem3  38526  hspmbllem2  38556  opnvonmbllem2  38562  sigaraf  38597  sigarmf  38598  nltle2tri  38851  iccpartiltu  38871  icceuelpart  38885  bgoldbtbndlem2  39036  pfxsuffeqwrdeq  39084  pfxsuff1eqwrdeq  39085  ccatpfx  39087  pfxpfx  39093  pfxccatin12lem1  39101  pfxccatpfx1  39105  pfxccatpfx2  39106  repswpfx  39114  pfxco  39116  subsubelfzo0  39200  issubgr2  39490  uhgrissubgr  39493  egrsubgr  39495  fusgrfisstep  39541  nbusgrfi  39594  nb3grprlem2  39601  cplgr3v  39648  cusgrsizeindslem  39658  vtxdgfival  39676  rusgrpropadjvtx  39747  1wlkvtxiedg  39783  upgr1wlkvtxedg  39800  uspgrn2crct  39922  umgr2adedgwlklem  39989  uhgr3cyclex  40019  umgr3cyclex  40020  xpprsng  40482  nn0sumltlt  40500  invginvrid  40521  ply1sclrmsm  40544  linccl  40576  lincvalpr  40580  lincresunit3lem1  40641  lincresunit3  40643  fdivmpt  40720  nnolog2flm1  40770  dignnld  40783  digexp  40787  dignn0flhalflem1  40795  reccot  40847  rectan  40848
  Copyright terms: Public domain W3C validator