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

Theorem 3ad2ant3 981
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 454 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 976 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simp3l  986  simp3r  987  simp31  994  simp32  995  simp33  996  simp3ll  1029  simp3lr  1030  simp3rl  1031  simp3rr  1032  simp3l1  1063  simp3l2  1064  simp3l3  1065  simp3r1  1066  simp3r2  1067  simp3r3  1068  simp31l  1081  simp31r  1082  simp32l  1083  simp32r  1084  simp33l  1085  simp33r  1086  simp311  1105  simp312  1106  simp313  1107  simp321  1108  simp322  1109  simp323  1110  simp331  1111  simp332  1112  simp333  1113  3anim123i  1140  3jaao  1252  ceqsalt  2980  ceqsralt  2981  vtoclgft  3004  tpssi  3967  prnebg  3981  epne3  4764  limsuc  4832  poltletr  5272  funprg  5503  funtpg  5504  fntpg  5509  ftpg  5919  fsnunf  5934  fsnunfv  5936  fvpr1g  5940  fvpr2g  5941  fnsuppres  5955  weniso  6078  smoel  6625  smoord  6630  omwordi  6817  oneo  6827  oeord  6834  oewordi  6837  nnmwordi  6881  nnneo  6897  uniinqs  6987  undifixp  7101  domss2  7269  domssex2  7270  unxpdomlem3  7318  dif1enOLD  7343  dif1en  7344  dffi2  7431  unwdomg  7555  ixpiunwdom  7562  oemapvali  7643  en3lplem1  7673  fodomfi2  7946  infcdaabs  8091  infunabs  8092  infdif  8094  ackbij1lem9  8113  ackbij1lem16  8120  coflim  8146  cfsmolem  8155  isfin2-2  8204  fin1a2lem9  8293  hsmexlem2  8312  axcc2lem  8321  axcc3  8323  domtriomlem  8327  axdc3lem4  8338  axcclem  8342  zornn0g  8390  axacndlem4  8490  axacndlem5  8491  axacnd  8492  gchdomtri  8509  fpwwe  8526  tskssel  8637  tskint  8665  tskurn  8669  gruurn  8678  gruixp  8689  grudomon  8697  gruina  8698  adderpqlem  8836  mulerpqlem  8837  addassnq  8840  mulassnq  8841  distrnq  8843  ltsonq  8851  ltanq  8853  ltmnq  8854  reclem3pr  8931  addid2  9254  addcan2  9256  divdir  9706  divcan5  9721  ltdiv1  9879  infmrcl  9992  infmrlb  9994  lt2halves  10207  zdivmul  10347  xaddass  10833  xleadd1  10839  xltadd1  10840  xmulasslem3  10870  xmulass  10871  xlemul1  10874  xlemul2  10875  xltmul1  10876  xadddir  10880  elioo5  10973  iccsupr  11002  iccneg  11023  icoshft  11024  icoshftf1o  11025  iccsplit  11034  fzen  11077  fzrevral  11136  fzshftral  11139  elfzo  11147  modabs  11279  modcyc  11281  moddi  11289  modsubdir  11290  expdiv  11435  leexp2a  11440  bcval3  11602  hashnnn0genn0  11632  hashgadd  11656  hashunx  11665  hashtpg  11696  hashfun  11705  brfi1indlem  11719  ccatval1  11750  ccatval2  11751  ccatval3  11752  ccatass  11755  swrdval2  11772  splval  11785  ccatco  11809  f1oun2prg  11869  swrds2  11885  sqr0  12052  elicc4abs  12128  mulcn2  12394  demoivreALT  12807  rpnnen2lem4  12822  dvdsval2  12860  dvdsexp  12910  mulgcd  13051  mulgcdr  13053  gcddiv  13054  rpmulgcd  13060  rplpwr  13061  prmexpb  13122  rpexp  13125  coprimeprodsq  13188  pythagtriplem1  13195  pythagtriplem3  13197  pythagtriplem10  13199  pythagtriplem6  13200  pythagtriplem11  13204  pythagtriplem12  13205  pythagtriplem13  13206  pythagtriplem15  13208  pythagtriplem17  13210  pythagtriplem19  13212  pcdvdsb  13247  pcfaclem  13272  vdwapun  13347  ramval  13381  0ram2  13394  0ramcl  13396  imasaddvallem  13759  imasvscaval  13768  mreiincl  13826  mremre  13834  mrieqv2d  13869  cofurid  14093  xpcpropd  14310  clatleglb  14558  gsumccat  14792  mulgdirlem  14919  mulgp1  14921  eqglact  14996  mndodcongi  15186  oddvdsnn0  15187  odngen  15216  gexnnod  15227  lsmlub  15302  lsmass  15307  efgsval2  15370  efgsrel  15371  ghmplusg  15466  odadd1  15468  odadd2  15469  gsumsn  15548  dvrcan1  15801  dvrcan3  15802  irredrmul  15817  srngadd  15950  srngmul  15951  lmhmvsca  16126  reslmhm2  16134  lbspss  16159  lsmsp  16163  lspsneu  16200  lidldvgen  16331  psropprmul  16637  coe1add  16662  coe1addfv  16663  coe1subfv  16664  coe1tm  16670  coe1sclmul  16679  coe1sclmul2  16681  cssmre  16925  iuncld  17114  clsss  17123  ntrcls0  17145  iscldtop  17164  neiss  17178  neips  17182  restcldi  17242  cnpnei  17333  cnconst2  17352  cnpresti  17357  sslm  17368  cnt0  17415  cnt1  17419  cnhaus  17423  cncmp  17460  cmpcld  17470  cnconn  17490  concompss  17501  elptr  17610  upxp  17660  qtoptop2  17736  ordthmeolem  17838  opnfbas  17879  isfil2  17893  fbasweak  17902  snfbas  17903  fgss  17910  fgcl  17915  fbasrn  17921  trnei  17929  cfinfil  17930  csdfil  17931  supfil  17932  filufint  17957  fin1aufil  17969  fmval  17980  fmf  17982  elfm  17984  elfm3  17987  imaelfm  17988  rnelfmlem  17989  rnelfm  17990  flimclslem  18021  flfneii  18029  cnpfcfi  18077  alexsubALT  18087  ptcmplem3  18090  ustref  18253  ustelimasn  18257  utop3cls  18286  ressusp  18300  cfiluexsm  18325  prdsxmetlem  18403  txmetcn  18583  nmmtri  18673  nmrtri  18675  unitnmn0  18709  nminvr  18710  nmotri  18778  nghmplusg  18779  isclmi  19107  fmcfil  19230  srabn  19319  itgconst  19713  dvn2bss  19821  evlsval  19945  evlsval2  19946  deg1mul3  20043  deg1mul3le  20044  deg1tmle  20045  q1peqb  20082  r1pcl  20085  r1pdeglt  20086  r1pid  20087  dvdsq1p  20088  dvdsr1p  20089  ptolemy  20409  sincosq1eq  20425  logmul2  20516  logdiv2  20517  cxplt2  20594  pythag  20664  bcmono  21066  efexple  21070  lgsdirnn0  21128  selberglem3  21246  nbgraf1olem1  21456  nbusgrafi  21463  nb3graprlem1  21465  nb3graprlem2  21466  cusgra2v  21476  cusgra3v  21478  2trllemH  21557  2trllemE  21558  constr1trl  21593  constr2spthlem1  21599  2pthlem2  21601  2wlklem1  21602  2pthon  21607  constr3lem4  21639  constr3trllem2  21643  constr3trllem5  21646  constr3pthlem2  21648  vdgrfival  21673  vdgrf  21674  vdgrfif  21675  vdusgra0nedg  21684  hashnbgravd  21686  gxpval  21852  gxnval  21853  gxnn0neg  21856  gxnn0suc  21857  gxneg  21859  gxsuc  21865  gxnn0add  21867  gxadd  21868  gxsub  21869  gxnn0mul  21870  gxmul  21871  gxmodid  21872  gxdi  21889  zerdivemp1  22027  rngoridfz  22028  vcid  22035  vcdi  22036  vcdir  22037  vcass  22038  imsmetlem  22187  0oval  22294  ajval  22368  shlub  22921  hmopco  23531  adjlnop  23594  mdslmd4i  23841  divnumden2  24166  ress0g  24187  ressnm  24189  ofldadd  24243  ofldmul  24244  pstmfval  24296  logeq0im1  24399  ind1  24421  ind0  24422  sigaclcuni  24506  sigagenss2  24538  measun  24570  measvuni  24573  dya2iocnrect  24636  ballotlemieq  24779  ballotlemrv1  24783  lgamgulmlem1  24818  erdszelem2  24883  cnpcon  24922  cvmscld  24965  ghomf1olem  25110  dedekind  25192  prodfrec  25228  ntrivcvgfvn0  25232  iprodefisumlem  25322  binomrisefac  25363  dvdspw  25374  dfon2lem3  25417  dfon2lem7  25421  predeq123  25445  predpo  25464  frrlem4  25590  nofulllem3  25664  brbtwn2  25849  axcgrid  25860  ax5seglem1  25872  ax5seglem2  25873  ax5seg  25882  axpasch  25885  axlowdimlem16  25901  axcontlem7  25914  btwndiff  25966  brcolinear2  25997  btwnconn1  26040  nnssi3  26211  nndivsub  26212  ftc1anclem4  26297  areacirclem2  26307  areacirclem5  26310  areacirc  26311  nn0prpwlem  26339  hmeoclda  26350  hmeocldb  26351  ivthALT  26352  ssref  26377  fnemeet1  26409  fnejoin1  26411  upixp  26445  filbcmb  26456  cnresima  26487  smprngopr  26676  igenval2  26690  ismrcd1  26766  istopclsd  26768  ismrc  26769  mapfzcons  26786  eldioph2  26834  diophrex  26848  diophren  26888  pellexlem1  26906  pellexlem5  26910  pellqrexplicit  26954  reglogmul  26970  reglogexp  26971  rmxycomplete  26994  congmul  27046  congabseq  27053  acongsym  27055  acongneg2  27056  fzneg  27061  acongeq  27062  jm2.19  27078  jm2.22  27080  jm2.23  27081  jm2.20nn  27082  rmydioph  27099  rmxdiophlem  27100  jm3.1  27105  pwssplit3  27181  pwssplit4  27182  frlmup4  27244  enfixsn  27248  mapfien2  27249  islindf2  27275  lindsind2  27280  f1lindf  27283  lindsss  27285  f1linds  27286  lindsmm  27289  lbslcic  27302  hbtlem2  27319  mndvcl  27437  mndvass  27438  mhmvlin  27443  idomrootle  27502  dvconstbi  27542  expgrowth  27543  fmul01lt1lem1  27704  climsuselem1  27723  climsuse  27724  stoweidlem3  27742  stoweidlem16  27755  stoweidlem17  27756  stoweidlem26  27765  stoweidlem34  27773  stoweidlem57  27796  el2xptp0  28076  oteqimp  28078  otthg  28079  2leaddle2  28115  ssfz12  28127  elfzelfzelfz  28132  elfz0fzfz0  28137  fz0fzelfz0  28141  fz0fzdiffz0  28142  ltdifltdiv  28171  modaddmulmod  28181  ccatsymb  28211  swrd0fv  28226  swrd0swrd  28231  swrdswrdlem  28232  swrdswrd  28233  swrdccatin12lem3  28246  swrdccat3b  28253  modprm0  28262  cshwleneq  28302  3cshw  28303  cshweqdif2  28304  cshweqdif2s  28305  wlkelwrd  28333  wlkcomp  28339  2wlkeq  28341  usg2wlkeq  28342  usgra2pth  28349  wlkiswwlk2  28379  el2wlkonot  28401  el2spthonot  28402  el2spthonot0  28403  el2wlkonotot0  28404  nbhashnn0  28430  isrgra  28441  3vfriswmgralem  28468  3vfriswmgra  28469  2spotdisj  28524  usg2spot2nb  28528  chordthmALT  29119  bnj837  29204  bnj517  29330  bnj553  29343  bnj594  29357  bnj967  29390  bnj1097  29424  bnj1110  29425  bnj1118  29427  bnj1128  29433  bnj1125  29435  bnj1145  29436  bnj1136  29440  bnj1173  29445  bnj1189  29452  bnj1204  29455  bnj1279  29461  bnj1321  29470  bnj1413  29478  lsmsat  29880  lsmsatcv  29882  lsatcvatlem  29921  islshpcv  29925  l1cvpat  29926  lfli  29933  lshpset2N  29991  cvrnbtwn  30143  meetat2  30169  atcmp  30183  atcvreq0  30186  atlatmstc  30191  cvlcvr1  30211  cvlcvrp  30212  cvlatcvr2  30214  cvr2N  30282  cvratlem  30292  2atjm  30316  athgt  30327  2lplnmN  30430  2llnmj  30431  2lplnmj  30493  dalemswapyzps  30561  dalem23  30567  dalem24  30568  dalem25  30569  dalem27  30570  dalem28  30571  dalem38  30581  dalem39  30582  dalem44  30587  dalem45  30588  dalem51  30594  dalem52  30595  dalem56  30599  pmapglbx  30640  pmapjat1  30724  pmapjat2  30725  paddatclN  30820  osumcllem4N  30830  osumcllem7N  30833  ltrncoval  31016  cdleme0aa  31081  cdleme0b  31083  cdleme8  31121  cdlemesner  31167  cdleme22eALTN  31216  cdleme26eALTN  31232  cdleme35h  31327  cdleme50trn2  31422  cdleme  31431  tgrpov  31619  tendotp  31632  tendoidcl  31640  tendo0co2  31659  cdlemkvcl  31713  dvhopvadd  31965  dvhopellsm  31989  dihmeetlem1N  32162  dihmeetlem9N  32187  dihatexv  32210  lcfl7lem  32371  mapdrvallem2  32517  mapdh9a  32662  hdmapevec  32710
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator