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

Theorem 3ad2ant3 978
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 452 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 973 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp3l  983  simp3r  984  simp31  991  simp32  992  simp33  993  simp3ll  1026  simp3lr  1027  simp3rl  1028  simp3rr  1029  simp3l1  1060  simp3l2  1061  simp3l3  1062  simp3r1  1063  simp3r2  1064  simp3r3  1065  simp31l  1078  simp31r  1079  simp32l  1080  simp32r  1081  simp33l  1082  simp33r  1083  simp311  1102  simp312  1103  simp313  1104  simp321  1105  simp322  1106  simp323  1107  simp331  1108  simp332  1109  simp333  1110  3anim123i  1137  3jaao  1249  ceqsalt  2844  ceqsralt  2845  vtoclgft  2868  epne3  4609  limsuc  4677  poltletr  5115  funprg  5338  fsnunf  5757  fsnunfv  5759  fnsuppres  5773  weniso  5894  smoel  6419  smoord  6424  omwordi  6611  oneo  6621  oeord  6628  oewordi  6631  nnmwordi  6675  nnneo  6691  uniinqs  6781  undifixp  6895  domss2  7063  domssex2  7064  unxpdomlem3  7112  dif1enOLD  7135  dif1en  7136  dffi2  7221  unwdomg  7343  ixpiunwdom  7350  oemapvali  7431  en3lplem1  7461  fodomfi2  7732  infcdaabs  7877  infunabs  7878  infdif  7880  ackbij1lem9  7899  ackbij1lem16  7906  coflim  7932  cfsmolem  7941  isfin2-2  7990  fin1a2lem9  8079  hsmexlem2  8098  axcc2lem  8107  axcc3  8109  domtriomlem  8113  axdc3lem4  8124  axcclem  8128  zornn0g  8177  axacndlem4  8277  axacndlem5  8278  axacnd  8279  gchdomtri  8296  fpwwe  8313  tskssel  8424  tskint  8452  tskurn  8456  gruurn  8465  gruixp  8476  grudomon  8484  gruina  8485  adderpqlem  8623  mulerpqlem  8624  addassnq  8627  mulassnq  8628  distrnq  8630  ltsonq  8638  ltanq  8640  ltmnq  8641  reclem3pr  8718  addid2  9040  addcan2  9042  divdir  9492  divcan5  9507  ltdiv1  9665  infmrcl  9778  infmrlb  9780  lt2halves  9993  zdivmul  10131  xaddass  10616  xleadd1  10622  xltadd1  10623  xmulasslem3  10653  xmulass  10654  xlemul1  10657  xlemul2  10658  xltmul1  10659  xadddir  10663  elioo5  10755  iccsupr  10783  iccneg  10804  icoshft  10805  icoshftf1o  10806  iccsplit  10815  fzen  10858  fzrevral  10913  fzshftral  10916  elfzo  10924  modabs  11044  modcyc  11046  moddi  11054  modsubdir  11055  expdiv  11199  leexp2a  11204  bcval3  11366  hashgadd  11406  hashfun  11436  ccatval1  11478  ccatval2  11479  ccatval3  11480  ccatass  11483  swrdval2  11500  splval  11513  ccatco  11537  swrds2  11607  sqr0  11774  elicc4abs  11850  mulcn2  12116  demoivreALT  12528  rpnnen2lem4  12543  dvdsval2  12581  dvdsexp  12631  mulgcd  12772  mulgcdr  12774  gcddiv  12775  rpmulgcd  12781  rplpwr  12782  prmexpb  12843  rpexp  12846  coprimeprodsq  12909  pythagtriplem1  12916  pythagtriplem3  12918  pythagtriplem10  12920  pythagtriplem6  12921  pythagtriplem11  12925  pythagtriplem12  12926  pythagtriplem13  12927  pythagtriplem15  12929  pythagtriplem17  12931  pythagtriplem19  12933  pcdvdsb  12968  pcfaclem  12993  vdwapun  13068  ramval  13102  0ram2  13115  0ramcl  13117  imasaddvallem  13480  imasvscaval  13489  mreiincl  13547  mremre  13555  mrieqv2d  13590  cofurid  13814  xpcpropd  14031  clatleglb  14279  gsumccat  14513  mulgdirlem  14640  mulgp1  14642  eqglact  14717  mndodcongi  14907  oddvdsnn0  14908  odngen  14937  gexnnod  14948  lsmlub  15023  lsmass  15028  efgsval2  15091  efgsrel  15092  ghmplusg  15187  odadd1  15189  odadd2  15190  gsumsn  15269  dvrcan1  15522  dvrcan3  15523  irredrmul  15538  srngadd  15671  srngmul  15672  lmhmvsca  15851  reslmhm2  15859  lbspss  15884  lsmsp  15888  lspsneu  15925  lidldvgen  16056  psropprmul  16365  coe1add  16390  coe1addfv  16391  coe1subfv  16392  coe1tm  16398  coe1sclmul  16407  coe1sclmul2  16409  cssmre  16649  iuncld  16838  clsss  16847  ntrcls0  16869  iscldtop  16888  neiss  16902  neips  16906  restcldi  16960  cnpnei  17049  cnconst2  17067  cnpresti  17072  sslm  17083  cnt0  17130  cnt1  17134  cnhaus  17138  cncmp  17175  cmpcld  17185  cnconn  17204  concompss  17215  elptr  17324  upxp  17373  qtoptop2  17446  ordthmeolem  17548  opnfbas  17589  isfil2  17603  fbasweak  17612  snfbas  17613  fgss  17620  fgcl  17625  fbasrn  17631  trnei  17639  cfinfil  17640  csdfil  17641  supfil  17642  filufint  17667  fin1aufil  17679  fmval  17690  fmf  17692  elfm  17694  elfm3  17697  imaelfm  17698  rnelfmlem  17699  rnelfm  17700  flimclslem  17731  flfneii  17739  cnpfcfi  17787  alexsubALT  17797  ptcmplem3  17800  prdsxmetlem  17984  txmetcn  18146  nmmtri  18195  nmrtri  18197  unitnmn0  18231  nminvr  18232  nmotri  18300  nghmplusg  18301  isclmi  18628  fmcfil  18751  srabn  18830  itgconst  19226  dvn2bss  19332  evlsval  19456  evlsval2  19457  deg1mul3  19554  deg1mul3le  19555  deg1tmle  19556  q1peqb  19593  r1pcl  19596  r1pdeglt  19597  r1pid  19598  dvdsq1p  19599  dvdsr1p  19600  ptolemy  19917  sincosq1eq  19933  cxplt2  20098  pythag  20168  bcmono  20569  efexple  20573  lgsdirnn0  20631  selberglem3  20749  gxpval  20979  gxnval  20980  gxnn0neg  20983  gxnn0suc  20984  gxneg  20986  gxsuc  20992  gxnn0add  20994  gxadd  20995  gxsub  20996  gxnn0mul  20997  gxmul  20998  gxmodid  20999  gxdi  21016  zerdivemp1  21154  rngoridfz  21155  vcid  21162  vcdi  21163  vcdir  21164  vcass  21165  imsmetlem  21314  0oval  21421  ajval  21495  shlub  22048  hmopco  22658  adjlnop  22721  mdslmd4i  22968  divnumden2  23313  ress0g  23335  ressnm  23337  ustref  23431  ressusp  23461  cfiluexsm  23482  logeq0im1  23586  sigaclcuni  23677  sigagenss2  23709  measun  23739  measvuni  23742  dya2iocnrect  23805  ind1  23831  ind0  23832  ballotlemieq  23948  ballotlemrv1  23952  erdszelem2  24007  cnpcon  24045  cvmscld  24088  ghomf1olem  24285  dedekind  24368  ntrivcvgfvn0  24404  dvdspw  24488  dfon2lem3  24526  dfon2lem7  24530  predpo  24569  frrlem4  24669  nofulllem3  24743  brbtwn2  24919  axcgrid  24930  ax5seglem1  24942  ax5seglem2  24943  ax5seg  24952  axpasch  24955  axlowdimlem16  24971  axcontlem7  24984  btwndiff  25036  brcolinear2  25067  btwnconn1  25110  nnssi3  25281  nndivsub  25282  areacirclem4  25344  areacirclem6  25347  areacirc  25348  nn0prpwlem  25387  hmeoclda  25400  hmeocldb  25401  ivthALT  25407  ssref  25432  fnemeet1  25464  fnejoin1  25466  upixp  25552  filbcmb  25581  cnresima  25632  smprngopr  25825  igenval2  25839  ismrcd1  25921  istopclsd  25923  ismrc  25924  mapfzcons  25941  eldioph2  25989  diophrex  26003  diophren  26044  pellexlem1  26062  pellexlem5  26066  pellqrexplicit  26110  reglogmul  26126  reglogexp  26127  rmxycomplete  26150  congmul  26202  congabseq  26209  acongsym  26211  acongneg2  26212  fzneg  26217  acongeq  26218  jm2.19  26234  jm2.22  26236  jm2.23  26237  jm2.20nn  26238  rmydioph  26255  rmxdiophlem  26256  jm3.1  26261  pwssplit3  26338  pwssplit4  26339  frlmup4  26401  enfixsn  26405  mapfien2  26406  islindf2  26432  lindsind2  26437  f1lindf  26440  lindsss  26442  f1linds  26443  lindsmm  26446  lbslcic  26459  hbtlem2  26476  mndvcl  26594  mndvass  26595  mhmvlin  26600  idomrootle  26659  dvconstbi  26699  expgrowth  26700  fmul01lt1lem1  26862  climsuselem1  26881  climsuse  26882  stoweidlem3  26900  stoweidlem16  26913  stoweidlem17  26914  stoweidlem26  26923  stoweidlem34  26931  stoweidlem57  26954  funtpg  27232  fntpg  27233  ftpg  27234  fvpr1g  27235  fvpr2g  27236  f1oun2prg  27241  hashtpg  27279  hashnnn0genn0  27286  hashunx  27294  nbusgra  27377  nbgraf1olem1  27388  nbusgrafi  27395  nb3graprlem1  27397  nb3graprlem2  27398  cusgra2v  27407  cusgra3v  27409  constr1trl  27484  constr2trl  27494  2pthon  27498  constr3lem4  27531  constr3trllem2  27535  constr3trllem5  27538  constr3pthlem2  27540  vdgref  27565  vdgrefinf  27566  vdgrvdgre  27567  vdusgra0nedg  27576  hashnbgravd  27577  3vfriswmgralem  27596  3vfriswmgra  27597  chordthmALT  28221  bnj837  28302  bnj517  28428  bnj553  28441  bnj594  28455  bnj967  28488  bnj1097  28522  bnj1110  28523  bnj1118  28525  bnj1128  28531  bnj1125  28533  bnj1145  28534  bnj1136  28538  bnj1173  28543  bnj1189  28550  bnj1204  28553  bnj1279  28559  bnj1321  28568  bnj1413  28576  lsmsat  29016  lsmsatcv  29018  lsatcvatlem  29057  islshpcv  29061  l1cvpat  29062  lfli  29069  lshpset2N  29127  cvrnbtwn  29279  meetat2  29305  atcmp  29319  atcvreq0  29322  atlatmstc  29327  cvlcvr1  29347  cvlcvrp  29348  cvlatcvr2  29350  cvr2N  29418  cvratlem  29428  2atjm  29452  athgt  29463  2lplnmN  29566  2llnmj  29567  2lplnmj  29629  dalemswapyzps  29697  dalem23  29703  dalem24  29704  dalem25  29705  dalem27  29706  dalem28  29707  dalem38  29717  dalem39  29718  dalem44  29723  dalem45  29724  dalem51  29730  dalem52  29731  dalem56  29735  pmapglbx  29776  pmapjat1  29860  pmapjat2  29861  paddatclN  29956  osumcllem4N  29966  osumcllem7N  29969  ltrncoval  30152  cdleme0aa  30217  cdleme0b  30219  cdleme8  30257  cdlemesner  30303  cdleme22eALTN  30352  cdleme26eALTN  30368  cdleme35h  30463  cdleme50trn2  30558  cdleme  30567  tgrpov  30755  tendotp  30768  tendoidcl  30776  tendo0co2  30795  cdlemkvcl  30849  dvhopvadd  31101  dvhopellsm  31125  dihmeetlem1N  31298  dihmeetlem9N  31323  dihatexv  31346  lcfl7lem  31507  mapdrvallem2  31653  mapdh9a  31798  hdmapevec  31846
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator