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  3110  ceqsralt  3111  vtoclgft  3135  euelss  3766  tpssi  4169  prnebg  4185  otthg  4705  poltletr  5252  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  7087  smoord  7092  omwordi  7280  oneo  7290  oeord  7297  oewordi  7300  nnmwordi  7344  nnneo  7360  uniinqs  7451  undifixp  7566  enfixsn  7687  domss2  7737  domssex2  7738  unxpdomlem3  7784  dif1en  7810  mapfien2  7928  dffi2  7943  unwdomg  8099  ixpiunwdom  8106  en3lplem1  8119  oemapvali  8188  fodomfi2  8489  infcdaabs  8634  infunabs  8635  infdif  8637  ackbij1lem9  8656  ackbij1lem16  8663  coflim  8689  cfsmolem  8698  isfin2-2  8747  fin1a2lem9  8836  hsmexlem2  8855  axcc2lem  8864  axcc3  8866  domtriomlem  8870  axdc3lem4  8881  axcclem  8885  zornn0g  8933  axacndlem4  9034  axacndlem5  9035  axacnd  9036  gchdomtri  9053  fpwwe  9070  tskssel  9181  tskint  9209  tskurn  9213  gruurn  9222  gruixp  9233  grudomon  9241  gruina  9242  adderpqlem  9378  mulerpqlem  9379  addassnq  9382  mulassnq  9383  distrnq  9385  ltsonq  9393  ltanq  9395  ltmnq  9396  reclem3pr  9473  dedekind  9796  addid2  9815  addcan2  9817  divdir  10292  divcan5  10308  ltdiv1  10468  infmrclOLD  10593  infrelb  10596  infmrlbOLD  10597  lt2halves  10847  zdivmul  11008  xaddass  11535  xleadd1  11541  xltadd1  11542  xmulasslem3  11572  xmulass  11573  xlemul1  11576  xlemul2  11577  xltmul1  11578  xadddir  11582  elioo5  11692  iccsupr  11727  iccneg  11751  icoshft  11752  icoshftf1o  11753  iccsplit  11763  fzen  11814  elfz1b  11862  fzrevral  11877  fzshftral  11880  elfz0ubfz0  11892  elfz0fzfz0  11893  fz0fzelfz0  11894  fz0fzdiffz0  11897  elfzo  11920  elfzonlteqm1  11986  ltdifltdiv  12063  modabs  12127  modcyc  12129  modaddmulmod  12153  moddi  12154  modsubdir  12155  expdiv  12320  leexp2a  12325  bcval3  12488  hashnnn0genn0  12523  hashgadd  12553  hashunx  12562  hashfun  12604  hashtpg  12632  brfi1indlem  12640  ccatval1  12709  ccatval2  12710  ccatval3  12711  ccatsymb  12714  ccatass  12719  ccats1val2  12745  swrdval2  12761  swrd0len0  12777  swrd0fv  12780  swrdeq  12785  swrdspsleq  12790  2swrdeqwrdeq  12794  swrdswrdlem  12800  swrdswrd  12801  swrd0swrd  12802  ccats1swrdeq  12810  ccats1swrdeqrex  12820  swrdccatin12lem2  12830  swrdccat3b  12837  swrdccatid  12838  splval  12843  repswswrd  12872  cshwidxmod  12890  cshwidx0mod  12891  cshwleneq  12901  scshwfzeqfzo  12910  ccatco  12917  cshco  12918  swrdco  12919  f1oun2prg  12981  swrds2  12999  trclfvss  13049  elicc4abs  13361  mulcn2  13637  fsumsplitsnun  13794  modfsummods  13831  prodfrec  13929  ntrivcvgfvn0  13933  binomrisefac  14073  demoivreALT  14233  rpnnen2lem4  14248  dvdsval2  14286  dvdsexp  14339  mulgcd  14485  mulgcdr  14487  gcddiv  14488  rpmulgcd  14494  rplpwr  14495  lcmfn0val  14558  lcmftp  14571  lcmfunsnlem2lem1  14573  lcmfunsnlem2lem2  14574  lcmfunsnlem2  14575  prmexpb  14632  rpexp  14634  modprm0  14710  modprmn0modprm0  14712  coprimeprodsq  14713  pythagtriplem1  14720  pythagtriplem3  14722  pythagtriplem10  14724  pythagtriplem6  14725  pythagtriplem11  14729  pythagtriplem12  14730  pythagtriplem13  14731  pythagtriplem15  14733  pythagtriplem17  14735  pythagtriplem19  14737  pcdvdsb  14772  pcfaclem  14797  vdwapun  14878  ramval  14914  ramvalOLD  14915  0ram2  14933  0ramcl  14935  fvprmselgcd1  14957  prmgaplem6  14980  imasaddvallem  15377  imasvscaval  15386  mreiincl  15444  mremre  15452  mrieqv2d  15487  cofurid  15738  initoeu2lem0  15850  initoeu2lem2  15852  funcestrcsetclem6  15972  funcestrcsetclem9  15975  funcsetcestrclem6  15987  funcsetcestrclem9  15990  xpcpropd  16035  clatleglb  16314  ress0g  16507  gsumccat  16567  gsumccatsn  16569  sgrp2nmndlem3  16601  sgrp2nmndlem5  16605  mulgdirlem  16724  mulgp1  16726  eqglact  16810  fvcosymgeq  17012  gsmsymgreqlem2  17014  pmtrprfv3  17037  pmtr3ncomlem1  17056  mndodcongi  17125  oddvdsnn0  17126  odngen  17155  gexnnod  17166  lsmlub  17241  lsmass  17246  efgsval2  17309  efgsrel  17310  ghmplusg  17410  odadd1  17412  odadd2  17413  srg1zr  17688  dvrcan1  17845  dvrcan3  17846  irredrmul  17861  srngadd  18011  srngmul  18012  lmhmvsca  18194  reslmhm2  18202  pwssplit3  18210  lbspss  18231  lsmsp  18235  lspsneu  18272  lidldvgen  18405  assa2ass  18472  evlsval  18668  evlsval2  18669  psropprmul  18757  coe1add  18783  coe1addfv  18784  coe1subfv  18785  coe1tm  18792  coe1sclmul  18801  coe1sclmul2  18803  coe1fzgsumdlem  18821  lply1binom  18826  evl1gsumdlem  18870  zrhpsgninv  19075  zrhpsgnevpm  19081  zrhpsgnodpm  19082  psgndiflemB  19090  cssmre  19178  frlmup4  19281  islindf2  19294  lindsind2  19299  f1lindf  19302  lindsss  19304  f1linds  19305  lindsmm  19308  lbslcic  19321  mndvcl  19338  mndvass  19339  mhmvlin  19344  matecl  19372  matvscacell  19383  mamulid  19388  mamurid  19389  mattposm  19406  madetsumid  19408  matepmcl  19409  matepm2cl  19410  mat1dimbas  19419  mavmulsolcl  19498  mulmarep1el  19519  mulmarep1gsum1  19520  mulmarep1gsum2  19521  1marepvsma1  19530  m1detdiag  19544  mdetdiaglem  19545  mdetdiag  19546  mdetunilem7  19565  mdetunilem9  19567  mdetmul  19570  gsummatr01lem3  19604  gsummatr01lem4  19605  gsummatr01  19606  smadiadetglem2  19619  matinv  19624  slesolinv  19627  cramerimplem1  19630  cramerimp  19633  cramerlem1  19634  pmatcoe1fsupp  19647  mat2pmatbas  19672  decpmatmullem  19717  pmatcollpw3lem  19729  chpscmat  19788  iuncld  19982  clsss  19991  ntrcls0  20014  iscldtop  20033  neiss  20047  neips  20051  restcldi  20111  cnpnei  20202  cnconst2  20221  cnpresti  20226  sslm  20237  cnt0  20284  cnt1  20288  cnhaus  20292  cncmp  20329  cmpcld  20339  cnconn  20359  concompss  20370  ssref  20449  elptr  20510  upxp  20560  qtoptop2  20636  ordthmeolem  20738  opnfbas  20779  isfil2  20793  fbasweak  20802  snfbas  20803  fgss  20810  fgcl  20815  fbasrn  20821  trnei  20829  cfinfil  20830  csdfil  20831  supfil  20832  filufint  20857  fin1aufil  20869  fmval  20880  fmf  20882  elfm  20884  elfm3  20887  imaelfm  20888  rnelfmlem  20889  rnelfm  20890  flimclslem  20921  flfneii  20929  cnpfcfi  20977  alexsubALT  20988  ptcmplem3  20991  ustref  21155  ustelimasn  21159  utop3cls  21188  ressusp  21202  cfiluexsm  21227  prdsxmetlem  21305  txmetcn  21485  nmmtri  21557  nmrtri  21559  unitnmn0  21593  nminvr  21594  nmotri  21662  nghmplusg  21663  isclmi  21992  fmcfil  22126  srabn  22211  rrxmvallem  22242  itgconst  22644  dvn2bss  22752  deg1mul3  22932  deg1mul3le  22933  deg1tmle  22934  q1peqb  22971  r1pcl  22974  r1pdeglt  22975  r1pid  22976  dvdsq1p  22977  dvdsr1p  22978  ptolemy  23307  sincosq1eq  23323  logeq0im1  23383  logmul2  23421  logdiv2  23422  cxplt2  23499  logbchbase  23564  relogbreexp  23568  relogbexp  23573  pythag  23602  lgamgulmlem1  23810  bcmono  24059  efexple  24063  lgsdirnn0  24121  selberglem3  24239  brbtwn2  24772  axcgrid  24783  ax5seglem1  24795  ax5seglem2  24796  ax5seg  24805  axpasch  24808  axlowdimlem16  24824  axcontlem7  24837  nbgraf1olem1  25005  nbusgrafi  25012  nb3graprlem1  25015  nb3graprlem2  25016  cusgra2v  25026  cusgra3v  25028  wlkcomp  25089  wlkelwrd  25094  2trllemH  25118  2trllemE  25119  constr1trl  25154  constr2spthlem1  25160  2pthlem2  25162  2wlklem1  25163  2pthon  25168  usgra2adedgwlkonALT  25180  constr3lem4  25211  constr3trllem2  25215  constr3trllem5  25218  constr3pthlem2  25220  wlkiswwlk2  25261  2wlkeq  25271  usg2wlkeq  25272  usg2wlkeq2  25273  wwlknred  25287  wwlknext  25288  wwlknredwwlkn  25290  wwlknfi  25302  wlknfi  25303  wlknwwlknvbij  25304  wwlkextproplem3  25307  clwlkcomp  25327  clwwlkgt0  25335  clwwlknprop  25336  clwwlkn0  25338  clwwlkel  25357  clwwlkf  25358  clwwlkf1  25360  clwwlkfo  25361  clwwlkvbij  25365  clwwlkext2edg  25366  clwwisshclwwlem1  25369  clwwisshclww  25371  clwwnisshclwwn  25373  erclwwlkeqlen  25376  erclwwlkref  25377  eleclclwwlknlem2  25382  erclwwlkneqlen  25388  erclwwlknref  25389  erclwwlknsym  25390  erclwwlkntr  25391  hashecclwwlkn1  25398  usghashecclwwlk  25399  hashclwwlkn  25400  clwwlkndivn  25401  clwlkfclwwlk  25408  clwlkfoclwwlk  25409  clwlkf1clwwlklem  25413  clwlkf1clwwlk  25414  el2wlkonot  25433  el2spthonot  25434  el2spthonot0  25435  el2wlkonotot0  25436  vdgrfival  25461  vdgrf  25462  vdgrfif  25463  vdusgra0nedg  25472  hashnbgravd  25476  nbhashnn0  25478  isrgra  25490  rusgranumwwlkl1  25510  rusgra0edg  25519  rusgranumwlks  25520  3vfriswmgralem  25568  3vfriswmgra  25569  usgn0fidegnn0  25593  2spotdisj  25625  usg2spot2nb  25629  extwwlkfablem1  25638  clwwlkextfrlem1  25640  extwwlkfablem2  25642  numclwwlkun  25643  numclwwlkovf2ex  25650  extwwlkfab  25654  numclwlk1lem2foa  25655  numclwlk1lem2f1  25658  numclwlk1lem2fo  25659  numclwwlk1  25662  numclwwlk2lem1  25666  numclwlk2lem2f  25667  numclwlk2lem2f1o  25669  numclwwlk2  25671  numclwwlk3  25673  numclwwlk4  25674  numclwwlk6  25677  numclwwlk7  25678  numclwwlk8  25679  frgrareg  25681  frgraregord013  25682  gxpval  25823  gxnval  25824  gxnn0neg  25827  gxnn0suc  25828  gxneg  25830  gxsuc  25836  gxnn0add  25838  gxadd  25839  gxsub  25840  gxnn0mul  25841  gxmul  25842  gxmodid  25843  gxdi  25860  zerdivemp1  25998  rngoridfz  25999  vcid  26006  vcdi  26007  vcdir  26008  vcass  26009  imsmetlem  26158  0oval  26265  ajval  26339  shlub  26893  hmopco  27502  adjlnop  27565  mdslmd4i  27812  fcoinvbr  28045  fresf1o  28062  divnumden2  28210  ressnm  28241  ress1r  28382  smatfval  28451  pstmfval  28529  pl1cn  28591  ind1  28670  ind0  28671  sigaclcuni  28770  sigagenss2  28802  measun  28863  measvuni  28866  dya2iocnrect  28933  omsmeas  28975  ballotlemieq  29166  ballotlemrv1  29170  sgn3da  29191  bnj837  29351  bnj517  29475  bnj553  29488  bnj594  29502  bnj967  29535  bnj1097  29569  bnj1110  29570  bnj1118  29572  bnj1128  29578  bnj1125  29580  bnj1145  29581  bnj1136  29585  bnj1173  29590  bnj1189  29597  bnj1204  29600  bnj1279  29606  bnj1321  29615  bnj1413  29623  erdszelem2  29694  cnpcon  29732  cvmscld  29775  mrsubcv  29927  mrsubvr  29928  ghomf1olem  30091  iprodefisumlem  30154  dvdspw  30164  dfon2lem3  30209  dfon2lem7  30213  frrlem4  30295  nofulllem3  30369  btwndiff  30570  brcolinear2  30601  btwnconn1  30644  nn0prpwlem  30754  hmeoclda  30765  hmeocldb  30766  ivthALT  30767  fnemeet1  30798  fnejoin1  30800  nnssi3  30892  nndivsub  30893  bj-ceqsalt1  31225  ftc1anclem4  31714  areacirclem2  31727  areacirclem5  31730  areacirc  31731  upixp  31750  filbcmb  31761  cnresima  31790  smprngopr  31979  igenval2  31993  lsmsat  32273  lsmsatcv  32275  lsatcvatlem  32314  islshpcv  32318  l1cvpat  32319  lfli  32326  lshpset2N  32384  cvrnbtwn  32536  meetat2  32562  atcmp  32576  atcvreq0  32579  atlatmstc  32584  cvlcvr1  32604  cvlcvrp  32605  cvlatcvr2  32607  cvr2N  32675  cvratlem  32685  2atjm  32709  athgt  32720  2lplnmN  32823  2llnmj  32824  2lplnmj  32886  dalemswapyzps  32954  dalem23  32960  dalem24  32961  dalem25  32962  dalem27  32963  dalem28  32964  dalem38  32974  dalem39  32975  dalem44  32980  dalem45  32981  dalem51  32987  dalem52  32988  dalem56  32992  pmapglbx  33033  pmapjat1  33117  pmapjat2  33118  paddatclN  33213  osumcllem4N  33223  osumcllem7N  33226  ltrncoval  33409  cdleme0aa  33475  cdleme0b  33477  cdleme8  33515  cdlemesner  33561  cdleme22eALTN  33611  cdleme26eALTN  33627  cdleme35h  33722  cdleme50trn2  33817  cdleme  33826  tgrpov  34014  tendotp  34027  tendoidcl  34035  tendo0co2  34054  cdlemkvcl  34108  dvhopvadd  34360  dvhopellsm  34384  dihmeetlem1N  34557  dihmeetlem9N  34582  dihatexv  34605  lcfl7lem  34766  mapdrvallem2  34912  mapdh9a  35057  hdmapevec  35105  ismrcd1  35239  istopclsd  35241  ismrc  35242  mapfzcons  35257  eldioph2  35303  diophrex  35317  diophren  35355  pellexlem1  35373  pellexlem5  35377  pellqrexplicit  35421  reglogmul  35437  reglogexp  35438  rmxycomplete  35461  congmul  35513  congabseq  35520  acongsym  35522  acongneg2  35523  fzneg  35528  acongeq  35529  jm2.19  35544  jm2.22  35546  jm2.23  35547  jm2.20nn  35548  rmydioph  35565  rmxdiophlem  35566  jm3.1  35571  pwssplit4  35643  hbtlem2  35679  idomrootle  35758  pwinfi2  35855  relexpaddss  35939  trclimalb2  35947  brtrclfv2  35948  trclfvdecomr  35949  dvconstbi  36310  expgrowth  36311  chordthmALT  36960  wessf1ornlem  37072  disjf1o  37079  fmul01lt1lem1  37224  climsuselem1  37248  climsuse  37249  limcperiod  37270  lptre2pt  37282  cncfshift  37313  cncfperiod  37318  icccncfext  37327  dvnmptconst  37375  dvnprodlem1  37380  dvnprodlem2  37381  iblspltprt  37409  itgspltprt  37415  stoweidlem3  37422  stoweidlem16  37435  stoweidlem17  37436  stoweidlem26  37445  stoweidlem34  37454  stoweidlem57  37477  fourierdlem41  37569  fourierdlem42  37570  fourierdlem52  37580  fourierdlem54  37582  fourierdlem74  37602  fourierdlem75  37603  fourierdlem80  37608  fourierdlem94  37622  fourierdlem102  37630  fourierdlem114  37642  etransclem18  37674  etransclem29  37685  etransclem46  37702  sge0f1o  37748  meadjiunlem  37802  carageniuncllem1  37841  caratheodorylem1  37846  caratheodory  37848  iccpartiltu  38116  icceuelpart  38130  oexpnegnz  38187  gbepos  38239  gbegt5  38242  gboage9  38245  bgoldbwt  38258  nnsum3primesgbe  38267  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  bgoldbtbndlem1  38280  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  tgblthelfgott  38288  pfxnd  38316  pfxlen0  38317  pfxfv  38320  pfxeq  38325  pfxsuffeqwrdeq  38327  pfxpfx  38336  ccats1pfxeq  38342  ccats1pfxeqrex  38343  pfxccatin12lem2  38345  pfxccatpfx1  38348  pfxccatid  38351  repswpfx  38357  elpwdifsn  38363  2leaddle2  38383  ssfz12  38393  fsumsplitsndif  38406  fsummmodsndifre  38407  fsummmodsnunz  38408  usgra2pth  38414  usgvincvad  38464  usgvincvadALT  38467  rngdir  38630  c0snmhm  38663  rngccatidALTV  38739  funcringcsetcALTV2lem6  38791  funcringcsetcALTV2lem9  38794  ringccatidALTV  38802  funcringcsetclem6ALTV  38814  ofaddmndmap  38875  mapprop  38877  nn0sumltlt  38881  gsumpr  38892  domnmsuppn0  38904  scmsuppss  38907  mndpsuppfi  38910  gsumlsscl  38918  ply1ass23l  38924  ply1mulgsumlem1  38928  lincfsuppcl  38956  linccl  38957  lincvalsng  38959  lincvalpr  38961  lincdifsn  38967  ellcoellss  38978  lincext1  38997  lincext2  38998  lincext3  38999  lindslinindimp2lem2  39002  ldepspr  39016  lincresunit3lem1  39022  lincresunit3lem2  39023  islindeps2  39026  logcxp0  39097  elbigo2r  39115  elbigolo1  39119  fllog2  39130  nnolog2flm1  39152  digvalnn0  39161  nn0digval  39162  dignn0fr  39163  dignn0ldlem  39164  dignnld  39165  digexp  39169  dignn0flhalflem1  39177  dignn0flhalflem2  39178  dignn0ehalf  39179  dignn0flhalf  39180
  Copyright terms: Public domain W3C validator