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

Theorem 3ad2ant3 1019
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 466 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 1014 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  simp3l  1024  simp3r  1025  simp31  1032  simp32  1033  simp33  1034  simp3ll  1067  simp3lr  1068  simp3rl  1069  simp3rr  1070  simp3l1  1101  simp3l2  1102  simp3l3  1103  simp3r1  1104  simp3r2  1105  simp3r3  1106  simp31l  1119  simp31r  1120  simp32l  1121  simp32r  1122  simp33l  1123  simp33r  1124  simp311  1143  simp312  1144  simp313  1145  simp321  1146  simp322  1147  simp323  1148  simp331  1149  simp332  1150  simp333  1151  3anim123i  1181  3jaao  1296  ceqsalt  3136  ceqsralt  3137  vtoclgft  3161  tpssi  4193  prnebg  4208  otthg  4730  poltletr  5400  funprg  5635  funtpg  5636  fntpg  5641  ftpg  6069  fsnunf  6097  fsnunfv  6099  fvpr1g  6104  fvpr2g  6105  fnsuppresOLD  6119  weniso  6236  ovmpt3rab1  6516  epne3  6594  limsuc  6662  oteqimp  6800  el2xptp0  6825  funsssuppss  6923  smoel  7028  smoord  7033  omwordi  7217  oneo  7227  oeord  7234  oewordi  7237  nnmwordi  7281  nnneo  7297  uniinqs  7388  undifixp  7502  enfixsn  7623  domss2  7673  domssex2  7674  unxpdomlem3  7723  dif1enOLD  7748  dif1en  7749  mapfien2  7864  dffi2  7879  unwdomg  8006  ixpiunwdom  8013  en3lplem1  8027  oemapvali  8099  fodomfi2  8437  infcdaabs  8582  infunabs  8583  infdif  8585  ackbij1lem9  8604  ackbij1lem16  8611  coflim  8637  cfsmolem  8646  isfin2-2  8695  fin1a2lem9  8784  hsmexlem2  8803  axcc2lem  8812  axcc3  8814  domtriomlem  8818  axdc3lem4  8829  axcclem  8833  zornn0g  8881  axacndlem4  8984  axacndlem5  8985  axacnd  8986  gchdomtri  9003  fpwwe  9020  tskssel  9131  tskint  9159  tskurn  9163  gruurn  9172  gruixp  9183  grudomon  9191  gruina  9192  adderpqlem  9328  mulerpqlem  9329  addassnq  9332  mulassnq  9333  distrnq  9335  ltsonq  9343  ltanq  9345  ltmnq  9346  reclem3pr  9423  dedekind  9739  addid2  9758  addcan2  9760  divdir  10226  divcan5  10242  ltdiv1  10402  infmrcl  10518  infmrlb  10520  lt2halves  10769  zdivmul  10929  xaddass  11437  xleadd1  11443  xltadd1  11444  xmulasslem3  11474  xmulass  11475  xlemul1  11478  xlemul2  11479  xltmul1  11480  xadddir  11484  elioo5  11578  iccsupr  11613  iccneg  11637  icoshft  11638  icoshftf1o  11639  iccsplit  11649  fzen  11699  elfz1b  11744  fzrevral  11758  fzshftral  11761  elfz0ubfz0  11772  elfz0fzfz0  11773  fz0fzelfz0  11774  fz0fzdiffz0  11777  elfzo  11795  elfzonlteqm1  11855  ltdifltdiv  11929  modabs  11992  modcyc  11994  modaddmulmod  12016  moddi  12017  modsubdir  12018  expdiv  12178  leexp2a  12183  bcval3  12346  hashnnn0genn0  12378  hashgadd  12407  hashunx  12416  hashfun  12455  hashtpg  12483  brfi1indlem  12491  ccatval1  12554  ccatval2  12555  ccatval3  12556  ccatsymb  12559  ccatass  12564  ccats1val2  12588  swrdval2  12604  swrd0len0  12617  swrd0fv  12623  swrdeq  12628  2swrdeqwrdeq  12635  swrdswrdlem  12641  swrdswrd  12642  swrd0swrd  12643  ccats1swrdeq  12651  ccats1swrdeqrex  12661  swrdccatin12lem2  12671  swrdccat3b  12678  swrdccatid  12679  splval  12684  repswswrd  12713  cshwidxmod  12731  cshwidx0mod  12732  cshwleneq  12742  scshwfzeqfzo  12751  ccatco  12758  cshco  12759  swrdco  12760  f1oun2prg  12822  swrds2  12840  elicc4abs  13108  mulcn2  13374  fsumsplitsnun  13526  modfsummods  13563  demoivreALT  13790  rpnnen2lem4  13805  dvdsval2  13843  dvdsexp  13894  mulgcd  14036  mulgcdr  14038  gcddiv  14039  rpmulgcd  14045  rplpwr  14046  prmexpb  14110  rpexp  14113  modprm0  14182  modprmn0modprm0  14184  coprimeprodsq  14185  pythagtriplem1  14192  pythagtriplem3  14194  pythagtriplem10  14196  pythagtriplem6  14197  pythagtriplem11  14201  pythagtriplem12  14202  pythagtriplem13  14203  pythagtriplem15  14205  pythagtriplem17  14207  pythagtriplem19  14209  pcdvdsb  14244  pcfaclem  14269  vdwapun  14344  ramval  14378  0ram2  14391  0ramcl  14393  imasaddvallem  14777  imasvscaval  14786  mreiincl  14844  mremre  14852  mrieqv2d  14887  cofurid  15111  xpcpropd  15328  clatleglb  15606  ress0g  15760  gsumccat  15829  gsumccatsn  15831  mulgdirlem  15963  mulgp1  15965  eqglact  16044  fvcosymgeq  16246  gsmsymgreqlem2  16248  pmtrprfv3  16272  pmtr3ncomlem1  16291  mndodcongi  16360  oddvdsnn0  16361  odngen  16390  gexnnod  16401  lsmlub  16476  lsmass  16481  efgsval2  16544  efgsrel  16545  ghmplusg  16642  odadd1  16644  odadd2  16645  dvrcan1  17121  dvrcan3  17122  irredrmul  17137  srngadd  17286  srngmul  17287  lmhmvsca  17471  reslmhm2  17479  pwssplit3  17487  lbspss  17508  lsmsp  17512  lspsneu  17549  lidldvgen  17682  assa2ass  17739  evlsval  17956  evlsval2  17957  psropprmul  18047  coe1add  18073  coe1addfv  18074  coe1subfv  18075  coe1tm  18082  coe1sclmul  18091  coe1sclmul2  18093  coe1fzgsumdlem  18111  lply1binom  18116  evl1gsumdlem  18160  zrhpsgninv  18385  zrhpsgnevpm  18391  zrhpsgnodpm  18392  psgndiflemB  18400  cssmre  18488  frlmup4  18599  islindf2  18613  lindsind2  18618  f1lindf  18621  lindsss  18623  f1linds  18624  lindsmm  18627  lbslcic  18640  mndvcl  18657  mndvass  18658  mhmvlin  18663  matecl  18691  matvscacell  18702  mamulid  18707  mamurid  18708  mattposm  18725  madetsumid  18727  matepmcl  18728  matepm2cl  18729  mat1dimbas  18738  mavmulsolcl  18817  mulmarep1el  18838  mulmarep1gsum1  18839  mulmarep1gsum2  18840  1marepvsma1  18849  m1detdiag  18863  mdetdiaglem  18864  mdetdiag  18865  mdetunilem7  18884  mdetunilem9  18886  mdetmul  18889  gsummatr01lem3  18923  gsummatr01lem4  18924  gsummatr01  18925  smadiadetglem2  18938  matinv  18943  slesolinv  18946  cramerimplem1  18949  cramerimp  18952  cramerlem1  18953  pmatcoe1fsupp  18966  mat2pmatbas  18991  decpmatmullem  19036  pmatcollpw3lem  19048  chpscmat  19107  iuncld  19309  clsss  19318  ntrcls0  19340  iscldtop  19359  neiss  19373  neips  19377  restcldi  19437  cnpnei  19528  cnconst2  19547  cnpresti  19552  sslm  19563  cnt0  19610  cnt1  19614  cnhaus  19618  cncmp  19655  cmpcld  19665  cnconn  19686  concompss  19697  elptr  19806  upxp  19856  qtoptop2  19932  ordthmeolem  20034  opnfbas  20075  isfil2  20089  fbasweak  20098  snfbas  20099  fgss  20106  fgcl  20111  fbasrn  20117  trnei  20125  cfinfil  20126  csdfil  20127  supfil  20128  filufint  20153  fin1aufil  20165  fmval  20176  fmf  20178  elfm  20180  elfm3  20183  imaelfm  20184  rnelfmlem  20185  rnelfm  20186  flimclslem  20217  flfneii  20225  cnpfcfi  20273  alexsubALT  20283  ptcmplem3  20286  ustref  20453  ustelimasn  20457  utop3cls  20486  ressusp  20500  cfiluexsm  20525  prdsxmetlem  20603  txmetcn  20783  nmmtri  20873  nmrtri  20875  unitnmn0  20909  nminvr  20910  nmotri  20978  nghmplusg  20979  isclmi  21309  fmcfil  21443  srabn  21532  rrxmvallem  21563  itgconst  21957  dvn2bss  22065  deg1mul3  22248  deg1mul3le  22249  deg1tmle  22250  q1peqb  22287  r1pcl  22290  r1pdeglt  22291  r1pid  22292  dvdsq1p  22293  dvdsr1p  22294  ptolemy  22619  sincosq1eq  22635  logmul2  22726  logdiv2  22727  cxplt2  22804  pythag  22874  bcmono  23277  efexple  23281  lgsdirnn0  23339  selberglem3  23457  brbtwn2  23881  axcgrid  23892  ax5seglem1  23904  ax5seglem2  23905  ax5seg  23914  axpasch  23917  axlowdimlem16  23933  axcontlem7  23946  nbgraf1olem1  24114  nbusgrafi  24121  nb3graprlem1  24124  nb3graprlem2  24125  cusgra2v  24135  cusgra3v  24137  wlkcomp  24198  wlkelwrd  24203  2trllemH  24227  2trllemE  24228  constr1trl  24263  constr2spthlem1  24269  2pthlem2  24271  2wlklem1  24272  2pthon  24277  usgra2adedgwlkonALT  24289  constr3lem4  24320  constr3trllem2  24324  constr3trllem5  24327  constr3pthlem2  24329  wlkiswwlk2  24370  2wlkeq  24380  usg2wlkeq  24381  usg2wlkeq2  24382  wwlknred  24396  wwlknext  24397  wwlknredwwlkn  24399  wwlknfi  24411  wlknfi  24412  wlknwwlknvbij  24413  wwlkextproplem3  24416  clwlkcomp  24436  clwwlkgt0  24444  clwwlknprop  24445  clwwlkn0  24447  clwwlkel  24466  clwwlkf  24467  clwwlkf1  24469  clwwlkfo  24470  clwwlkvbij  24474  clwwlkext2edg  24475  clwwisshclwwlem1  24478  clwwisshclww  24480  clwwnisshclwwn  24482  erclwwlkeqlen  24485  erclwwlkref  24486  eleclclwwlknlem2  24491  erclwwlkneqlen  24497  erclwwlknref  24498  erclwwlknsym  24499  erclwwlkntr  24500  hashecclwwlkn1  24507  usghashecclwwlk  24508  hashclwwlkn  24509  clwwlkndivn  24510  clwlkfclwwlk  24517  clwlkfoclwwlk  24518  clwlkf1clwwlklem  24522  clwlkf1clwwlk  24523  el2wlkonot  24542  el2spthonot  24543  el2spthonot0  24544  el2wlkonotot0  24545  vdgrfival  24570  vdgrf  24571  vdgrfif  24572  vdusgra0nedg  24581  hashnbgravd  24585  nbhashnn0  24587  isrgra  24599  rusgranumwwlkl1  24619  rusgra0edg  24628  rusgranumwlks  24629  3vfriswmgralem  24677  3vfriswmgra  24678  usgn0fidegnn0  24703  2spotdisj  24735  usg2spot2nb  24739  extwwlkfablem1  24748  clwwlkextfrlem1  24750  extwwlkfablem2  24752  numclwwlkun  24753  numclwwlkovf2ex  24760  extwwlkfab  24764  numclwlk1lem2foa  24765  numclwlk1lem2f1  24768  numclwlk1lem2fo  24769  numclwwlk1  24772  numclwwlk2lem1  24776  numclwlk2lem2f  24777  numclwlk2lem2f1o  24779  numclwwlk2  24781  numclwwlk3  24783  numclwwlk4  24784  numclwwlk6  24787  numclwwlk7  24788  numclwwlk8  24789  frgrareg  24791  frgraregord013  24792  gxpval  24934  gxnval  24935  gxnn0neg  24938  gxnn0suc  24939  gxneg  24941  gxsuc  24947  gxnn0add  24949  gxadd  24950  gxsub  24951  gxnn0mul  24952  gxmul  24953  gxmodid  24954  gxdi  24971  zerdivemp1  25109  rngoridfz  25110  vcid  25117  vcdi  25118  vcdir  25119  vcass  25120  imsmetlem  25269  0oval  25376  ajval  25450  shlub  26005  hmopco  26615  adjlnop  26678  mdslmd4i  26925  fcoinvbr  27131  divnumden2  27273  ressnm  27298  ress1r  27439  pstmfval  27508  pl1cn  27570  logeq0im1  27647  ind1  27669  ind0  27670  sigaclcuni  27755  sigagenss2  27787  measun  27819  measvuni  27822  dya2iocnrect  27889  ballotlemieq  28092  ballotlemrv1  28096  sgn3da  28117  lgamgulmlem1  28208  erdszelem2  28273  cnpcon  28312  cvmscld  28355  ghomf1olem  28506  prodfrec  28603  ntrivcvgfvn0  28607  iprodefisumlem  28697  binomrisefac  28738  dvdspw  28749  dfon2lem3  28791  dfon2lem7  28795  predeq123  28819  predpo  28838  frrlem4  28964  nofulllem3  29038  btwndiff  29251  brcolinear2  29282  btwnconn1  29325  nnssi3  29495  nndivsub  29496  ftc1anclem4  29668  areacirclem2  29683  areacirclem5  29686  areacirc  29687  nn0prpwlem  29715  hmeoclda  29726  hmeocldb  29727  ivthALT  29728  ssref  29753  fnemeet1  29785  fnejoin1  29787  upixp  29821  filbcmb  29832  cnresima  29861  smprngopr  30050  igenval2  30064  ismrcd1  30232  istopclsd  30234  ismrc  30235  mapfzcons  30250  eldioph2  30297  diophrex  30311  diophren  30349  pellexlem1  30367  pellexlem5  30371  pellqrexplicit  30415  reglogmul  30431  reglogexp  30432  rmxycomplete  30455  congmul  30507  congabseq  30514  acongsym  30516  acongneg2  30517  fzneg  30522  acongeq  30523  jm2.19  30539  jm2.22  30541  jm2.23  30542  jm2.20nn  30543  rmydioph  30560  rmxdiophlem  30561  jm3.1  30566  pwssplit4  30639  mapfien2OLD  30646  hbtlem2  30677  idomrootle  30757  dvconstbi  30839  expgrowth  30840  iooshift  31126  fmul01lt1lem1  31134  climsuselem1  31149  climsuse  31150  mullimc  31158  mullimcf  31165  limcperiod  31170  lptre2pt  31182  cncfshift  31212  cncfperiod  31217  icccncfext  31226  iblspltprt  31291  itgspltprt  31297  stoweidlem3  31303  stoweidlem16  31316  stoweidlem17  31317  stoweidlem26  31326  stoweidlem34  31334  stoweidlem57  31357  fourierdlem41  31448  fourierdlem42  31449  fourierdlem52  31459  fourierdlem54  31461  fourierdlem74  31481  fourierdlem75  31482  fourierdlem80  31487  fourierdlem94  31501  fourierdlem102  31509  fourierdlem114  31521  elpwdifsn  31763  2leaddle2  31789  ssfz12  31799  fsumsplitsndif  31815  fsummmodsndifre  31816  fsummmodsnunz  31817  usgra2pth  31823  usgvincvad  31873  usgvincvadALT  31876  ofaddmndmap  31997  mapprop  31999  nn0sumltlt  32003  gsumpr  32014  domnmsuppn0  32035  scmsuppss  32038  mndpsuppfi  32041  gsumlsscl  32049  ply1ass23l  32055  ply1mulgsumlem1  32059  lincfsuppcl  32087  linccl  32088  lincvalsng  32090  lincvalpr  32092  lincdifsn  32098  ellcoellss  32109  lincext1  32128  lincext2  32129  lincext3  32130  lindslinindimp2lem2  32133  ldepspr  32147  lincresunit3lem1  32153  lincresunit3lem2  32154  islindeps2  32157  chordthmALT  32813  bnj837  32898  bnj517  33022  bnj553  33035  bnj594  33049  bnj967  33082  bnj1097  33116  bnj1110  33117  bnj1118  33119  bnj1128  33125  bnj1125  33127  bnj1145  33128  bnj1136  33132  bnj1173  33137  bnj1189  33144  bnj1204  33147  bnj1279  33153  bnj1321  33162  bnj1413  33170  bj-ceqsalt1  33531  lsmsat  33805  lsmsatcv  33807  lsatcvatlem  33846  islshpcv  33850  l1cvpat  33851  lfli  33858  lshpset2N  33916  cvrnbtwn  34068  meetat2  34094  atcmp  34108  atcvreq0  34111  atlatmstc  34116  cvlcvr1  34136  cvlcvrp  34137  cvlatcvr2  34139  cvr2N  34207  cvratlem  34217  2atjm  34241  athgt  34252  2lplnmN  34355  2llnmj  34356  2lplnmj  34418  dalemswapyzps  34486  dalem23  34492  dalem24  34493  dalem25  34494  dalem27  34495  dalem28  34496  dalem38  34506  dalem39  34507  dalem44  34512  dalem45  34513  dalem51  34519  dalem52  34520  dalem56  34524  pmapglbx  34565  pmapjat1  34649  pmapjat2  34650  paddatclN  34745  osumcllem4N  34755  osumcllem7N  34758  ltrncoval  34941  cdleme0aa  35006  cdleme0b  35008  cdleme8  35046  cdlemesner  35092  cdleme22eALTN  35141  cdleme26eALTN  35157  cdleme35h  35252  cdleme50trn2  35347  cdleme  35356  tgrpov  35544  tendotp  35557  tendoidcl  35565  tendo0co2  35584  cdlemkvcl  35638  dvhopvadd  35890  dvhopellsm  35914  dihmeetlem1N  36087  dihmeetlem9N  36112  dihatexv  36135  lcfl7lem  36296  mapdrvallem2  36442  mapdh9a  36587  hdmapevec  36635
  Copyright terms: Public domain W3C validator