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

Theorem 3adant2 1013
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 992 . 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 setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 185  df-an 369  df-3an 973
This theorem is referenced by:  3ad2ant1  1015  eupickb  2291  vtoclegft  3106  eqeu  3195  funopg  5528  fnco  5597  dff1o2  5729  fnimapr  5838  fvmptt  5873  fnreseql  5899  f1elima  6072  f13dfv  6081  f1ocnvfvb  6086  oprssov  6343  ordunel  6561  poxp  6811  smoiso  6951  oaord  7114  oaword  7116  omcan  7136  omwordri  7139  odi  7146  omeulem1  7149  oeord  7155  oecan  7156  oewordri  7159  oeordsuc  7161  nnaord  7186  nnaordr  7187  nndi  7190  nnaword  7194  nnmwordri  7203  erov  7326  ecopovtrn  7332  xpdom3  7534  mapxpen  7602  findcard  7674  indexfi  7743  suppr  7844  r111  8106  tcrank  8215  acndom  8345  infdif2  8503  infxpdom  8504  cfeq0  8549  cfsuc  8550  cfflb  8552  cflim2  8556  cfsmolem  8563  axcc3  8731  domtriomlem  8735  axdc3lem2  8744  axdc3lem4  8746  axdc4lem  8748  axcclem  8750  pwcfsdom  8871  tsktrss  9050  tsksuc  9051  tskuni  9072  adderpqlem  9243  mulerpqlem  9244  mulcanenq  9249  distrnq  9250  ltsonq  9258  ltanq  9260  ltmnq  9261  distrlem1pr  9314  distrlem5pr  9316  ltsopr  9321  ltsosr  9382  ltasr  9388  adddir  9498  axlttrn  9568  letr  9589  ltneOLD  9593  nnncan1  9768  npncan3  9770  pnpcan2  9772  subdi  9908  subdir  9909  mulcan1g  10119  mulcan2g  10120  divmul  10127  div23  10143  div13  10145  divsubdir  10157  divcan7  10170  ltmul2  10310  lemul1  10311  lemul2  10312  lemul2a  10314  lediv1  10324  ltmuldiv2  10333  lemuldiv  10340  lemuldiv2  10341  ltdiv2  10346  lediv2  10351  infmrlb  10440  nndivtr  10494  bndndx  10711  nn0n0n1ge2  10776  fnn0ind  10878  xrletr  11282  qsqueeze  11321  xleadd2a  11367  xleadd1  11368  xltadd2  11370  xltmul2  11406  supxrbnd  11441  iooneg  11561  iccneg  11562  icoshft  11563  icoshftf1o  11564  fzen  11624  uzsubsubfz  11628  fzrevral2  11686  fzshftral  11688  fz0fzdiffz0  11705  elfzmlbmOLD  11707  elfzmlbp  11708  elfzo  11724  nelfzo  11727  fzoaddel2  11771  fzosubel2  11775  elfzom1p1elfzo  11794  ssfzo12bi  11806  fzonfzoufzol  11812  flltdivnn0lt  11865  modmulnn  11914  modcyc  11932  modaddabs  11935  modaddmod  11936  modadd2mod  11940  modsubmod  11948  modsubmodmod  11949  modaddmodup  11953  modmulmod  11955  moddi  11957  modsubdir  11958  uzindi  11994  axdc4uzlem  11995  expneg2  12078  expdiv  12119  expubnd  12129  bernneq2  12195  hashinfxadd  12356  brfi1indlem  12435  ccatval3  12506  ccatsymb  12509  ccatfv0  12510  ccatval1lsw  12511  ccats1val2  12540  swrdnd  12568  2swrd1eqwrdeq  12590  swrdswrd  12596  wrd2ind  12614  swrdccatin1  12619  swrdccatin12lem2b  12622  swrdccatin2  12623  swrdccatin12lem2  12625  swrdccatin12lem3  12626  swrdccat  12629  swrdccat3a  12630  swrdccat3blem  12631  repswswrd  12667  repswccat  12668  cshwidxmod  12685  2cshw  12692  3cshw  12697  scshwfzeqfzo  12705  cshwcsh2id  12707  ccatco  12712  cshco  12713  swrdco  12714  lswco  12715  swrds2  12794  2swrd2eqwrdeq  12802  shftuz  12904  shftval2  12910  abs3dif  13166  modfsummods  13609  sin02gt0  13929  dvdsval2  13991  dvdscmul  14012  dvdsmulc  14013  dvdscmulr  14014  dvdsmulcr  14015  mulmoddvds  14046  divalglem8  14060  ndvdssub  14067  rpmulgcd  14195  isprm3  14228  coprmdvds  14245  modprm0  14332  coprimeprodsq  14335  pythagtriplem12  14352  pythagtriplem14  14354  pcprendvds  14366  pcmul  14377  pcdiv  14378  pcqcl  14382  pcqdiv  14383  pcdvdsb  14394  pcgcd  14403  vdwnnlem1  14515  hashbcss  14524  cshwshashlem1  14582  fvsetsid  14661  mrcss  15023  mrcsscl  15027  mrcun  15029  cofulid  15296  catcisolem  15502  funcsetcestrclem9  15549  latleeqj1  15810  lubun  15870  clatleglb  15873  pslem  15953  dirtr  15983  mgmb1mgm1  16000  pwspjmhm  16116  gsumccat  16126  grpinvid1  16215  grpinvid2  16216  grpinvadd  16233  grpsubf  16234  grpsubrcan  16236  grpinvsub  16237  grpsubeq0  16241  grpsubadd0sub  16242  grppncan  16246  grpnpcan  16247  mulgnn0p1  16270  subgsubcl  16329  subgsub  16330  eqglact  16369  qussub  16378  ghmsub  16392  psgnunilem4  16639  oddvds2  16705  odsubdvds  16708  gexnnod  16725  slwn0  16752  gsumdixpOLD  17370  gsumdixp  17371  dvrcl  17448  unitdvcl  17449  dvrcan1  17453  dvrcan3  17454  dvreq1  17455  subrgdv  17559  abvsubtri  17597  idsrngd  17624  lmodvsubval2  17678  lsmcl  17842  lsmsp2  17846  lspsntrim  17857  lidldvgen  18016  evlslem4OLD  18286  evlslem4  18287  mpfsubrg  18314  ply1tmcl  18426  eqcoe1ply1eq  18452  gsummoncoe1  18459  lply1binomsc  18462  chrcong  18659  zndvds  18679  zntoslem  18686  ocvsscon  18797  obselocv  18850  frlmphl  18901  mamudm  18975  mamufacex  18976  scmatf1  19118  scmatf1o  19119  scmatrngiso  19123  submabas  19165  mdetdiaglem  19185  mdetralt2  19196  mdetero  19197  mdetunilem2  19200  mdetunilem6  19204  m2detleiblem7  19214  maducoeval2  19227  gsummatr01lem3  19244  gsummatr01  19246  smadiadetglem2  19259  cramerlem1  19274  mply1topmatcl  19391  mp2pm2mplem4  19395  istps3OLD  19508  ntrin  19647  elnei  19698  neindisj2  19710  ordtopn3  19783  ordtcld3  19786  leordtval2  19799  lecldbas  19806  cnrest2  19873  cmpsublem  19985  ptrescn  20225  xkococn  20246  kqfeq  20310  snfbas  20452  neifil  20466  fclsrest  20610  utopsnnei  20837  neipcfilu  20884  psmetsym  20899  psmetge0  20901  xmetge0  20932  xmetsym  20935  metusttoOLD  21145  metustto  21146  metustblOLD  21168  metustbl  21169  restmetu  21175  nm2dif  21229  nmtri  21230  cnmet  21364  cnmpt2pc  21513  iihalf1  21516  iihalf2  21518  iocopnst  21525  cphsqrtcl3  21719  cph2ass  21744  caublcls  21832  bcthlem3  21850  bcthlem4  21851  srabn  21885  rrxmet  21920  iblconst  22309  tdeglem3  22542  mdegmullem  22563  dvdsq1p  22646  coeid3  22722  aannenlem2  22810  pserdvlem2  22908  tanord1  23009  cxpef  23133  recxpcl  23143  logbchbase  23229  relogbcl  23231  relogbzcl  23232  logbleb  23241  logblt  23242  relogbcxpb  23245  lawcos  23266  pythag  23267  isosctrlem1  23268  isosctrlem2  23269  ax5seglem1  24352  axcontlem2  24389  axcontlem8  24395  fiusgraedgfi  24528  nbgraf1olem3  24564  nb3graprlem2  24573  cusgra3v  24585  cusgrasizeindslem3  24596  cusgrasizeinds  24597  iswlkon  24655  istrlon  24664  2trllemE  24676  usgrnloop  24686  ispthon  24699  isspthon  24706  usgra2adedgwlkonALT  24737  usgrcyclnl2  24762  3v3e3cycl1  24765  constr3lem4  24768  constr3lem5  24769  constr3lem6  24770  constr3trllem2  24772  constr3trllem3  24773  4cycl4dv  24788  wwlkextproplem3  24864  clwwlkgt0  24892  clwwlknndef  24894  clwwlknfi  24899  clwlkisclwwlklem2a4  24905  clwlkisclwwlklem2a  24906  clwwlkel  24914  clwwlkext2edg  24923  clwwisshclwwlem1  24926  clwwnisshclwwn  24930  erclwwlktr  24936  erclwwlkntr  24948  clwlkfclwwlk  24965  clwlkfoclwwlk  24966  usg2wotspth  25005  2spontn0vne  25008  nbhashnn0  25035  nbhashuvtx  25037  usgrauvtxvdbi  25041  rusgra0edg  25076  frgra3v  25123  usg2spot2nb  25186  numclwlk3lem3  25194  extwwlkfablem2  25199  numclwwlkovf2ex  25207  numclwwlkovgelim  25210  numclwwlk4  25231  numclwwlk5lem  25232  numclwwlk5  25233  numclwwlk6  25234  numclwwlk7  25235  isgrpo  25315  grpoinvid1  25349  grpoinvid2  25350  grpoasscan1  25356  grpoasscan2  25357  grpoinvop  25360  grpodivinv  25363  grpoinvdiv  25364  grpodivf  25365  grpopncan  25370  grponpcan  25371  grpopnpcan2  25372  gxid  25392  resgrprn  25399  ablonncan  25413  zerdivemp1  25553  vcnegsubdi2  25585  vcsub4  25586  nvmval  25654  nvmval2  25655  nvmfval  25656  nvmul0or  25664  nvsubadd  25667  nvpncan2  25668  nvaddsub4  25673  nvnncan  25675  nvmeq0  25676  nvdif  25685  nvpi  25686  nvmtri  25691  nvabs  25693  imsmetlem  25713  ipval2lem3  25732  ipval2  25734  4ipval2  25735  ipval3  25736  ipval2lem6  25738  nmooge0  25799  blometi  25835  hvaddsub12  26072  hvsubdistr1  26083  hvsubdistr2  26084  hvaddcan2  26105  hvmulcan  26106  hvmulcan2  26107  hvsubcan  26108  hvsubcan2  26109  his7  26124  his2sub  26126  his2sub2  26127  norm3dif2  26185  shsubcl  26255  hhssnv  26297  shlej2  26396  fh2  26654  cm2j  26655  pjoi0  26752  hodcl  26782  hosubdi  26843  unopf1o  26951  unopadj  26954  adj2  26969  braadd  26980  bramul  26981  lnopaddmuli  27008  lnopsubmuli  27010  homco2  27012  lnfnaddmuli  27080  adjlnop  27121  leopmul  27169  leoptr  27172  pjimai  27211  atcv1  27415  atexch  27416  atcvatlem  27420  fcoinvbr  27594  divnumden2  27762  xdivmul  27774  resvsca  27974  hasheuni  28233  difelsiga  28282  cndprobin  28556  bayesth  28561  sgn3da  28663  ghomf1olem  29223  lediv2aALT  29232  subdivcomb1  29271  fununiq  29365  dfrdg2  29393  wfrlem4  29511  sltres  29589  nobndlem8  29624  ftc1anclem4  30259  areacirc  30278  clsun  30312  neiin  30316  filbcmb  30397  ismtybnd  30469  grpoeqdivid  30509  ghomco  30511  rngonegrmul  30521  zerdivemp1x  30524  rngohomco  30543  rngoisoco  30551  riscer  30557  intidl  30592  isfldidl  30631  mzprename  30847  dvdsrabdioph  30909  pell14qrdivcl  30966  monotoddzz  31044  dvdsabsmod0OLD  31094  jm2.19lem2  31098  jm2.19  31101  dvconstbi  31407  unima  31608  upbdrech  31671  cncfshift  31842  cncfperiod  31847  cncfuni  31855  icccncfext  31856  dvmptfprodlem  31907  dvnprodlem1  31909  itgspltprt  31944  stoweidlem3  31951  stoweidlem10  31958  stoweidlem19  31967  stoweidlem31  31979  stoweidlem34  31982  stoweidlem44  31992  fourierdlem41  32096  fourierdlem42  32097  fourierdlem51  32106  fourierdlem68  32123  fourierdlem89  32144  fourierdlem91  32146  fourierdlem92  32147  fourierdlem94  32149  etransclem24  32207  etransclem34  32217  sigaraf  32236  sigarmf  32237  pfxsuffeqwrdeq  32581  pfxsuff1eqwrdeq  32582  ccatpfx  32584  pfxpfx  32590  pfxccatin12lem1  32598  pfxccatpfx1  32602  pfxccatpfx2  32603  repswpfx  32611  pfxco  32613  subsubelfzo0  32659  xpprsng  33121  nn0sumltlt  33139  invginvrid  33160  ply1sclrmsm  33183  linccl  33215  lincvalpr  33219  lincresunit3lem1  33280  lincresunit3  33282  fdivmpt  33361  nnolog2flm1  33411  dignnld  33424  digexp  33428  dignn0flhalflem1  33436  reccot  33488  rectan  33489  chordthmALT  34080  isosctrlem1ALT  34081  lshpnelb  35122  opnlen0  35326  opcon3b  35334  opcon2b  35335  oplecon3b  35338  opltcon3b  35342  opltcon2b  35344  oldmm1  35355  oldmm4  35358  oldmj1  35359  oldmj4  35362  cvrval2  35412  cvrcon3b  35415  leatb  35430  atcmp  35449  atcvreq0  35452  atlatle  35458  athgt  35593  3dim2  35605  islln2a  35654  lplnnleat  35679  lvolnleat  35720  4atlem10  35743  4atlem11  35746  4atlem12  35749  dalem21  35831  dalem22  35832  dalem23  35833  dalem29  35838  dalem30  35839  dalem31N  35840  dalem32  35841  dalem33  35842  dalem34  35843  dalem35  35844  dalem36  35845  dalem37  35846  dalem40  35849  dalem46  35855  dalem47  35856  dalem51  35860  dalem52  35861  dalem58  35867  dalem59  35868  pmaple  35898  paddclN  35979  pmapjoin  35989  pmapjat1  35990  elpcliN  36030  pclssN  36031  pclun2N  36036  2polcon4bN  36055  paddunN  36064  poldmj1N  36065  pmapj2N  36066  pmapocjN  36067  psubclinN  36085  paddatclN  36086  poml4N  36090  lautco  36234  ldilco  36253  ltrneq2  36285  trljat1  36304  cdlemc1  36329  cdleme10  36392  ltrnco  36858  trlcocnv  36859  trljco  36879  trljco2  36880  cdlemi1  36957  tendocnv  37161  diaord  37187  dibord  37299  dihord3  37397  dihord4  37398  dihmeetlem2N  37439  dihmeetlem4preN  37446  dochdmj1  37530  hdmap10lem  37982  relexpaddss  38223
  Copyright terms: Public domain W3C validator