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

Theorem 3ad2ant3 1011
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 1006 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  simp3l  1016  simp3r  1017  simp31  1024  simp32  1025  simp33  1026  simp3ll  1059  simp3lr  1060  simp3rl  1061  simp3rr  1062  simp3l1  1093  simp3l2  1094  simp3l3  1095  simp3r1  1096  simp3r2  1097  simp3r3  1098  simp31l  1111  simp31r  1112  simp32l  1113  simp32r  1114  simp33l  1115  simp33r  1116  simp311  1135  simp312  1136  simp313  1137  simp321  1138  simp322  1139  simp323  1140  simp331  1141  simp332  1142  simp333  1143  3anim123i  1173  3jaao  1287  ceqsalt  3101  ceqsralt  3102  vtoclgft  3126  tpssi  4148  prnebg  4163  poltletr  5342  funprg  5576  funtpg  5577  fntpg  5582  ftpg  6002  fsnunf  6026  fsnunfv  6028  fvpr1g  6033  fvpr2g  6034  fnsuppresOLD  6048  weniso  6155  epne3  6503  limsuc  6571  funsssuppss  6826  smoel  6932  smoord  6937  omwordi  7121  oneo  7131  oeord  7138  oewordi  7141  nnmwordi  7185  nnneo  7201  uniinqs  7291  undifixp  7410  enfixsn  7531  domss2  7581  domssex2  7582  unxpdomlem3  7631  dif1enOLD  7656  dif1en  7657  mapfien2  7770  dffi2  7785  unwdomg  7911  ixpiunwdom  7918  en3lplem1  7932  oemapvali  8004  fodomfi2  8342  infcdaabs  8487  infunabs  8488  infdif  8490  ackbij1lem9  8509  ackbij1lem16  8516  coflim  8542  cfsmolem  8551  isfin2-2  8600  fin1a2lem9  8689  hsmexlem2  8708  axcc2lem  8717  axcc3  8719  domtriomlem  8723  axdc3lem4  8734  axcclem  8738  zornn0g  8786  axacndlem4  8889  axacndlem5  8890  axacnd  8891  gchdomtri  8908  fpwwe  8925  tskssel  9036  tskint  9064  tskurn  9068  gruurn  9077  gruixp  9088  grudomon  9096  gruina  9097  adderpqlem  9235  mulerpqlem  9236  addassnq  9239  mulassnq  9240  distrnq  9242  ltsonq  9250  ltanq  9252  ltmnq  9253  reclem3pr  9330  dedekind  9645  addid2  9664  addcan2  9666  divdir  10129  divcan5  10145  ltdiv1  10305  infmrcl  10421  infmrlb  10423  lt2halves  10671  zdivmul  10826  xaddass  11324  xleadd1  11330  xltadd1  11331  xmulasslem3  11361  xmulass  11362  xlemul1  11365  xlemul2  11366  xltmul1  11367  xadddir  11371  elioo5  11465  iccsupr  11500  iccneg  11524  icoshft  11525  icoshftf1o  11526  iccsplit  11536  fzen  11585  elfzelfzelfz  11602  elfz0fzfz0  11603  fz0fzelfz0  11604  fz0fzdiffz0  11607  elfz1b  11645  fzrevral  11662  fzshftral  11665  elfzo  11673  ltdifltdiv  11796  modabs  11859  modcyc  11861  modaddmulmod  11883  moddi  11884  modsubdir  11885  expdiv  12032  leexp2a  12037  bcval3  12200  hashnnn0genn0  12232  hashgadd  12259  hashunx  12268  hashtpg  12305  hashfun  12318  brfi1indlem  12337  ccatval1  12395  ccatval2  12396  ccatval3  12397  ccatsymb  12400  ccatass  12405  ccats1val2  12426  swrdval2  12435  swrd0len0  12448  swrd0fv  12454  swrdeq  12459  2swrdeqwrdeq  12466  swrdswrdlem  12472  swrdswrd  12473  swrd0swrd  12474  ccats1swrdeq  12482  swrdccatin12lem2  12499  swrdccat3b  12506  swrdccatid  12507  splval  12512  repswswrd  12541  cshwidxmod  12559  cshwidx0mod  12560  cshwleneq  12570  ccatco  12582  cshco  12583  swrdco  12584  f1oun2prg  12646  swrds2  12664  elicc4abs  12926  mulcn2  13192  demoivreALT  13604  rpnnen2lem4  13619  dvdsval2  13657  dvdsexp  13708  mulgcd  13849  mulgcdr  13851  gcddiv  13852  rpmulgcd  13858  rplpwr  13859  prmexpb  13922  rpexp  13925  modprm0  13992  modprmn0modprm0  13994  coprimeprodsq  13995  pythagtriplem1  14002  pythagtriplem3  14004  pythagtriplem10  14006  pythagtriplem6  14007  pythagtriplem11  14011  pythagtriplem12  14012  pythagtriplem13  14013  pythagtriplem15  14015  pythagtriplem17  14017  pythagtriplem19  14019  pcdvdsb  14054  pcfaclem  14079  vdwapun  14154  ramval  14188  0ram2  14201  0ramcl  14203  imasaddvallem  14587  imasvscaval  14596  mreiincl  14654  mremre  14662  mrieqv2d  14697  cofurid  14921  xpcpropd  15138  clatleglb  15416  ress0g  15570  gsumccat  15639  gsumccatsn  15641  mulgdirlem  15771  mulgp1  15773  eqglact  15852  fvcosymgeq  16054  gsmsymgreqlem2  16056  pmtrprfv3  16080  pmtr3ncomlem1  16099  mndodcongi  16168  oddvdsnn0  16169  odngen  16198  gexnnod  16209  lsmlub  16284  lsmass  16289  efgsval2  16352  efgsrel  16353  ghmplusg  16450  odadd1  16452  odadd2  16453  gsumsn  16572  dvrcan1  16907  dvrcan3  16908  irredrmul  16923  srngadd  17066  srngmul  17067  lmhmvsca  17250  reslmhm2  17258  pwssplit3  17266  lbspss  17287  lsmsp  17291  lspsneu  17328  lidldvgen  17461  evlsval  17730  evlsval2  17731  psropprmul  17817  coe1add  17842  coe1addfv  17843  coe1subfv  17844  coe1tm  17851  coe1sclmul  17860  coe1sclmul2  17862  evl1gsumdlem  17916  zrhpsgninv  18141  zrhpsgnevpm  18147  zrhpsgnodpm  18148  psgndiflemB  18156  cssmre  18244  frlmup4  18355  islindf2  18369  lindsind2  18374  f1lindf  18377  lindsss  18379  f1linds  18380  lindsmm  18383  lbslcic  18396  mndvcl  18417  mndvass  18418  mhmvlin  18423  mamulid  18430  mamurid  18431  matecl  18452  mattposm  18472  madetsumid  18474  matepmcl  18475  matepm2cl  18476  mavmulsolcl  18490  mulmarep1el  18511  mulmarep1gsum1  18512  mulmarep1gsum2  18513  1marepvsma1  18522  m1detdiag  18536  mdetdiaglem  18537  mdetdiag  18538  mdetunilem7  18557  mdetunilem9  18559  mdetmul  18562  gsummatr01lem3  18596  gsummatr01lem4  18597  gsummatr01  18598  smadiadetglem2  18611  matinv  18616  slesolinv  18619  cramerimplem1  18622  cramerimp  18625  cramerlem1  18626  iuncld  18782  clsss  18791  ntrcls0  18813  iscldtop  18832  neiss  18846  neips  18850  restcldi  18910  cnpnei  19001  cnconst2  19020  cnpresti  19025  sslm  19036  cnt0  19083  cnt1  19087  cnhaus  19091  cncmp  19128  cmpcld  19138  cnconn  19159  concompss  19170  elptr  19279  upxp  19329  qtoptop2  19405  ordthmeolem  19507  opnfbas  19548  isfil2  19562  fbasweak  19571  snfbas  19572  fgss  19579  fgcl  19584  fbasrn  19590  trnei  19598  cfinfil  19599  csdfil  19600  supfil  19601  filufint  19626  fin1aufil  19638  fmval  19649  fmf  19651  elfm  19653  elfm3  19656  imaelfm  19657  rnelfmlem  19658  rnelfm  19659  flimclslem  19690  flfneii  19698  cnpfcfi  19746  alexsubALT  19756  ptcmplem3  19759  ustref  19926  ustelimasn  19930  utop3cls  19959  ressusp  19973  cfiluexsm  19998  prdsxmetlem  20076  txmetcn  20256  nmmtri  20346  nmrtri  20348  unitnmn0  20382  nminvr  20383  nmotri  20451  nghmplusg  20452  isclmi  20782  fmcfil  20916  srabn  21005  rrxmvallem  21036  itgconst  21430  dvn2bss  21538  deg1mul3  21721  deg1mul3le  21722  deg1tmle  21723  q1peqb  21760  r1pcl  21763  r1pdeglt  21764  r1pid  21765  dvdsq1p  21766  dvdsr1p  21767  ptolemy  22092  sincosq1eq  22108  logmul2  22199  logdiv2  22200  cxplt2  22277  pythag  22347  bcmono  22750  efexple  22754  lgsdirnn0  22812  selberglem3  22930  brbtwn2  23304  axcgrid  23315  ax5seglem1  23327  ax5seglem2  23328  ax5seg  23337  axpasch  23340  axlowdimlem16  23356  axcontlem7  23369  nbgraf1olem1  23503  nbusgrafi  23510  nb3graprlem1  23512  nb3graprlem2  23513  cusgra2v  23523  cusgra3v  23525  2trllemH  23604  2trllemE  23605  constr1trl  23640  constr2spthlem1  23646  2pthlem2  23648  2wlklem1  23649  2pthon  23654  constr3lem4  23686  constr3trllem2  23690  constr3trllem5  23693  constr3pthlem2  23695  vdgrfival  23720  vdgrf  23721  vdgrfif  23722  vdusgra0nedg  23731  hashnbgravd  23733  gxpval  23899  gxnval  23900  gxnn0neg  23903  gxnn0suc  23904  gxneg  23906  gxsuc  23912  gxnn0add  23914  gxadd  23915  gxsub  23916  gxnn0mul  23917  gxmul  23918  gxmodid  23919  gxdi  23936  zerdivemp1  24074  rngoridfz  24075  vcid  24082  vcdi  24083  vcdir  24084  vcass  24085  imsmetlem  24234  0oval  24341  ajval  24415  shlub  24970  hmopco  25580  adjlnop  25643  mdslmd4i  25890  divnumden2  26233  ressnm  26258  gsumsnf  26390  ress1r  26403  pstmfval  26469  pl1cn  26531  logeq0im1  26599  ind1  26621  ind0  26622  sigaclcuni  26707  sigagenss2  26739  measun  26771  measvuni  26774  dya2iocnrect  26841  ballotlemieq  27044  ballotlemrv1  27048  sgn3da  27069  lgamgulmlem1  27160  erdszelem2  27225  cnpcon  27264  cvmscld  27307  ghomf1olem  27458  prodfrec  27555  ntrivcvgfvn0  27559  iprodefisumlem  27649  binomrisefac  27690  dvdspw  27701  dfon2lem3  27743  dfon2lem7  27747  predeq123  27771  predpo  27790  frrlem4  27916  nofulllem3  27990  btwndiff  28203  brcolinear2  28234  btwnconn1  28277  nnssi3  28447  nndivsub  28448  ftc1anclem4  28619  areacirclem2  28634  areacirclem5  28637  areacirc  28638  nn0prpwlem  28666  hmeoclda  28677  hmeocldb  28678  ivthALT  28679  ssref  28704  fnemeet1  28736  fnejoin1  28738  upixp  28772  filbcmb  28783  cnresima  28812  smprngopr  29001  igenval2  29015  ismrcd1  29183  istopclsd  29185  ismrc  29186  mapfzcons  29201  eldioph2  29249  diophrex  29263  diophren  29301  pellexlem1  29319  pellexlem5  29323  pellqrexplicit  29367  reglogmul  29383  reglogexp  29384  rmxycomplete  29407  congmul  29459  congabseq  29466  acongsym  29468  acongneg2  29469  fzneg  29474  acongeq  29475  jm2.19  29491  jm2.22  29493  jm2.23  29494  jm2.20nn  29495  rmydioph  29512  rmxdiophlem  29513  jm3.1  29518  pwssplit4  29591  mapfien2OLD  29598  hbtlem2  29629  idomrootle  29709  dvconstbi  29757  expgrowth  29758  fmul01lt1lem1  29914  climsuselem1  29929  climsuse  29930  stoweidlem3  29947  stoweidlem16  29960  stoweidlem17  29961  stoweidlem26  29970  stoweidlem34  29978  stoweidlem57  30001  el2xptp0  30276  oteqimp  30278  otthg  30279  ovmpt3rab1  30310  2leaddle2  30324  ssfz12  30346  elfzonlteqm1  30374  fsumsplitsndif  30387  fsummmodsndifre  30388  fsumsplitsnun  30391  fsummmodsnunre  30392  modfsummods  30393  ccats1swrdeqrex  30408  wlkelwrd  30429  wlkcomp  30435  2wlkeq  30437  usg2wlkeq  30438  usgra2pth  30450  wlkiswwlk2  30480  usg2wlkeq2  30490  wwlknred  30504  wwlknext  30505  wwlknredwwlkn  30507  wwlknfi  30519  wlknfi  30520  wlknwwlknvbij  30521  el2wlkonot  30537  el2spthonot  30538  el2spthonot0  30539  el2wlkonotot0  30540  clwlkcomp  30575  clwwlkgt0  30583  clwwlknprop  30584  clwwlkn0  30586  clwwlkel  30604  clwwlkf  30605  clwwlkf1  30607  clwwlkfo  30608  clwwlkvbij  30612  clwwlkext2edg  30613  clwwisshclwwlem1  30618  clwwisshclww  30620  clwwnisshclwwn  30622  erclwwlkeqlen  30631  erclwwlkref  30632  eleclclwwlknlem2  30640  scshwfzeqfzo  30641  erclwwlkneqlen  30647  erclwwlknref  30648  erclwwlknsym  30649  erclwwlkntr  30650  hashecclwwlkn1  30657  usghashecclwwlk  30658  hashclwwlkn  30659  clwwlkndivn  30660  clwlkfclwwlk  30666  clwlkfoclwwlk  30667  clwlkf1clwwlklem  30671  clwlkf1clwwlk  30672  nbhashnn0  30681  isrgra  30692  rusgranumwlkl1lem1  30707  wwlkextproplem3  30711  rusgra0edg  30722  rusgranumwlks  30723  3vfriswmgralem  30745  3vfriswmgra  30746  usgn0fidegnn0  30771  2spotdisj  30803  usg2spot2nb  30807  extwwlkfablem1  30816  clwwlkextfrlem1  30818  extwwlkfablem2  30820  numclwwlkun  30821  numclwwlkovf2ex  30828  extwwlkfab  30832  numclwlk1lem2foa  30833  numclwlk1lem2f1  30836  numclwlk1lem2fo  30837  numclwwlk1  30840  numclwwlk2lem1  30844  numclwlk2lem2f  30845  numclwlk2lem2f1o  30847  numclwwlk2  30849  numclwwlk3  30851  numclwwlk4  30852  numclwwlk6  30855  numclwwlk7  30856  numclwwlk8  30857  frgrareg  30859  frgraregord013  30860  ofaddmndmap  30883  mapprop  30885  nn0sumltlt  30891  gsumpr  30907  domnmsuppn0  30931  scmsuppss  30934  mndpsuppfi  30938  gsumlsscl  30970  assa2ass  30975  ply1ass23l  30982  coe1fzgsumdlem  30991  ply1mulgsumlem1  30999  lply1binom  31010  matvscacell  31022  mat1dimbas  31035  lincfsuppcl  31080  linccl  31081  lincvalsng  31083  lincvalpr  31085  lincdifsn  31091  ellcoellss  31102  lincext1  31121  lincext2  31122  lincext3  31123  lindslinindimp2lem2  31126  ldepspr  31140  lincresunit3lem1  31146  lincresunit3lem2  31147  islindeps2  31150  pmatcoe1fsupp  31193  mat2pmatbas  31216  m2pminv2  31240  decpmatmullem  31259  pmatcollpw3lem  31271  cpscmat  31329  chordthmALT  32002  bnj837  32087  bnj517  32211  bnj553  32224  bnj594  32238  bnj967  32271  bnj1097  32305  bnj1110  32306  bnj1118  32308  bnj1128  32314  bnj1125  32316  bnj1145  32317  bnj1136  32321  bnj1173  32326  bnj1189  32333  bnj1204  32336  bnj1279  32342  bnj1321  32351  bnj1413  32359  bj-ceqsalt1  32718  lsmsat  32992  lsmsatcv  32994  lsatcvatlem  33033  islshpcv  33037  l1cvpat  33038  lfli  33045  lshpset2N  33103  cvrnbtwn  33255  meetat2  33281  atcmp  33295  atcvreq0  33298  atlatmstc  33303  cvlcvr1  33323  cvlcvrp  33324  cvlatcvr2  33326  cvr2N  33394  cvratlem  33404  2atjm  33428  athgt  33439  2lplnmN  33542  2llnmj  33543  2lplnmj  33605  dalemswapyzps  33673  dalem23  33679  dalem24  33680  dalem25  33681  dalem27  33682  dalem28  33683  dalem38  33693  dalem39  33694  dalem44  33699  dalem45  33700  dalem51  33706  dalem52  33707  dalem56  33711  pmapglbx  33752  pmapjat1  33836  pmapjat2  33837  paddatclN  33932  osumcllem4N  33942  osumcllem7N  33945  ltrncoval  34128  cdleme0aa  34193  cdleme0b  34195  cdleme8  34233  cdlemesner  34279  cdleme22eALTN  34328  cdleme26eALTN  34344  cdleme35h  34439  cdleme50trn2  34534  cdleme  34543  tgrpov  34731  tendotp  34744  tendoidcl  34752  tendo0co2  34771  cdlemkvcl  34825  dvhopvadd  35077  dvhopellsm  35101  dihmeetlem1N  35274  dihmeetlem9N  35299  dihatexv  35322  lcfl7lem  35483  mapdrvallem2  35629  mapdh9a  35774  hdmapevec  35822
  Copyright terms: Public domain W3C validator