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  areacirclem4  26274  areacirclem6  26277  areacirc  26278  nn0prpwlem  26306  hmeoclda  26317  hmeocldb  26318  ivthALT  26319  ssref  26344  fnemeet1  26376  fnejoin1  26378  upixp  26412  filbcmb  26423  cnresima  26454  smprngopr  26643  igenval2  26657  ismrcd1  26733  istopclsd  26735  ismrc  26736  mapfzcons  26753  eldioph2  26801  diophrex  26815  diophren  26855  pellexlem1  26873  pellexlem5  26877  pellqrexplicit  26921  reglogmul  26937  reglogexp  26938  rmxycomplete  26961  congmul  27013  congabseq  27020  acongsym  27022  acongneg2  27023  fzneg  27028  acongeq  27029  jm2.19  27045  jm2.22  27047  jm2.23  27048  jm2.20nn  27049  rmydioph  27066  rmxdiophlem  27067  jm3.1  27072  pwssplit3  27148  pwssplit4  27149  frlmup4  27211  enfixsn  27215  mapfien2  27216  islindf2  27242  lindsind2  27247  f1lindf  27250  lindsss  27252  f1linds  27253  lindsmm  27256  lbslcic  27269  hbtlem2  27286  mndvcl  27404  mndvass  27405  mhmvlin  27410  idomrootle  27469  dvconstbi  27509  expgrowth  27510  fmul01lt1lem1  27671  climsuselem1  27690  climsuse  27691  stoweidlem3  27709  stoweidlem16  27722  stoweidlem17  27723  stoweidlem26  27732  stoweidlem34  27740  stoweidlem57  27763  el2xptp0  28041  oteqimp  28043  otthg  28044  2leaddle2  28067  ssfz12  28078  elfzelfzelfz  28083  elfz0fzfz0  28088  fz0fzelfz0  28092  fz0fzdiffz0  28093  ltdifltdiv  28116  modaddmulmod  28126  ccatsymb  28142  swrd0swrd  28153  swrdswrdlem  28154  swrdswrd  28155  swrdccatin12lem3  28168  swrdccat3b  28175  modprm0  28184  cshwleneq  28221  3cshw  28222  cshweqdif2  28223  cshweqdif2s  28224  usgra2pth  28254  el2wlkonot  28279  el2spthonot  28280  el2spthonot0  28281  el2wlkonotot0  28282  3vfriswmgralem  28321  3vfriswmgra  28322  2spotdisj  28377  usg2spot2nb  28381  chordthmALT  28972  bnj837  29057  bnj517  29183  bnj553  29196  bnj594  29210  bnj967  29243  bnj1097  29277  bnj1110  29278  bnj1118  29280  bnj1128  29286  bnj1125  29288  bnj1145  29289  bnj1136  29293  bnj1173  29298  bnj1189  29305  bnj1204  29308  bnj1279  29314  bnj1321  29323  bnj1413  29331  lsmsat  29733  lsmsatcv  29735  lsatcvatlem  29774  islshpcv  29778  l1cvpat  29779  lfli  29786  lshpset2N  29844  cvrnbtwn  29996  meetat2  30022  atcmp  30036  atcvreq0  30039  atlatmstc  30044  cvlcvr1  30064  cvlcvrp  30065  cvlatcvr2  30067  cvr2N  30135  cvratlem  30145  2atjm  30169  athgt  30180  2lplnmN  30283  2llnmj  30284  2lplnmj  30346  dalemswapyzps  30414  dalem23  30420  dalem24  30421  dalem25  30422  dalem27  30423  dalem28  30424  dalem38  30434  dalem39  30435  dalem44  30440  dalem45  30441  dalem51  30447  dalem52  30448  dalem56  30452  pmapglbx  30493  pmapjat1  30577  pmapjat2  30578  paddatclN  30673  osumcllem4N  30683  osumcllem7N  30686  ltrncoval  30869  cdleme0aa  30934  cdleme0b  30936  cdleme8  30974  cdlemesner  31020  cdleme22eALTN  31069  cdleme26eALTN  31085  cdleme35h  31180  cdleme50trn2  31275  cdleme  31284  tgrpov  31472  tendotp  31485  tendoidcl  31493  tendo0co2  31512  cdlemkvcl  31566  dvhopvadd  31818  dvhopellsm  31842  dihmeetlem1N  32015  dihmeetlem9N  32040  dihatexv  32063  lcfl7lem  32224  mapdrvallem2  32370  mapdh9a  32515  hdmapevec  32563
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