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

Theorem 3ad2ant3 980
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 453 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 975 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp3l  985  simp3r  986  simp31  993  simp32  994  simp33  995  simp3ll  1028  simp3lr  1029  simp3rl  1030  simp3rr  1031  simp3l1  1062  simp3l2  1063  simp3l3  1064  simp3r1  1065  simp3r2  1066  simp3r3  1067  simp31l  1080  simp31r  1081  simp32l  1082  simp32r  1083  simp33l  1084  simp33r  1085  simp311  1104  simp312  1105  simp313  1106  simp321  1107  simp322  1108  simp323  1109  simp331  1110  simp332  1111  simp333  1112  3anim123i  1139  3jaao  1251  ceqsalt  2970  ceqsralt  2971  vtoclgft  2994  tpssi  3957  prnebg  3971  epne3  4753  limsuc  4821  poltletr  5261  funprg  5492  funtpg  5493  fntpg  5498  ftpg  5908  fsnunf  5923  fsnunfv  5925  fvpr1g  5929  fvpr2g  5930  fnsuppres  5944  weniso  6067  smoel  6614  smoord  6619  omwordi  6806  oneo  6816  oeord  6823  oewordi  6826  nnmwordi  6870  nnneo  6886  uniinqs  6976  undifixp  7090  domss2  7258  domssex2  7259  unxpdomlem3  7307  dif1enOLD  7332  dif1en  7333  dffi2  7420  unwdomg  7544  ixpiunwdom  7551  oemapvali  7632  en3lplem1  7662  fodomfi2  7933  infcdaabs  8078  infunabs  8079  infdif  8081  ackbij1lem9  8100  ackbij1lem16  8107  coflim  8133  cfsmolem  8142  isfin2-2  8191  fin1a2lem9  8280  hsmexlem2  8299  axcc2lem  8308  axcc3  8310  domtriomlem  8314  axdc3lem4  8325  axcclem  8329  zornn0g  8377  axacndlem4  8477  axacndlem5  8478  axacnd  8479  gchdomtri  8496  fpwwe  8513  tskssel  8624  tskint  8652  tskurn  8656  gruurn  8665  gruixp  8676  grudomon  8684  gruina  8685  adderpqlem  8823  mulerpqlem  8824  addassnq  8827  mulassnq  8828  distrnq  8830  ltsonq  8838  ltanq  8840  ltmnq  8841  reclem3pr  8918  addid2  9241  addcan2  9243  divdir  9693  divcan5  9708  ltdiv1  9866  infmrcl  9979  infmrlb  9981  lt2halves  10194  zdivmul  10334  xaddass  10820  xleadd1  10826  xltadd1  10827  xmulasslem3  10857  xmulass  10858  xlemul1  10861  xlemul2  10862  xltmul1  10863  xadddir  10867  elioo5  10960  iccsupr  10989  iccneg  11010  icoshft  11011  icoshftf1o  11012  iccsplit  11021  fzen  11064  fzrevral  11123  fzshftral  11126  elfzo  11134  modabs  11266  modcyc  11268  moddi  11276  modsubdir  11277  expdiv  11422  leexp2a  11427  bcval3  11589  hashnnn0genn0  11619  hashgadd  11643  hashunx  11652  hashtpg  11683  hashfun  11692  brfi1indlem  11706  ccatval1  11737  ccatval2  11738  ccatval3  11739  ccatass  11742  swrdval2  11759  splval  11772  ccatco  11796  f1oun2prg  11856  swrds2  11872  sqr0  12039  elicc4abs  12115  mulcn2  12381  demoivreALT  12794  rpnnen2lem4  12809  dvdsval2  12847  dvdsexp  12897  mulgcd  13038  mulgcdr  13040  gcddiv  13041  rpmulgcd  13047  rplpwr  13048  prmexpb  13109  rpexp  13112  coprimeprodsq  13175  pythagtriplem1  13182  pythagtriplem3  13184  pythagtriplem10  13186  pythagtriplem6  13187  pythagtriplem11  13191  pythagtriplem12  13192  pythagtriplem13  13193  pythagtriplem15  13195  pythagtriplem17  13197  pythagtriplem19  13199  pcdvdsb  13234  pcfaclem  13259  vdwapun  13334  ramval  13368  0ram2  13381  0ramcl  13383  imasaddvallem  13746  imasvscaval  13755  mreiincl  13813  mremre  13821  mrieqv2d  13856  cofurid  14080  xpcpropd  14297  clatleglb  14545  gsumccat  14779  mulgdirlem  14906  mulgp1  14908  eqglact  14983  mndodcongi  15173  oddvdsnn0  15174  odngen  15203  gexnnod  15214  lsmlub  15289  lsmass  15294  efgsval2  15357  efgsrel  15358  ghmplusg  15453  odadd1  15455  odadd2  15456  gsumsn  15535  dvrcan1  15788  dvrcan3  15789  irredrmul  15804  srngadd  15937  srngmul  15938  lmhmvsca  16113  reslmhm2  16121  lbspss  16146  lsmsp  16150  lspsneu  16187  lidldvgen  16318  psropprmul  16624  coe1add  16649  coe1addfv  16650  coe1subfv  16651  coe1tm  16657  coe1sclmul  16666  coe1sclmul2  16668  cssmre  16912  iuncld  17101  clsss  17110  ntrcls0  17132  iscldtop  17151  neiss  17165  neips  17169  restcldi  17229  cnpnei  17320  cnconst2  17339  cnpresti  17344  sslm  17355  cnt0  17402  cnt1  17406  cnhaus  17410  cncmp  17447  cmpcld  17457  cnconn  17477  concompss  17488  elptr  17597  upxp  17647  qtoptop2  17723  ordthmeolem  17825  opnfbas  17866  isfil2  17880  fbasweak  17889  snfbas  17890  fgss  17897  fgcl  17902  fbasrn  17908  trnei  17916  cfinfil  17917  csdfil  17918  supfil  17919  filufint  17944  fin1aufil  17956  fmval  17967  fmf  17969  elfm  17971  elfm3  17974  imaelfm  17975  rnelfmlem  17976  rnelfm  17977  flimclslem  18008  flfneii  18016  cnpfcfi  18064  alexsubALT  18074  ptcmplem3  18077  ustref  18240  ustelimasn  18244  utop3cls  18273  ressusp  18287  cfiluexsm  18312  prdsxmetlem  18390  txmetcn  18570  nmmtri  18660  nmrtri  18662  unitnmn0  18696  nminvr  18697  nmotri  18765  nghmplusg  18766  isclmi  19094  fmcfil  19217  srabn  19306  itgconst  19702  dvn2bss  19808  evlsval  19932  evlsval2  19933  deg1mul3  20030  deg1mul3le  20031  deg1tmle  20032  q1peqb  20069  r1pcl  20072  r1pdeglt  20073  r1pid  20074  dvdsq1p  20075  dvdsr1p  20076  ptolemy  20396  sincosq1eq  20412  logmul2  20503  logdiv2  20504  cxplt2  20581  pythag  20651  bcmono  21053  efexple  21057  lgsdirnn0  21115  selberglem3  21233  nbgraf1olem1  21443  nbusgrafi  21450  nb3graprlem1  21452  nb3graprlem2  21453  cusgra2v  21463  cusgra3v  21465  2trllemH  21544  2trllemE  21545  constr1trl  21580  constr2spthlem1  21586  2pthlem2  21588  2wlklem1  21589  2pthon  21594  constr3lem4  21626  constr3trllem2  21630  constr3trllem5  21633  constr3pthlem2  21635  vdgrfival  21660  vdgrf  21661  vdgrfif  21662  vdusgra0nedg  21671  hashnbgravd  21673  gxpval  21839  gxnval  21840  gxnn0neg  21843  gxnn0suc  21844  gxneg  21846  gxsuc  21852  gxnn0add  21854  gxadd  21855  gxsub  21856  gxnn0mul  21857  gxmul  21858  gxmodid  21859  gxdi  21876  zerdivemp1  22014  rngoridfz  22015  vcid  22022  vcdi  22023  vcdir  22024  vcass  22025  imsmetlem  22174  0oval  22281  ajval  22355  shlub  22908  hmopco  23518  adjlnop  23581  mdslmd4i  23828  divnumden2  24153  ress0g  24174  ressnm  24176  ofldadd  24230  ofldmul  24231  pstmfval  24283  logeq0im1  24386  ind1  24408  ind0  24409  sigaclcuni  24493  sigagenss2  24525  measun  24557  measvuni  24560  dya2iocnrect  24623  ballotlemieq  24766  ballotlemrv1  24770  lgamgulmlem1  24805  erdszelem2  24870  cnpcon  24909  cvmscld  24952  ghomf1olem  25097  dedekind  25179  prodfrec  25215  ntrivcvgfvn0  25219  iprodefisumlem  25309  binomrisefac  25350  dvdspw  25361  dfon2lem3  25404  dfon2lem7  25408  predeq123  25432  predpo  25451  frrlem4  25577  nofulllem3  25651  brbtwn2  25836  axcgrid  25847  ax5seglem1  25859  ax5seglem2  25860  ax5seg  25869  axpasch  25872  axlowdimlem16  25888  axcontlem7  25901  btwndiff  25953  brcolinear2  25984  btwnconn1  26027  nnssi3  26198  nndivsub  26199  ftc1anclem4  26273  areacirclem4  26284  areacirclem6  26287  areacirc  26288  nn0prpwlem  26316  hmeoclda  26327  hmeocldb  26328  ivthALT  26329  ssref  26354  fnemeet1  26386  fnejoin1  26388  upixp  26422  filbcmb  26433  cnresima  26464  smprngopr  26653  igenval2  26667  ismrcd1  26743  istopclsd  26745  ismrc  26746  mapfzcons  26763  eldioph2  26811  diophrex  26825  diophren  26865  pellexlem1  26883  pellexlem5  26887  pellqrexplicit  26931  reglogmul  26947  reglogexp  26948  rmxycomplete  26971  congmul  27023  congabseq  27030  acongsym  27032  acongneg2  27033  fzneg  27038  acongeq  27039  jm2.19  27055  jm2.22  27057  jm2.23  27058  jm2.20nn  27059  rmydioph  27076  rmxdiophlem  27077  jm3.1  27082  pwssplit3  27158  pwssplit4  27159  frlmup4  27221  enfixsn  27225  mapfien2  27226  islindf2  27252  lindsind2  27257  f1lindf  27260  lindsss  27262  f1linds  27263  lindsmm  27266  lbslcic  27279  hbtlem2  27296  mndvcl  27414  mndvass  27415  mhmvlin  27420  idomrootle  27479  dvconstbi  27519  expgrowth  27520  fmul01lt1lem1  27681  climsuselem1  27700  climsuse  27701  stoweidlem3  27719  stoweidlem16  27732  stoweidlem17  27733  stoweidlem26  27742  stoweidlem34  27750  stoweidlem57  27773  el2xptp0  28051  oteqimp  28053  otthg  28054  2leaddle2  28077  ssfz12  28088  elfzelfzelfz  28093  elfz0fzfz0  28098  fz0fzelfz0  28102  fz0fzdiffz0  28103  ltdifltdiv  28126  modaddmulmod  28136  ccatsymb  28152  swrd0swrd  28163  swrdswrdlem  28164  swrdswrd  28165  swrdccatin12lem3  28178  swrdccat3b  28185  modprm0  28194  cshwleneq  28231  3cshw  28232  cshweqdif2  28233  cshweqdif2s  28234  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  el2wlkonotot0  28292  3vfriswmgralem  28331  3vfriswmgra  28332  2spotdisj  28387  usg2spot2nb  28391  chordthmALT  28982  bnj837  29067  bnj517  29193  bnj553  29206  bnj594  29220  bnj967  29253  bnj1097  29287  bnj1110  29288  bnj1118  29290  bnj1128  29296  bnj1125  29298  bnj1145  29299  bnj1136  29303  bnj1173  29308  bnj1189  29315  bnj1204  29318  bnj1279  29324  bnj1321  29333  bnj1413  29341  lsmsat  29743  lsmsatcv  29745  lsatcvatlem  29784  islshpcv  29788  l1cvpat  29789  lfli  29796  lshpset2N  29854  cvrnbtwn  30006  meetat2  30032  atcmp  30046  atcvreq0  30049  atlatmstc  30054  cvlcvr1  30074  cvlcvrp  30075  cvlatcvr2  30077  cvr2N  30145  cvratlem  30155  2atjm  30179  athgt  30190  2lplnmN  30293  2llnmj  30294  2lplnmj  30356  dalemswapyzps  30424  dalem23  30430  dalem24  30431  dalem25  30432  dalem27  30433  dalem28  30434  dalem38  30444  dalem39  30445  dalem44  30450  dalem45  30451  dalem51  30457  dalem52  30458  dalem56  30462  pmapglbx  30503  pmapjat1  30587  pmapjat2  30588  paddatclN  30683  osumcllem4N  30693  osumcllem7N  30696  ltrncoval  30879  cdleme0aa  30944  cdleme0b  30946  cdleme8  30984  cdlemesner  31030  cdleme22eALTN  31079  cdleme26eALTN  31095  cdleme35h  31190  cdleme50trn2  31285  cdleme  31294  tgrpov  31482  tendotp  31495  tendoidcl  31503  tendo0co2  31522  cdlemkvcl  31576  dvhopvadd  31828  dvhopellsm  31852  dihmeetlem1N  32025  dihmeetlem9N  32050  dihatexv  32073  lcfl7lem  32234  mapdrvallem2  32380  mapdh9a  32525  hdmapevec  32573
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator