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

Theorem 3ad2ant2 979
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant2  |-  ( ( ps  /\  ph  /\  th )  ->  ch )

Proof of Theorem 3ad2ant2
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantr 452 . 2  |-  ( (
ph  /\  th )  ->  ch )
323adant1 975 1  |-  ( ( ps  /\  ph  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp2l  983  simp2r  984  simp21  990  simp22  991  simp23  992  simp2ll  1024  simp2lr  1025  simp2rl  1026  simp2rr  1027  simp2l1  1056  simp2l2  1057  simp2l3  1058  simp2r1  1059  simp2r2  1060  simp2r3  1061  simp21l  1074  simp21r  1075  simp22l  1076  simp22r  1077  simp23l  1078  simp23r  1079  simp211  1095  simp212  1096  simp213  1097  simp221  1098  simp222  1099  simp223  1100  simp231  1101  simp232  1102  simp233  1103  3anim123i  1139  3jaao  1251  ceqsalt  2922  vtoclgft  2946  vtoclegft  2967  epne3  4702  sofld  5259  funtpg  5442  fnprg  5446  fntpg  5447  fnco  5494  fvun1  5734  fsnunf2  5872  oprssov  6155  sorpssuni  6468  sorpssint  6469  onfununi  6540  onoviun  6542  smogt  6566  omass  6760  f1dom2g  7062  domunfican  7316  inelfi  7359  dffi2  7364  ordiso2  7418  wemapso  7454  unwdomg  7486  wdomima2g  7488  ixpiunwdom  7493  cantnfres  7567  dif1card  7826  ackbij1lem9  8042  ackbij1lem16  8049  cfflb  8073  coflim  8075  cfsmolem  8084  fincssdom  8137  isf32lem11  8177  domtriomlem  8256  axdc4lem  8269  ac6num  8293  axacndlem4  8419  axacndlem5  8420  axacnd  8421  elwina  8495  elina  8496  winaon  8497  inawina  8499  winacard  8501  winainflem  8502  tsksuc  8571  tskuni  8592  grupr  8606  nqereu  8740  enqeq  8745  nqereq  8746  adderpqlem  8765  mulerpqlem  8766  addassnq  8769  mulassnq  8770  distrnq  8772  ltsonq  8780  ltanq  8782  ltmnq  8783  div2neg  9670  lediv2  9833  nndivtr  9974  zdivmul  10275  gtndiv  10280  fzind  10301  eluzp1p1  10444  peano2uz  10463  xrre2  10691  xaddass  10761  xlt2add  10772  xmulasslem3  10798  xmulass  10799  supxrun  10827  icc0  10897  ubioc1  10898  ubicc2  10947  iccsplit  10962  elfzo0  11102  modabs  11202  modcyc  11204  moddi  11212  modsubdir  11213  expneg2  11318  expnbnd  11436  digit2  11440  hashnnn0genn0  11555  hashgadd  11579  hashinfxadd  11587  hashgt12el2  11611  hashfun  11628  brfi1indlem  11642  ccatval3  11675  ccatass  11678  swrd00  11693  swrdval2  11695  swrdlen  11698  ccatopth  11704  ccatopth2  11705  ccatco  11732  f1oun2prg  11792  swrds2  11808  rediv  11864  imdiv  11871  resqrex  11984  resqrcl  11987  limsupgle  12199  climuni  12274  mulcn2  12317  iseraltlem3  12405  rpnnen2lem7  12748  divalglem8  12848  ndvdssub  12855  bitsfzo  12875  mulgcd  12974  mulgcdr  12976  gcddiv  12977  rplpwr  12984  rppwr  12985  qredeq  13034  pythagtriplem1  13118  pythagtriplem3  13120  pythagtriplem10  13122  pythagtriplem6  13123  pythagtriplem7  13124  pythagtriplem11  13127  pythagtriplem12  13128  pythagtriplem13  13129  pythagtriplem14  13130  pythagtriplem16  13132  pythagtriplem19  13135  pythagtrip  13136  pcfaclem  13195  pcbc  13197  vdwapun  13270  vdwapid1  13271  imasaddvallem  13682  ismre  13743  mreincl  13752  submre  13758  mrcss  13769  comfeq  13860  cofurid  14016  xpcpropd  14233  issubmnd  14652  frmdup3  14739  cycsubg2cl  14906  ghmnsgima  14957  mndodcongi  15109  oddvdsnn0  15110  oddvds  15113  odeq  15116  odmulg2  15119  odmulg  15120  odhash2  15137  odhash3  15138  gexnnod  15150  gexcl2  15151  isslw  15170  subgslw  15178  oppglsm  15204  lsmsubm  15215  lsmless1  15221  lsmless2  15222  lsmass  15230  efgsval2  15293  efgsrel  15294  efgsfo  15299  ghmplusg  15389  odadd1  15391  odadd2  15392  gsumconst  15460  gsumsn  15471  ablfac1eu  15559  pgpfac1lem5  15565  ablfaclem3  15573  rngidss  15618  irredrmul  15740  abvres  15855  srngadd  15873  srngmul  15874  lssincl  15969  lsslsp  16019  reslmhm2b  16058  lsmsp  16086  sralmod  16186  aspid  16317  asclmul1  16326  asclmul2  16327  coe1add  16585  coe1addfv  16586  coe1subfv  16587  ntrin  17049  elnei  17099  restco  17151  restcldi  17160  sslm  17286  cnt1  17337  cmpsublem  17385  cmpcld  17388  kgen2ss  17509  upxp  17577  xkopjcn  17610  xkococnlem  17613  xkococn  17614  qtopval2  17650  qtoptop2  17653  ordthmeolem  17755  isfil2  17810  fgss  17827  fbasrn  17838  ufilmax  17861  filufint  17874  fmval  17897  elfm2  17902  elfm3  17904  rnelfmlem  17906  rnelfm  17907  flimrest  17937  flfnei  17945  isflf  17947  flffbas  17949  fclsrest  17978  cnpfcfi  17994  alexsubALTlem4  18003  subgntr  18058  opnsubg  18059  tgpconcompss  18065  divstgpopn  18071  divstgphaus  18074  utopsnnei  18201  blres  18352  metcnp3  18461  blval2  18483  xmsusp  18489  nmmtri  18540  nmrtri  18542  nminvr  18577  nmotri  18645  nghmplusg  18646  tgqioo  18703  iccpnfhmeo  18842  caun0  19106  cmetcusp1  19175  pjth  19208  volsup2  19365  itg2le  19499  dvn2bss  19684  evlsval2  19809  mdegldg  19857  mdegnn0cl  19862  deg1ldgdomn  19885  deg1mul3  19906  drnguc1p  19961  ig1peu  19962  ig1pdvds  19967  coeid3  20027  coe11  20039  dgradd2  20054  facth  20091  dvtaylp  20154  pserdvlem2  20212  ptolemy  20272  tanord1  20307  cxple2  20456  cxpeq  20509  isosctrlem2  20531  muval1  20784  dvdssqf  20789  chpwordi  20808  efchtdvds  20810  logfacbnd3  20875  bcmono  20929  efexple  20933  lgslem1  20948  lgsneg  20971  lgssq2  20988  lgsdirnn0  20991  dchrmusumlema  21055  selberglem3  21109  pntrmax  21126  padicabv  21192  usgra2edg  21269  fiusgraedgfi  21288  nbgraf1olem3  21320  nb3graprlem1  21327  nb3graprlem2  21328  nb3grapr  21329  cusgra2v  21338  cusgra3v  21340  cusgrasizeinds  21352  iswlkon  21396  istrlon  21406  ispthon  21431  constr1trl  21437  constr2trl  21447  constr2pth  21450  2pthon  21451  constr3lem4  21483  constr3trllem2  21487  constr3trllem5  21490  constr3pthlem2  21492  constr3cyclp  21498  vdusgra0nedg  21528  gxmodid  21716  resgrprn  21717  ghomid  21802  nvsge0  22001  nmoub2i  22124  isblo3i  22151  dipassr2  22197  bcs2  22533  elspansn2  22918  fh2  22970  pjoi0  23068  homco2  23329  leopmul  23486  cdj3lem2  23787  rexdiv  24011  ofldadd  24065  ofldmul  24066  unitdivcld  24104  nmmulg  24154  relogbcl  24199  sigaclcuni  24298  volss  24378  volfiniune  24381  dya2iocnrect  24426  probun  24457  cndprobtot  24474  ballotlemsgt1  24548  ballotlemieq  24554  ballotlemfrcn0  24567  cnpcon  24697  cvmsf1o  24739  cvmscld  24740  cvmlift2lem6  24775  ghomfo  24882  modaddabs  24895  fzp1nel  24990  prodfn0  25002  prodfrec  25003  dfrdg2  25177  frrlem5e  25314  nobndlem8  25378  nofulllem2  25382  brbtwn2  25559  ax5seglem2  25583  ax5seglem3  25585  axlowdim  25615  axcontlem7  25624  axcontlem8  25625  fvtransport  25681  nndivsub  25922  itg2addnclem  25958  itg2addnc  25960  nn0prpwlem  26017  nn0prpw  26018  ivthALT  26030  fness  26054  topmeet  26085  fnejoin1  26089  f1ocan1fv  26120  f1ocan2fv  26121  upixp  26123  filbcmb  26134  mettrifi  26155  rngohom0  26280  rngohomsub  26281  rngokerinj  26283  intidl  26331  keridl  26334  nacsfix  26458  mapco2g  26461  mapfzcons  26464  mzpexpmpt  26494  mzpsubst  26497  mzpresrename  26499  coeq0i  26503  eldioph2lem1  26510  lzunuz  26518  diophren  26566  pellexlem1  26584  pell14qrexpclnn0  26621  pellqrexplicit  26632  reglogcl  26645  reglogmul  26648  reglogexp  26649  rmxycomplete  26672  monotuz  26696  zindbi  26701  rmxypos  26704  jm2.17a  26717  congtr  26722  congmul  26724  congabseq  26731  acongsym  26733  acongrep  26737  fzneg  26739  acongeq  26740  dvdsabsmod0  26749  jm2.19  26756  jm2.20nn  26760  jm2.15nn0  26766  rmydioph  26777  rmxdiophlem  26778  jm3.1  26783  rpnnen3lem  26794  aomclem2  26822  islssfgi  26840  pwssplit4  26861  uvcval  26904  mapfien2  26928  lindsind2  26959  f1lindf  26962  lindsss  26964  f1linds  26965  lsslindf  26970  lsslinds  26971  islindf4  26978  lbslcic  26981  hbtlem1  26997  hbtlem2  26998  hbtlem5  27002  cnsrexpcl  27040  mndvcl  27116  mndvass  27117  mhmvlin  27122  hashgcdlem  27186  fnchoice  27369  fmul01lt1lem1  27383  climsuselem1  27402  climsuse  27403  stoweidlem10  27428  stoweidlem14  27432  stoweidlem16  27434  stoweidlem17  27435  stoweidlem20  27438  stoweidlem44  27462  stoweidlem57  27475  stoweidlem60  27478  wallispilem3  27485  3vfriswmgra  27759  3cyclfrgrarn2  27768  n4cyclfrgra  27772  4cyclusnfrgra  27773  vdn0frgrav2  27778  vdn1frgrav2  27780  tratrb  27964  chordthmALT  28388  bnj240  28402  bnj836  28468  bnj545  28605  bnj600  28629  bnj966  28654  bnj967  28655  bnj1097  28689  bnj1118  28692  bnj1128  28698  bnj1204  28720  bnj1321  28735  bnj1408  28744  bnj1514  28771  lsmsat  29124  lcv1  29157  lub0N  29305  glb0N  29309  atcmp  29427  atnle  29433  cvlatcvr2  29458  hlsupr2  29502  cvrval3  29528  atcvr0eq  29541  2atlt  29554  llnnleat  29628  llnle  29633  llncmp  29637  2llnmat  29639  lplnle  29655  2lplnmN  29674  2llnmj  29675  lplncmp  29677  lvolcmp  29732  2lplnmj  29737  pmapmeet  29888  2lnat  29899  elpadd2at  29921  pclssN  30009  lhp0lt  30118  lhpj1  30137  lhpmcvr5N  30142  lhpmcvr6N  30143  ltrneq  30264  cdleme0aa  30325  cdleme10  30369  cdleme27a  30482  cdleme32fva  30552  cdleme42b  30593  cdlemf1  30676  cdlemg35  30828  tendovalco  30880  tendoidcl  30884  tendo0co2  30903  cdleml7  31097  dvhopvadd  31209  dvhopellsm  31233  dihmeetcN  31418  dihmeet  31459  mapdrvallem2  31761  mapdpglem32  31821
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