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

Theorem 3ad2ant3 1028
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant3  |-  ( ( ps  /\  th  /\  ph )  ->  ch )

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantl 467 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 1023 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  simp3l  1033  simp3r  1034  simp31  1041  simp32  1042  simp33  1043  simp3ll  1076  simp3lr  1077  simp3rl  1078  simp3rr  1079  simp3l1  1110  simp3l2  1111  simp3l3  1112  simp3r1  1113  simp3r2  1114  simp3r3  1115  simp31l  1128  simp31r  1129  simp32l  1130  simp32r  1131  simp33l  1132  simp33r  1133  simp311  1152  simp312  1153  simp313  1154  simp321  1155  simp322  1156  simp323  1157  simp331  1158  simp332  1159  simp333  1160  3anim123i  1190  3jaao  1332  ceqsalt  3104  ceqsralt  3105  vtoclgft  3129  euelss  3760  tpssi  4166  prnebg  4182  otthg  4704  poltletr  5251  predeq123  5400  predpo  5417  funprg  5650  funtpg  5651  fntpg  5656  ftpg  6089  fsnunf  6117  fsnunfv  6119  fvpr1g  6124  fvpr2g  6125  weniso  6260  ovmpt3rab1  6539  epne3  6621  limsuc  6690  oteqimp  6826  el2xptp0  6851  funsssuppss  6952  smoel  7090  smoord  7095  omwordi  7283  oneo  7293  oeord  7300  oewordi  7303  nnmwordi  7347  nnneo  7363  uniinqs  7454  undifixp  7569  enfixsn  7690  domss2  7740  domssex2  7741  unxpdomlem3  7787  dif1en  7813  mapfien2  7931  dffi2  7946  unwdomg  8108  ixpiunwdom  8115  en3lplem1  8128  oemapvali  8197  fodomfi2  8498  infcdaabs  8643  infunabs  8644  infdif  8646  ackbij1lem9  8665  ackbij1lem16  8672  coflim  8698  cfsmolem  8707  isfin2-2  8756  fin1a2lem9  8845  hsmexlem2  8864  axcc2lem  8873  axcc3  8875  domtriomlem  8879  axdc3lem4  8890  axcclem  8894  zornn0g  8942  axacndlem4  9042  axacndlem5  9043  axacnd  9044  gchdomtri  9061  fpwwe  9078  tskssel  9189  tskint  9217  tskurn  9221  gruurn  9230  gruixp  9241  grudomon  9249  gruina  9250  adderpqlem  9386  mulerpqlem  9387  addassnq  9390  mulassnq  9391  distrnq  9393  ltsonq  9401  ltanq  9403  ltmnq  9404  reclem3pr  9481  dedekind  9804  addid2  9823  addcan2  9825  divdir  10300  divcan5  10316  ltdiv1  10476  infmrclOLD  10600  infrelb  10603  infmrlbOLD  10604  lt2halves  10854  zdivmul  11015  xaddass  11542  xleadd1  11548  xltadd1  11549  xmulasslem3  11579  xmulass  11580  xlemul1  11583  xlemul2  11584  xltmul1  11585  xadddir  11589  elioo5  11699  iccsupr  11734  iccneg  11760  icoshft  11761  icoshftf1o  11762  iccsplit  11772  fzen  11823  elfz1b  11871  fzrevral  11886  fzshftral  11889  elfz0ubfz0  11901  elfz0fzfz0  11902  fz0fzelfz0  11903  fz0fzdiffz0  11906  elfzo  11929  elfzonlteqm1  11995  ltdifltdiv  12072  modabs  12136  modcyc  12138  modaddmulmod  12162  moddi  12163  modsubdir  12164  expdiv  12329  leexp2a  12334  bcval3  12497  hashnnn0genn0  12532  hashgadd  12562  hashunx  12571  hashfun  12613  hash2prd  12638  hashtpg  12645  brfi1indlem  12653  ccatval1  12726  ccatval2  12727  ccatval3  12728  ccatsymb  12731  ccatass  12736  ccats1val2  12762  swrdval2  12778  swrd0len0  12794  swrd0fv  12797  swrdeq  12802  swrdspsleq  12807  2swrdeqwrdeq  12811  swrdswrdlem  12817  swrdswrd  12818  swrd0swrd  12819  ccats1swrdeq  12827  ccats1swrdeqrex  12837  swrdccatin12lem2  12847  swrdccat3b  12854  swrdccatid  12855  splval  12860  repswswrd  12889  cshwidxmod  12907  cshwidx0mod  12908  cshwleneq  12918  scshwfzeqfzo  12927  ccatco  12934  cshco  12935  swrdco  12936  f1oun2prg  13002  swrds2  13020  trclfvss  13070  elicc4abs  13382  mulcn2  13658  fsumsplitsnun  13815  modfsummods  13852  prodfrec  13950  ntrivcvgfvn0  13954  binomrisefac  14094  demoivreALT  14254  rpnnen2lem4  14269  dvdsval2  14307  dvdsexp  14360  mulgcd  14513  mulgcdr  14515  gcddiv  14516  rpmulgcd  14522  rplpwr  14523  lcmfn0val  14592  lcmfn0valOLD  14595  lcmftp  14608  lcmfunsnlem2lem1  14610  lcmfunsnlem2lem2  14611  lcmfunsnlem2  14612  prmexpb  14669  rpexp  14671  modprm0  14755  modprmn0modprm0  14757  coprimeprodsq  14758  pythagtriplem1  14765  pythagtriplem3  14767  pythagtriplem10  14769  pythagtriplem6  14770  pythagtriplem11  14774  pythagtriplem12  14775  pythagtriplem13  14776  pythagtriplem15  14778  pythagtriplem17  14780  pythagtriplem19  14782  pcdvdsb  14817  pcfaclem  14842  vdwapun  14923  ramval  14959  ramvalOLD  14960  0ram2  14978  0ramcl  14980  fvprmselgcd1  15002  prmgaplem6  15025  imasaddvallem  15434  imasvscaval  15443  mreiincl  15501  mremre  15509  mrieqv2d  15544  cofurid  15795  initoeu2lem0  15907  initoeu2lem2  15909  funcestrcsetclem6  16029  funcestrcsetclem9  16032  funcsetcestrclem6  16044  funcsetcestrclem9  16047  xpcpropd  16092  clatleglb  16371  ress0g  16564  gsumccat  16624  gsumccatsn  16626  sgrp2nmndlem3  16658  sgrp2nmndlem5  16662  mulgdirlem  16781  mulgp1  16783  eqglact  16867  fvcosymgeq  17069  gsmsymgreqlem2  17071  pmtrprfv3  17094  pmtr3ncomlem1  17113  mndodcongi  17191  oddvdsnn0  17192  odngen  17225  gexnnod  17239  lsmlub  17314  lsmass  17319  efgsval2  17382  efgsrel  17383  ghmplusg  17483  odadd1  17485  odadd2  17486  srg1zr  17761  dvrcan1  17918  dvrcan3  17919  irredrmul  17934  srngadd  18084  srngmul  18085  lmhmvsca  18267  reslmhm2  18275  pwssplit3  18283  lbspss  18304  lsmsp  18308  lspsneu  18345  lidldvgen  18478  assa2ass  18545  evlsval  18741  evlsval2  18742  psropprmul  18830  coe1add  18856  coe1addfv  18857  coe1subfv  18858  coe1tm  18865  coe1sclmul  18874  coe1sclmul2  18876  coe1fzgsumdlem  18894  lply1binom  18899  evl1gsumdlem  18943  zrhpsgninv  19151  zrhpsgnevpm  19157  zrhpsgnodpm  19158  psgndiflemB  19166  cssmre  19254  frlmup4  19357  islindf2  19370  lindsind2  19375  f1lindf  19378  lindsss  19380  f1linds  19381  lindsmm  19384  lbslcic  19397  mndvcl  19414  mndvass  19415  mhmvlin  19420  matecl  19448  matvscacell  19459  mamulid  19464  mamurid  19465  mattposm  19482  madetsumid  19484  matepmcl  19485  matepm2cl  19486  mat1dimbas  19495  mavmulsolcl  19574  mulmarep1el  19595  mulmarep1gsum1  19596  mulmarep1gsum2  19597  1marepvsma1  19606  m1detdiag  19620  mdetdiaglem  19621  mdetdiag  19622  mdetunilem7  19641  mdetunilem9  19643  mdetmul  19646  gsummatr01lem3  19680  gsummatr01lem4  19681  gsummatr01  19682  smadiadetglem2  19695  matinv  19700  slesolinv  19703  cramerimplem1  19706  cramerimp  19709  cramerlem1  19710  pmatcoe1fsupp  19723  mat2pmatbas  19748  decpmatmullem  19793  pmatcollpw3lem  19805  chpscmat  19864  iuncld  20058  clsss  20067  ntrcls0  20090  iscldtop  20109  neiss  20123  neips  20127  restcldi  20187  cnpnei  20278  cnconst2  20297  cnpresti  20302  sslm  20313  cnt0  20360  cnt1  20364  cnhaus  20368  cncmp  20405  cmpcld  20415  cnconn  20435  concompss  20446  ssref  20525  elptr  20586  upxp  20636  qtoptop2  20712  ordthmeolem  20814  opnfbas  20855  isfil2  20869  fbasweak  20878  snfbas  20879  fgss  20886  fgcl  20891  fbasrn  20897  trnei  20905  cfinfil  20906  csdfil  20907  supfil  20908  filufint  20933  fin1aufil  20945  fmval  20956  fmf  20958  elfm  20960  elfm3  20963  imaelfm  20964  rnelfmlem  20965  rnelfm  20966  flimclslem  20997  flfneii  21005  cnpfcfi  21053  alexsubALT  21064  ptcmplem3  21067  ustref  21231  ustelimasn  21235  utop3cls  21264  ressusp  21278  cfiluexsm  21303  prdsxmetlem  21381  txmetcn  21561  nmmtri  21633  nmrtri  21635  unitnmn0  21669  nminvr  21670  nmotri  21758  nghmplusg  21759  isclmi  22106  fmcfil  22240  srabn  22325  rrxmvallem  22356  itgconst  22774  dvn2bss  22882  deg1mul3  23062  deg1mul3le  23063  deg1tmle  23064  q1peqb  23103  r1pcl  23106  r1pdeglt  23107  r1pid  23108  dvdsq1p  23109  dvdsr1p  23110  ptolemy  23449  sincosq1eq  23465  logeq0im1  23525  logmul2  23563  logdiv2  23564  cxplt2  23641  logbchbase  23706  relogbreexp  23710  relogbexp  23715  pythag  23744  lgamgulmlem1  23952  bcmono  24203  efexple  24207  lgsdirnn0  24265  selberglem3  24383  brbtwn2  24933  axcgrid  24944  ax5seglem1  24956  ax5seglem2  24957  ax5seg  24966  axpasch  24969  axlowdimlem16  24985  axcontlem7  24998  nbgraf1olem1  25167  nbusgrafi  25174  nb3graprlem1  25177  nb3graprlem2  25178  cusgra2v  25188  cusgra3v  25190  wlkcomp  25251  wlkelwrd  25256  2trllemH  25280  2trllemE  25281  constr1trl  25316  constr2spthlem1  25322  2pthlem2  25324  2wlklem1  25325  2pthon  25330  usgra2adedgwlkonALT  25342  constr3lem4  25373  constr3trllem2  25377  constr3trllem5  25380  constr3pthlem2  25382  wlkiswwlk2  25423  2wlkeq  25433  usg2wlkeq  25434  usg2wlkeq2  25435  wwlknred  25449  wwlknext  25450  wwlknredwwlkn  25452  wwlknfi  25464  wlknfi  25465  wlknwwlknvbij  25466  wwlkextproplem3  25469  clwlkcomp  25489  clwwlkgt0  25497  clwwlknprop  25498  clwwlkn0  25500  clwwlkel  25519  clwwlkf  25520  clwwlkf1  25522  clwwlkfo  25523  clwwlkvbij  25527  clwwlkext2edg  25528  clwwisshclwwlem1  25531  clwwisshclww  25533  clwwnisshclwwn  25535  erclwwlkeqlen  25538  erclwwlkref  25539  eleclclwwlknlem2  25544  erclwwlkneqlen  25550  erclwwlknref  25551  erclwwlknsym  25552  erclwwlkntr  25553  hashecclwwlkn1  25560  usghashecclwwlk  25561  hashclwwlkn  25562  clwwlkndivn  25563  clwlkfclwwlk  25570  clwlkfoclwwlk  25571  clwlkf1clwwlklem  25575  clwlkf1clwwlk  25576  el2wlkonot  25595  el2spthonot  25596  el2spthonot0  25597  el2wlkonotot0  25598  vdgrfival  25623  vdgrf  25624  vdgrfif  25625  vdusgra0nedg  25634  hashnbgravd  25638  nbhashnn0  25640  isrgra  25652  rusgranumwwlkl1  25672  rusgra0edg  25681  rusgranumwlks  25682  3vfriswmgralem  25730  3vfriswmgra  25731  usgn0fidegnn0  25755  2spotdisj  25787  usg2spot2nb  25791  extwwlkfablem1  25800  clwwlkextfrlem1  25802  extwwlkfablem2  25804  numclwwlkun  25805  numclwwlkovf2ex  25812  extwwlkfab  25816  numclwlk1lem2foa  25817  numclwlk1lem2f1  25820  numclwlk1lem2fo  25821  numclwwlk1  25824  numclwwlk2lem1  25828  numclwlk2lem2f  25829  numclwlk2lem2f1o  25831  numclwwlk2  25833  numclwwlk3  25835  numclwwlk4  25836  numclwwlk6  25839  numclwwlk7  25840  numclwwlk8  25841  frgrareg  25843  frgraregord013  25844  gxpval  25985  gxnval  25986  gxnn0neg  25989  gxnn0suc  25990  gxneg  25992  gxsuc  25998  gxnn0add  26000  gxadd  26001  gxsub  26002  gxnn0mul  26003  gxmul  26004  gxmodid  26005  gxdi  26022  zerdivemp1  26160  rngoridfz  26161  vcid  26168  vcdi  26169  vcdir  26170  vcass  26171  imsmetlem  26320  0oval  26427  ajval  26501  shlub  27065  hmopco  27674  adjlnop  27737  mdslmd4i  27984  fcoinvbr  28217  fresf1o  28233  divnumden2  28388  ressnm  28419  ress1r  28560  smatfval  28629  pstmfval  28707  pl1cn  28769  ind1  28848  ind0  28849  sigaclcuni  28948  sigagenss2  28980  measun  29041  measvuni  29044  dya2iocnrect  29111  omsmeas  29163  omsmeasOLD  29164  ballotlemieq  29357  ballotlemrv1  29361  ballotlemieqOLD  29395  ballotlemrv1OLD  29399  sgn3da  29420  bnj837  29580  bnj517  29704  bnj553  29717  bnj594  29731  bnj967  29764  bnj1097  29798  bnj1110  29799  bnj1118  29801  bnj1128  29807  bnj1125  29809  bnj1145  29810  bnj1136  29814  bnj1173  29819  bnj1189  29826  bnj1204  29829  bnj1279  29835  bnj1321  29844  bnj1413  29852  erdszelem2  29923  cnpcon  29961  cvmscld  30004  mrsubcv  30156  mrsubvr  30157  ghomf1olem  30320  iprodefisumlem  30383  dvdspw  30393  dfon2lem3  30438  dfon2lem7  30442  frrlem4  30524  nofulllem3  30598  btwndiff  30799  brcolinear2  30830  btwnconn1  30873  nn0prpwlem  30983  hmeoclda  30994  hmeocldb  30995  ivthALT  30996  fnemeet1  31027  fnejoin1  31029  nnssi3  31121  nndivsub  31122  bj-ceqsalt1  31453  onsucuni3  31734  ftc1anclem4  31984  areacirclem2  31997  areacirclem5  32000  areacirc  32001  upixp  32020  filbcmb  32031  cnresima  32060  smprngopr  32249  igenval2  32263  lsmsat  32543  lsmsatcv  32545  lsatcvatlem  32584  islshpcv  32588  l1cvpat  32589  lfli  32596  lshpset2N  32654  cvrnbtwn  32806  meetat2  32832  atcmp  32846  atcvreq0  32849  atlatmstc  32854  cvlcvr1  32874  cvlcvrp  32875  cvlatcvr2  32877  cvr2N  32945  cvratlem  32955  2atjm  32979  athgt  32990  2lplnmN  33093  2llnmj  33094  2lplnmj  33156  dalemswapyzps  33224  dalem23  33230  dalem24  33231  dalem25  33232  dalem27  33233  dalem28  33234  dalem38  33244  dalem39  33245  dalem44  33250  dalem45  33251  dalem51  33257  dalem52  33258  dalem56  33262  pmapglbx  33303  pmapjat1  33387  pmapjat2  33388  paddatclN  33483  osumcllem4N  33493  osumcllem7N  33496  ltrncoval  33679  cdleme0aa  33745  cdleme0b  33747  cdleme8  33785  cdlemesner  33831  cdleme22eALTN  33881  cdleme26eALTN  33897  cdleme35h  33992  cdleme50trn2  34087  cdleme  34096  tgrpov  34284  tendotp  34297  tendoidcl  34305  tendo0co2  34324  cdlemkvcl  34378  dvhopvadd  34630  dvhopellsm  34654  dihmeetlem1N  34827  dihmeetlem9N  34852  dihatexv  34875  lcfl7lem  35036  mapdrvallem2  35182  mapdh9a  35327  hdmapevec  35375  ismrcd1  35509  istopclsd  35511  ismrc  35512  mapfzcons  35527  eldioph2  35573  diophrex  35587  diophren  35625  pellexlem1  35643  pellexlem5  35647  pellqrexplicit  35693  reglogmul  35711  reglogexp  35712  rmxycomplete  35735  congmul  35787  congabseq  35794  acongsym  35796  acongneg2  35797  fzneg  35802  acongeq  35803  jm2.19  35818  jm2.22  35820  jm2.23  35821  jm2.20nn  35822  rmydioph  35839  rmxdiophlem  35840  jm3.1  35845  pwssplit4  35917  hbtlem2  35953  idomrootle  36039  pwinfi2  36136  relexpaddss  36280  trclimalb2  36288  brtrclfv2  36289  trclfvdecomr  36290  dvconstbi  36653  expgrowth  36654  chordthmALT  37303  wessf1ornlem  37420  disjf1o  37427  fmul01lt1lem1  37602  climsuselem1  37626  climsuse  37627  limcperiod  37648  lptre2pt  37660  cncfshift  37691  cncfperiod  37696  icccncfext  37705  dvnmptconst  37756  dvnprodlem1  37761  dvnprodlem2  37762  iblspltprt  37790  itgspltprt  37796  stoweidlem3  37803  stoweidlem16  37816  stoweidlem17  37817  stoweidlem26  37826  stoweidlem34  37835  stoweidlem57  37858  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem52  37962  fourierdlem54  37964  fourierdlem74  37984  fourierdlem75  37985  fourierdlem80  37990  fourierdlem94  38004  fourierdlem102  38012  fourierdlem114  38024  etransclem18  38057  etransclem29  38068  etransclem46  38085  sge0f1o  38132  sge0xp  38179  meadjiunlem  38211  carageniuncllem1  38250  caratheodorylem1  38255  caratheodory  38257  isomenndlem  38259  hoicvr  38274  ovnsubaddlem2  38297  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  iccpartiltu  38606  icceuelpart  38620  oexpnegnz  38677  gbepos  38729  gbegt5  38732  gboage9  38735  bgoldbwt  38748  nnsum3primesgbe  38757  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  bgoldbtbndlem1  38770  bgoldbtbndlem2  38771  bgoldbtbndlem3  38772  tgblthelfgott  38778  pfxnd  38806  pfxlen0  38807  pfxfv  38810  pfxeq  38815  pfxsuffeqwrdeq  38817  pfxpfx  38826  ccats1pfxeq  38832  ccats1pfxeqrex  38833  pfxccatin12lem2  38835  pfxccatpfx1  38838  pfxccatid  38841  repswpfx  38847  elpwdifsn  38856  ssprsseq  38868  fun2dmnop  38890  2leaddle2  38898  ssfz12  38908  fsumsplitsndif  38922  fsummmodsndifre  38923  fsummmodsnunz  38924  structiedg0val  38954  incistruhgr  39001  ausgrumgri  39049  ausgrusgri  39050  usgredg2vtx  39083  usgredg2vtxeuALT  39085  usgredgedga  39091  usgr1vr  39106  usgr1v0edg  39108  uhgrissubgr  39121  egrsubgr  39123  0uhgrsubgr  39125  dfnbgr3  39175  nbumgrres  39203  nb3grprlem1  39214  cplgr3v  39259  usgra2pth  39288  usgvincvad  39336  usgvincvadALT  39339  rngdir  39502  c0snmhm  39535  rngccatidALTV  39611  funcringcsetcALTV2lem6  39663  funcringcsetcALTV2lem9  39666  ringccatidALTV  39674  funcringcsetclem6ALTV  39686  ofaddmndmap  39747  mapprop  39749  nn0sumltlt  39753  gsumpr  39764  domnmsuppn0  39776  scmsuppss  39779  mndpsuppfi  39782  gsumlsscl  39790  ply1ass23l  39796  ply1mulgsumlem1  39800  lincfsuppcl  39828  linccl  39829  lincvalsng  39831  lincvalpr  39833  lincdifsn  39839  ellcoellss  39850  lincext1  39869  lincext2  39870  lincext3  39871  lindslinindimp2lem2  39874  ldepspr  39888  lincresunit3lem1  39894  lincresunit3lem2  39895  islindeps2  39898  logcxp0  39968  elbigo2r  39986  elbigolo1  39990  fllog2  40001  nnolog2flm1  40023  digvalnn0  40032  nn0digval  40033  dignn0fr  40034  dignn0ldlem  40035  dignnld  40036  digexp  40040  dignn0flhalflem1  40048  dignn0flhalflem2  40049  dignn0ehalf  40050  dignn0flhalf  40051
  Copyright terms: Public domain W3C validator