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  2337  vtoclegft  3153  eqeu  3241  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  7050  smoiso  7092  oaord  7259  oaword  7261  omcan  7281  omwordri  7284  odi  7291  omeulem1  7294  oeord  7300  oecan  7301  oewordri  7304  oeordsuc  7306  nnaord  7331  nnaordr  7332  nndi  7335  nnaword  7339  nnmwordri  7348  erov  7471  ecopovtrn  7477  xpdom3  7679  mapxpen  7747  findcard  7819  indexfi  7891  suppr  7996  infpr  8028  r111  8254  tcrank  8363  acndom  8489  infdif2  8647  infxpdom  8648  cfeq0  8693  cfsuc  8694  cfflb  8696  cflim2  8700  cfsmolem  8707  axcc3  8875  domtriomlem  8879  axdc3lem2  8888  axdc3lem4  8890  axdc4lem  8892  axcclem  8894  pwcfsdom  9015  tsktrss  9193  tsksuc  9194  tskuni  9215  adderpqlem  9386  mulerpqlem  9387  mulcanenq  9392  distrnq  9393  ltsonq  9401  ltanq  9403  ltmnq  9404  distrlem1pr  9457  distrlem5pr  9459  ltsopr  9464  ltsosr  9525  ltasr  9531  adddir  9641  axlttrn  9713  letr  9734  ltneOLD  9738  nnncan1  9917  npncan3  9919  pnpcan2  9921  subdi  10059  subdir  10060  mulcan1g  10272  mulcan2g  10273  divmul  10280  div23  10296  div13  10298  divsubdir  10310  divcan7  10323  ltmul2  10463  lemul1  10464  lemul2  10465  lemul2a  10467  lediv1  10477  ltmuldiv2  10486  lemuldiv  10493  lemuldiv2  10494  ltdiv2  10499  lediv2  10503  fiminre  10562  infrelb  10603  infmrlbOLD  10604  nndivtr  10658  bndndx  10875  nn0n0n1ge2  10939  fnn0ind  11041  xrletr  11462  qsqueeze  11501  xleadd2a  11547  xleadd1  11548  xltadd2  11550  xltmul2  11586  supxrbnd  11621  iooneg  11759  iccneg  11760  icoshft  11761  icoshftf1o  11762  fzen  11823  uzsubsubfz  11828  fzrevral2  11887  fzshftral  11889  fz0fzdiffz0  11906  elfzmlbmOLD  11908  elfzmlbp  11909  elfzo  11929  nelfzo  11932  fzoaddel2  11976  fzosubel2  11980  elfzom1p1elfzo  11999  ssfzo12bi  12012  fzonfzoufzol  12018  flltdivnn0lt  12071  modmulnn  12120  modcyc  12138  modaddabs  12141  modaddmod  12142  modadd2mod  12146  modsubmod  12154  modsubmodmod  12155  modaddmodup  12159  modmulmod  12161  moddi  12163  modsubdir  12164  uzindi  12200  axdc4uzlem  12201  expneg2  12287  expdiv  12329  expubnd  12339  bernneq2  12405  hashinfxadd  12570  brfi1indlem  12653  ccatval3  12728  ccatsymb  12731  ccatfv0  12732  ccatval1lsw  12733  ccats1val2  12762  swrdnd  12790  2swrd1eqwrdeq  12812  swrdswrd  12818  wrd2ind  12836  swrdccatin1  12841  swrdccatin12lem2b  12844  swrdccatin2  12845  swrdccatin12lem2  12847  swrdccatin12lem3  12848  swrdccat  12851  swrdccat3a  12852  swrdccat3blem  12853  repswswrd  12889  repswccat  12890  cshwidxmod  12907  2cshw  12914  3cshw  12919  scshwfzeqfzo  12927  cshwcsh2id  12929  ccatco  12934  cshco  12935  swrdco  12936  lswco  12937  swrds2  13020  2swrd2eqwrdeq  13028  shftuz  13132  shftval2  13138  abs3dif  13394  modfsummods  13852  sin02gt0  14245  dvdsval2  14307  dvdscmul  14328  dvdsmulc  14329  dvdscmulr  14330  dvdsmulcr  14331  mulmoddvds  14362  divalglem8  14379  ndvdssub  14387  rpmulgcd  14522  isprm3  14632  coprmdvds  14658  coprmprod  14677  modprm0  14755  coprimeprodsq  14758  pythagtriplem12  14775  pythagtriplem14  14777  pcprendvds  14789  pcmul  14800  pcdiv  14801  pcqcl  14805  pcqdiv  14806  pcdvdsb  14817  pcgcd  14826  vdwnnlem1  14944  hashbcss  14955  cshwshashlem1  15065  fvsetsid  15147  mrcss  15521  mrcsscl  15525  mrcun  15527  cofulid  15794  catcisolem  16000  funcsetcestrclem9  16047  latleeqj1  16308  lubun  16368  clatleglb  16371  pslem  16451  dirtr  16481  mgmb1mgm1  16498  pwspjmhm  16614  gsumccat  16624  grpinvid1  16713  grpinvid2  16714  grpinvadd  16731  grpsubf  16732  grpsubrcan  16734  grpinvsub  16735  grpsubeq0  16739  grpsubadd0sub  16740  grppncan  16744  grpnpcan  16745  mulgnn0p1  16768  subgsubcl  16827  subgsub  16828  eqglact  16867  qussub  16876  ghmsub  16890  psgnunilem4  17137  oddvds2  17216  odsubdvds  17219  gexnnod  17239  slwn0  17266  gsumdixp  17836  dvrcl  17913  unitdvcl  17914  dvrcan1  17918  dvrcan3  17919  dvreq1  17920  subrgdv  18024  abvsubtri  18062  idsrngd  18089  lmodvsubval2  18142  lsmcl  18305  lsmsp2  18309  lspsntrim  18320  lidldvgen  18478  evlslem4  18730  mpfsubrg  18754  ply1tmcl  18864  eqcoe1ply1eq  18890  gsummoncoe1  18897  lply1binomsc  18900  chrcong  19098  zndvds  19118  zntoslem  19125  ocvsscon  19236  obselocv  19289  frlmphl  19337  mamudm  19411  mamufacex  19412  scmatf1  19554  scmatf1o  19555  scmatrngiso  19559  submabas  19601  mdetdiaglem  19621  mdetralt2  19632  mdetero  19633  mdetunilem2  19636  mdetunilem6  19640  m2detleiblem7  19650  maducoeval2  19663  gsummatr01lem3  19680  gsummatr01  19682  smadiadetglem2  19695  cramerlem1  19710  mply1topmatcl  19827  mp2pm2mplem4  19831  ntrin  20074  elnei  20125  neindisj2  20137  ordtopn3  20210  ordtcld3  20213  leordtval2  20226  lecldbas  20233  cnrest2  20300  cmpsublem  20412  ptrescn  20652  xkococn  20673  kqfeq  20737  snfbas  20879  neifil  20893  fclsrest  21037  utopsnnei  21262  neipcfilu  21309  psmetsym  21324  psmetge0  21326  xmetge0  21357  xmetsym  21360  metustto  21566  metustbl  21579  restmetu  21583  nm2dif  21636  nmtri  21637  cnmet  21790  cnmpt2pc  21954  iihalf1  21957  iihalf2  21959  iocopnst  21966  cphsqrtcl3  22163  cph2ass  22188  caublcls  22276  bcthlem3  22292  bcthlem4  22293  srabn  22325  rrxmet  22360  iblconst  22773  tdeglem3  23006  mdegmullem  23025  dvdsq1p  23109  coeid3  23192  aannenlem2  23283  pserdvlem2  23381  tanord1  23484  cxpef  23608  recxpcl  23618  logbchbase  23706  relogbcl  23708  relogbzcl  23709  logbleb  23718  logblt  23719  relogbcxpb  23722  lawcos  23743  pythag  23744  isosctrlem1  23745  isosctrlem2  23746  ax5seglem1  24956  axcontlem2  24993  axcontlem8  24999  fiusgraedgfi  25133  nbgraf1olem3  25169  nb3graprlem2  25178  cusgra3v  25190  cusgrasizeindslem3  25201  cusgrasizeinds  25202  iswlkon  25260  istrlon  25269  2trllemE  25281  usgrwlknloop  25291  ispthon  25304  isspthon  25311  usgra2adedgwlkonALT  25342  usgrcyclnl2  25367  3v3e3cycl1  25370  constr3lem4  25373  constr3lem5  25374  constr3lem6  25375  constr3trllem2  25377  constr3trllem3  25378  4cycl4dv  25393  wwlkextproplem3  25469  clwwlkgt0  25497  clwwlknndef  25499  clwwlknfi  25504  clwlkisclwwlklem2a4  25510  clwlkisclwwlklem2a  25511  clwwlkel  25519  clwwlkext2edg  25528  clwwisshclwwlem1  25531  clwwnisshclwwn  25535  erclwwlktr  25541  erclwwlkntr  25553  clwlkfclwwlk  25570  clwlkfoclwwlk  25571  usg2wotspth  25610  2spontn0vne  25613  nbhashnn0  25640  nbhashuvtx  25642  usgrauvtxvdbi  25646  rusgra0edg  25681  frgra3v  25728  usg2spot2nb  25791  numclwlk3lem3  25799  extwwlkfablem2  25804  numclwwlkovf2ex  25812  numclwwlkovgelim  25815  numclwwlk4  25836  numclwwlk5lem  25837  numclwwlk5  25838  numclwwlk6  25839  numclwwlk7  25840  isgrpo  25922  grpoinvid1  25956  grpoinvid2  25957  grpoasscan1  25963  grpoasscan2  25964  grpoinvop  25967  grpodivinv  25970  grpoinvdiv  25971  grpodivf  25972  grpopncan  25977  grponpcan  25978  grpopnpcan2  25979  gxid  25999  resgrprn  26006  ablonncan  26020  zerdivemp1  26160  vcnegsubdi2  26192  vcsub4  26193  nvmval  26261  nvmval2  26262  nvmfval  26263  nvmul0or  26271  nvsubadd  26274  nvpncan2  26275  nvaddsub4  26280  nvnncan  26282  nvmeq0  26283  nvdif  26292  nvpi  26293  nvmtri  26298  nvabs  26300  imsmetlem  26320  ipval2lem3  26339  ipval2  26341  4ipval2  26342  ipval3  26343  ipval2lem6  26345  nmooge0  26406  blometi  26442  hvaddsub12  26689  hvsubdistr1  26700  hvsubdistr2  26701  hvaddcan2  26722  hvmulcan  26723  hvmulcan2  26724  hvsubcan  26725  hvsubcan2  26726  his7  26741  his2sub  26743  his2sub2  26744  norm3dif2  26802  shsubcl  26871  hhssnv  26913  shlej2  27012  fh2  27270  cm2j  27271  pjoi0  27368  hodcl  27398  hosubdi  27459  unopf1o  27567  unopadj  27570  adj2  27585  braadd  27596  bramul  27597  lnopaddmuli  27624  lnopsubmuli  27626  homco2  27628  lnfnaddmuli  27696  adjlnop  27737  leopmul  27785  leoptr  27788  pjimai  27827  atcv1  28031  atexch  28032  atcvatlem  28036  fcoinvbr  28217  divnumden2  28388  xdivmul  28401  resvsca  28601  hasheuni  28914  difelsiga  28963  cndprobin  29275  bayesth  29280  sgn3da  29420  ghomf1olem  30320  lediv2aALT  30329  subdivcomb1  30367  fununiq  30417  dfrdg2  30449  sltres  30558  nobndlem8  30593  clsun  30989  neiin  30993  rdgeqoa  31737  poimirlem32  31936  ftc1anclem4  31984  areacirc  32001  filbcmb  32031  ismtybnd  32103  grpoeqdivid  32143  ghomco  32145  rngonegrmul  32155  zerdivemp1x  32158  rngohomco  32177  rngoisoco  32185  riscer  32191  intidl  32226  isfldidl  32265  lshpnelb  32519  opnlen0  32723  opcon3b  32731  opcon2b  32732  oplecon3b  32735  opltcon3b  32739  opltcon2b  32741  oldmm1  32752  oldmm4  32755  oldmj1  32756  oldmj4  32759  cvrval2  32809  cvrcon3b  32812  leatb  32827  atcmp  32846  atcvreq0  32849  atlatle  32855  athgt  32990  3dim2  33002  islln2a  33051  lplnnleat  33076  lvolnleat  33117  4atlem10  33140  4atlem11  33143  4atlem12  33146  dalem21  33228  dalem22  33229  dalem23  33230  dalem29  33235  dalem30  33236  dalem31N  33237  dalem32  33238  dalem33  33239  dalem34  33240  dalem35  33241  dalem36  33242  dalem37  33243  dalem40  33246  dalem46  33252  dalem47  33253  dalem51  33257  dalem52  33258  dalem58  33264  dalem59  33265  pmaple  33295  paddclN  33376  pmapjoin  33386  pmapjat1  33387  elpcliN  33427  pclssN  33428  pclun2N  33433  2polcon4bN  33452  paddunN  33461  poldmj1N  33462  pmapj2N  33463  pmapocjN  33464  psubclinN  33482  paddatclN  33483  poml4N  33487  lautco  33631  ldilco  33650  ltrneq2  33682  trljat1  33701  cdlemc1  33726  cdleme10  33789  ltrnco  34255  trlcocnv  34256  trljco  34276  trljco2  34277  cdlemi1  34354  tendocnv  34558  diaord  34584  dibord  34696  dihord3  34794  dihord4  34795  dihmeetlem2N  34836  dihmeetlem4preN  34843  dochdmj1  34927  hdmap10lem  35379  mzprename  35560  dvdsrabdioph  35622  pell14qrdivcl  35681  monotoddzz  35761  dvdsabsmod0OLD  35811  jm2.19lem2  35815  jm2.19  35818  relexpaddss  36280  dvconstbi  36653  chordthmALT  37303  isosctrlem1ALT  37304  unima  37389  wessf1ornlem  37420  disjf1o  37427  disjinfi  37429  ssnnf1octb  37431  projf1o  37435  upbdrech  37477  iuneqfzuzlem  37511  suplesup  37516  cncfshift  37691  cncfperiod  37696  cncfuni  37704  icccncfext  37705  dvmptfprodlem  37759  dvnprodlem1  37761  itgspltprt  37796  stoweidlem3  37803  stoweidlem10  37810  stoweidlem19  37819  stoweidlem31  37832  stoweidlem34  37835  stoweidlem44  37845  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem51  37961  fourierdlem68  37978  fourierdlem89  37999  fourierdlem91  38001  fourierdlem92  38002  fourierdlem94  38004  etransclem24  38063  etransclem34  38073  salincl  38105  saldifcl2  38108  sge0pr  38144  sge0pnffigt  38146  nnfoctbdjlem  38201  nnfoctbdj  38202  meadjiunlem  38211  caratheodorylem2  38256  hoidmv1le  38320  hoidmvlelem3  38323  sigaraf  38333  sigarmf  38334  nltle2tri  38586  iccpartiltu  38606  icceuelpart  38620  bgoldbtbndlem2  38771  pfxsuffeqwrdeq  38817  pfxsuff1eqwrdeq  38818  ccatpfx  38820  pfxpfx  38826  pfxccatin12lem1  38834  pfxccatpfx1  38838  pfxccatpfx2  38839  repswpfx  38847  pfxco  38849  subsubelfzo0  38916  issubgr2  39117  uhgrissubgr  39120  egrsubgr  39122  fusgrfisstep  39161  nbusgrfi  39211  nb3grprlem2  39214  cplgr3v  39258  cusgrsizeindslem  39268  xpprsng  39734  nn0sumltlt  39752  invginvrid  39773  ply1sclrmsm  39796  linccl  39828  lincvalpr  39832  lincresunit3lem1  39893  lincresunit3  39895  fdivmpt  39972  nnolog2flm1  40022  dignnld  40035  digexp  40039  dignn0flhalflem1  40047  reccot  40099  rectan  40100
  Copyright terms: Public domain W3C validator