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

Theorem 3ad2ant3 1004
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 463 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 999 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  simp3l  1009  simp3r  1010  simp31  1017  simp32  1018  simp33  1019  simp3ll  1052  simp3lr  1053  simp3rl  1054  simp3rr  1055  simp3l1  1086  simp3l2  1087  simp3l3  1088  simp3r1  1089  simp3r2  1090  simp3r3  1091  simp31l  1104  simp31r  1105  simp32l  1106  simp32r  1107  simp33l  1108  simp33r  1109  simp311  1128  simp312  1129  simp313  1130  simp321  1131  simp322  1132  simp323  1133  simp331  1134  simp332  1135  simp333  1136  3anim123i  1166  3jaao  1279  ceqsalt  2985  ceqsralt  2986  vtoclgft  3009  tpssi  4027  prnebg  4042  poltletr  5221  funprg  5455  funtpg  5456  fntpg  5461  ftpg  5879  fsnunf  5903  fsnunfv  5905  fvpr1g  5910  fvpr2g  5911  fnsuppresOLD  5925  weniso  6032  epne3  6381  limsuc  6449  funsssuppss  6704  smoel  6807  smoord  6812  omwordi  6998  oneo  7008  oeord  7015  oewordi  7018  nnmwordi  7062  nnneo  7078  uniinqs  7168  undifixp  7287  enfixsn  7408  domss2  7458  domssex2  7459  unxpdomlem3  7507  dif1enOLD  7532  dif1en  7533  mapfien2  7646  dffi2  7661  unwdomg  7787  ixpiunwdom  7794  en3lplem1  7808  oemapvali  7880  fodomfi2  8218  infcdaabs  8363  infunabs  8364  infdif  8366  ackbij1lem9  8385  ackbij1lem16  8392  coflim  8418  cfsmolem  8427  isfin2-2  8476  fin1a2lem9  8565  hsmexlem2  8584  axcc2lem  8593  axcc3  8595  domtriomlem  8599  axdc3lem4  8610  axcclem  8614  zornn0g  8662  axacndlem4  8765  axacndlem5  8766  axacnd  8767  gchdomtri  8784  fpwwe  8801  tskssel  8912  tskint  8940  tskurn  8944  gruurn  8953  gruixp  8964  grudomon  8972  gruina  8973  adderpqlem  9111  mulerpqlem  9112  addassnq  9115  mulassnq  9116  distrnq  9118  ltsonq  9126  ltanq  9128  ltmnq  9129  reclem3pr  9206  dedekind  9521  addid2  9540  addcan2  9542  divdir  10005  divcan5  10021  ltdiv1  10181  infmrcl  10297  infmrlb  10299  lt2halves  10547  zdivmul  10702  xaddass  11200  xleadd1  11206  xltadd1  11207  xmulasslem3  11237  xmulass  11238  xlemul1  11241  xlemul2  11242  xltmul1  11243  xadddir  11247  elioo5  11341  iccsupr  11370  iccneg  11393  icoshft  11394  icoshftf1o  11395  iccsplit  11405  fzen  11454  elfzelfzelfz  11471  elfz0fzfz0  11472  fz0fzelfz0  11473  fz0fzdiffz0  11476  elfz1b  11511  fzrevral  11528  fzshftral  11531  elfzo  11539  ltdifltdiv  11662  modabs  11725  modcyc  11727  modaddmulmod  11749  moddi  11750  modsubdir  11751  expdiv  11898  leexp2a  11903  bcval3  12066  hashnnn0genn0  12098  hashgadd  12124  hashunx  12133  hashtpg  12170  hashfun  12183  brfi1indlem  12202  ccatval1  12260  ccatval2  12261  ccatval3  12262  ccatsymb  12265  ccatass  12270  ccats1val2  12291  swrdval2  12300  swrd0len0  12313  swrd0fv  12319  swrdeq  12324  2swrdeqwrdeq  12331  swrdswrdlem  12337  swrdswrd  12338  swrd0swrd  12339  ccats1swrdeq  12347  swrdccatin12lem2  12364  swrdccat3b  12371  swrdccatid  12372  splval  12377  repswswrd  12406  cshwidxmod  12424  cshwidx0mod  12425  cshwleneq  12435  ccatco  12447  cshco  12448  swrdco  12449  f1oun2prg  12511  swrds2  12529  elicc4abs  12791  mulcn2  13057  demoivreALT  13468  rpnnen2lem4  13483  dvdsval2  13521  dvdsexp  13572  mulgcd  13713  mulgcdr  13715  gcddiv  13716  rpmulgcd  13722  rplpwr  13723  prmexpb  13786  rpexp  13789  modprm0  13856  modprmn0modprm0  13858  coprimeprodsq  13859  pythagtriplem1  13866  pythagtriplem3  13868  pythagtriplem10  13870  pythagtriplem6  13871  pythagtriplem11  13875  pythagtriplem12  13876  pythagtriplem13  13877  pythagtriplem15  13879  pythagtriplem17  13881  pythagtriplem19  13883  pcdvdsb  13918  pcfaclem  13943  vdwapun  14018  ramval  14052  0ram2  14065  0ramcl  14067  imasaddvallem  14450  imasvscaval  14459  mreiincl  14517  mremre  14525  mrieqv2d  14560  cofurid  14784  xpcpropd  15001  clatleglb  15279  ress0g  15433  gsumccat  15499  gsumccatsn  15501  mulgdirlem  15631  mulgp1  15633  eqglact  15712  fvcosymgeq  15914  gsmsymgreqlem2  15916  pmtrprfv3  15940  pmtr3ncomlem1  15959  mndodcongi  16026  oddvdsnn0  16027  odngen  16056  gexnnod  16067  lsmlub  16142  lsmass  16147  efgsval2  16210  efgsrel  16211  ghmplusg  16308  odadd1  16310  odadd2  16311  gsumsn  16425  dvrcan1  16717  dvrcan3  16718  irredrmul  16733  srngadd  16866  srngmul  16867  lmhmvsca  17048  reslmhm2  17056  pwssplit3  17064  lbspss  17085  lsmsp  17089  lspsneu  17126  lidldvgen  17259  psropprmul  17591  coe1add  17616  coe1addfv  17617  coe1subfv  17618  coe1tm  17624  coe1sclmul  17633  coe1sclmul2  17635  zrhpsgninv  17857  zrhpsgnevpm  17863  zrhpsgnodpm  17864  psgndiflemB  17872  cssmre  17960  frlmup4  18071  islindf2  18085  lindsind2  18090  f1lindf  18093  lindsss  18095  f1linds  18096  lindsmm  18099  lbslcic  18112  mndvcl  18133  mndvass  18134  mhmvlin  18139  mamulid  18146  mamurid  18147  matecl  18168  mattposm  18186  madetsumid  18188  matepmcl  18189  matepm2cl  18190  mavmulsolcl  18204  mulmarep1el  18225  mulmarep1gsum1  18226  mulmarep1gsum2  18227  1marepvsma1  18236  mdetunilem7  18266  mdetunilem9  18268  mdetmul  18271  gsummatr01lem3  18305  gsummatr01lem4  18306  gsummatr01  18307  smadiadetglem2  18320  matinv  18325  slesolinv  18328  cramerimplem1  18331  cramerimp  18334  cramerlem1  18335  iuncld  18491  clsss  18500  ntrcls0  18522  iscldtop  18541  neiss  18555  neips  18559  restcldi  18619  cnpnei  18710  cnconst2  18729  cnpresti  18734  sslm  18745  cnt0  18792  cnt1  18796  cnhaus  18800  cncmp  18837  cmpcld  18847  cnconn  18868  concompss  18879  elptr  18988  upxp  19038  qtoptop2  19114  ordthmeolem  19216  opnfbas  19257  isfil2  19271  fbasweak  19280  snfbas  19281  fgss  19288  fgcl  19293  fbasrn  19299  trnei  19307  cfinfil  19308  csdfil  19309  supfil  19310  filufint  19335  fin1aufil  19347  fmval  19358  fmf  19360  elfm  19362  elfm3  19365  imaelfm  19366  rnelfmlem  19367  rnelfm  19368  flimclslem  19399  flfneii  19407  cnpfcfi  19455  alexsubALT  19465  ptcmplem3  19468  ustref  19635  ustelimasn  19639  utop3cls  19668  ressusp  19682  cfiluexsm  19707  prdsxmetlem  19785  txmetcn  19965  nmmtri  20055  nmrtri  20057  unitnmn0  20091  nminvr  20092  nmotri  20160  nghmplusg  20161  isclmi  20491  fmcfil  20625  srabn  20714  rrxmvallem  20745  itgconst  21138  dvn2bss  21246  evlsval  21371  evlsval2  21372  deg1mul3  21472  deg1mul3le  21473  deg1tmle  21474  q1peqb  21511  r1pcl  21514  r1pdeglt  21515  r1pid  21516  dvdsq1p  21517  dvdsr1p  21518  ptolemy  21843  sincosq1eq  21859  logmul2  21950  logdiv2  21951  cxplt2  22028  pythag  22098  bcmono  22501  efexple  22505  lgsdirnn0  22563  selberglem3  22681  brbtwn2  22974  axcgrid  22985  ax5seglem1  22997  ax5seglem2  22998  ax5seg  23007  axpasch  23010  axlowdimlem16  23026  axcontlem7  23039  nbgraf1olem1  23173  nbusgrafi  23180  nb3graprlem1  23182  nb3graprlem2  23183  cusgra2v  23193  cusgra3v  23195  2trllemH  23274  2trllemE  23275  constr1trl  23310  constr2spthlem1  23316  2pthlem2  23318  2wlklem1  23319  2pthon  23324  constr3lem4  23356  constr3trllem2  23360  constr3trllem5  23363  constr3pthlem2  23365  vdgrfival  23390  vdgrf  23391  vdgrfif  23392  vdusgra0nedg  23401  hashnbgravd  23403  gxpval  23569  gxnval  23570  gxnn0neg  23573  gxnn0suc  23574  gxneg  23576  gxsuc  23582  gxnn0add  23584  gxadd  23585  gxsub  23586  gxnn0mul  23587  gxmul  23588  gxmodid  23589  gxdi  23606  zerdivemp1  23744  rngoridfz  23745  vcid  23752  vcdi  23753  vcdir  23754  vcass  23755  imsmetlem  23904  0oval  24011  ajval  24085  shlub  24640  hmopco  25250  adjlnop  25313  mdslmd4i  25560  divnumden2  25910  ressnm  25935  gsumsnf  26096  ress1r  26110  pstmfval  26177  pl1cn  26239  logeq0im1  26307  ind1  26329  ind0  26330  sigaclcuni  26415  sigagenss2  26447  measun  26479  measvuni  26482  dya2iocnrect  26550  ballotlemieq  26747  ballotlemrv1  26751  sgn3da  26772  lgamgulmlem1  26863  erdszelem2  26928  cnpcon  26967  cvmscld  27010  ghomf1olem  27160  prodfrec  27257  ntrivcvgfvn0  27261  iprodefisumlem  27351  binomrisefac  27392  dvdspw  27403  dfon2lem3  27445  dfon2lem7  27449  predeq123  27473  predpo  27492  frrlem4  27618  nofulllem3  27692  btwndiff  27905  brcolinear2  27936  btwnconn1  27979  nnssi3  28150  nndivsub  28151  ftc1anclem4  28314  areacirclem2  28329  areacirclem5  28332  areacirc  28333  nn0prpwlem  28361  hmeoclda  28372  hmeocldb  28373  ivthALT  28374  ssref  28399  fnemeet1  28431  fnejoin1  28433  upixp  28467  filbcmb  28478  cnresima  28507  smprngopr  28696  igenval2  28710  ismrcd1  28879  istopclsd  28881  ismrc  28882  mapfzcons  28897  eldioph2  28945  diophrex  28959  diophren  28997  pellexlem1  29015  pellexlem5  29019  pellqrexplicit  29063  reglogmul  29079  reglogexp  29080  rmxycomplete  29103  congmul  29155  congabseq  29162  acongsym  29164  acongneg2  29165  fzneg  29170  acongeq  29171  jm2.19  29187  jm2.22  29189  jm2.23  29190  jm2.20nn  29191  rmydioph  29208  rmxdiophlem  29209  jm3.1  29214  pwssplit4  29287  mapfien2OLD  29294  hbtlem2  29325  idomrootle  29405  dvconstbi  29453  expgrowth  29454  fmul01lt1lem1  29610  climsuselem1  29626  climsuse  29627  stoweidlem3  29644  stoweidlem16  29657  stoweidlem17  29658  stoweidlem26  29667  stoweidlem34  29675  stoweidlem57  29698  el2xptp0  29973  oteqimp  29975  otthg  29976  ovmpt3rab1  30007  2leaddle2  30021  ssfz12  30043  elfzonlteqm1  30071  fsumsplitsndif  30084  fsummmodsndifre  30085  fsumsplitsnun  30088  fsummmodsnunre  30089  modfsummods  30090  ccats1swrdeqrex  30105  wlkelwrd  30126  wlkcomp  30132  2wlkeq  30134  usg2wlkeq  30135  usgra2pth  30147  wlkiswwlk2  30177  usg2wlkeq2  30187  wwlknred  30201  wwlknext  30202  wwlknredwwlkn  30204  wwlknfi  30216  wlknfi  30217  wlknwwlknvbij  30218  el2wlkonot  30234  el2spthonot  30235  el2spthonot0  30236  el2wlkonotot0  30237  clwlkcomp  30272  clwwlkgt0  30280  clwwlknprop  30281  clwwlkn0  30283  clwwlkel  30301  clwwlkf  30302  clwwlkf1  30304  clwwlkfo  30305  clwwlkvbij  30309  clwwlkext2edg  30310  clwwisshclwwlem1  30315  clwwisshclww  30317  clwwnisshclwwn  30319  erclwwlkeqlen  30328  erclwwlkref  30329  eleclclwwlknlem2  30337  scshwfzeqfzo  30338  erclwwlkneqlen  30344  erclwwlknref  30345  erclwwlknsym  30346  erclwwlkntr  30347  hashecclwwlkn1  30354  usghashecclwwlk  30355  hashclwwlkn  30356  clwwlkndivn  30357  clwlkfclwwlk  30363  clwlkfoclwwlk  30364  clwlkf1clwwlklem  30368  clwlkf1clwwlk  30369  nbhashnn0  30378  isrgra  30389  rusgranumwlkl1lem1  30404  wwlkextproplem3  30408  rusgra0edg  30419  rusgranumwlks  30420  3vfriswmgralem  30442  3vfriswmgra  30443  usgn0fidegnn0  30468  2spotdisj  30500  usg2spot2nb  30504  extwwlkfablem1  30513  clwwlkextfrlem1  30515  extwwlkfablem2  30517  numclwwlkun  30518  numclwwlkovf2ex  30525  extwwlkfab  30529  numclwlk1lem2foa  30530  numclwlk1lem2f1  30533  numclwlk1lem2fo  30534  numclwwlk1  30537  numclwwlk2lem1  30541  numclwlk2lem2f  30542  numclwlk2lem2f1o  30544  numclwwlk2  30546  numclwwlk3  30548  numclwwlk4  30549  numclwwlk6  30552  numclwwlk7  30553  numclwwlk8  30554  frgrareg  30556  frgraregord013  30557  ofaddmndmap  30578  mapprop  30580  gsumpr  30592  domnmsuppn0  30613  scmsuppss  30616  mndpsuppfi  30619  gsumlsscl  30625  matvscacell  30642  lincfsuppcl  30656  linccl  30657  lincvalsng  30659  lincvalpr  30661  lincdifsn  30667  ellcoellss  30678  lincext1  30697  lincext2  30698  lincext3  30699  lindslinindimp2lem2  30702  ldepspr  30716  lincresunit3lem1  30722  lincresunit3lem2  30723  islindeps2  30726  chordthmALT  31371  bnj837  31456  bnj517  31580  bnj553  31593  bnj594  31607  bnj967  31640  bnj1097  31674  bnj1110  31675  bnj1118  31677  bnj1128  31683  bnj1125  31685  bnj1145  31686  bnj1136  31690  bnj1173  31695  bnj1189  31702  bnj1204  31705  bnj1279  31711  bnj1321  31720  bnj1413  31728  bj-ceqsalt  31988  lsmsat  32226  lsmsatcv  32228  lsatcvatlem  32267  islshpcv  32271  l1cvpat  32272  lfli  32279  lshpset2N  32337  cvrnbtwn  32489  meetat2  32515  atcmp  32529  atcvreq0  32532  atlatmstc  32537  cvlcvr1  32557  cvlcvrp  32558  cvlatcvr2  32560  cvr2N  32628  cvratlem  32638  2atjm  32662  athgt  32673  2lplnmN  32776  2llnmj  32777  2lplnmj  32839  dalemswapyzps  32907  dalem23  32913  dalem24  32914  dalem25  32915  dalem27  32916  dalem28  32917  dalem38  32927  dalem39  32928  dalem44  32933  dalem45  32934  dalem51  32940  dalem52  32941  dalem56  32945  pmapglbx  32986  pmapjat1  33070  pmapjat2  33071  paddatclN  33166  osumcllem4N  33176  osumcllem7N  33179  ltrncoval  33362  cdleme0aa  33427  cdleme0b  33429  cdleme8  33467  cdlemesner  33513  cdleme22eALTN  33562  cdleme26eALTN  33578  cdleme35h  33673  cdleme50trn2  33768  cdleme  33777  tgrpov  33965  tendotp  33978  tendoidcl  33986  tendo0co2  34005  cdlemkvcl  34059  dvhopvadd  34311  dvhopellsm  34335  dihmeetlem1N  34508  dihmeetlem9N  34533  dihatexv  34556  lcfl7lem  34717  mapdrvallem2  34863  mapdh9a  35008  hdmapevec  35056
  Copyright terms: Public domain W3C validator