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

Theorem 3adant3r3 1207
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3adant3r3

Proof of Theorem 3adant3r3
StepHypRef Expression
1 3exp.1 . . 3
213expb 1197 . 2
323adantr3 1157 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  ressress  14694  plttr  15600  plelttr  15602  latledi  15719  latmlej11  15720  latmlej21  15722  latmlej22  15723  latjass  15725  latj12  15726  latj31  15729  ipopos  15790  latdisdlem  15819  imasmnd2  15957  imasmnd  15958  grpaddsubass  16128  grpsubsub4  16131  grpnpncan  16133  imasgrp2  16185  imasgrp  16186  frgp0  16778  cmn12  16818  abladdsub  16825  imasring  17268  dvrass  17339  lss1  17585  islmhm2  17684  psrgrp  18051  psrlmod  18054  zntoslem  18595  ipdir  18674  t1sep  19871  mettri2  20844  xmetrtri  20858  xmetrtri2  20859  pi1grplem  21549  dchrabl  23529  motgrp  23930  xmstrkgc  24189  ax5seglem4  24235  grpomuldivass  25251  grpopnpcan2  25255  grponpncan  25257  grpodiveq  25258  ablomuldiv  25291  ablodivdiv4  25293  nvadd12  25516  nvmdi  25545  nvsubadd  25550  nvmtri2  25575  dipdi  25758  dipsubdir  25763  dipsubdi  25764  cgr3tr4  29702  cgr3rflx  29704  seglemin  29763  linerflx1  29799  elicc3  30135  rngosubdi  30356  rngosubdir  30357  igenval2  30463  dmncan1  30473  mendlmod  31142  lincsumscmcl  33034  latmassOLD  34954  omlfh1N  34983  omlfh3N  34984  cvrnbtwn  34996  cvrnbtwn2  35000  cvrnbtwn4  35004  hlatj12  35095  cvrntr  35149  islpln2a  35272  3atnelvolN  35310  elpadd2at2  35531  paddasslem17  35560  paddass  35562  paddssw2  35568  pmapjlln1  35579  ltrn2ateq  35905  cdlemc3  35918  cdleme1b  35951  cdleme3b  35954  cdleme3c  35955  cdleme9b  35977  erngdvlem3  36716  erngdvlem3-rN  36724  dvalveclem  36752
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator