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

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

Proof of Theorem 3adant3r1
StepHypRef Expression
1 3exp.1 . . 3
213expb 1197 . 2
323adantr1 1155 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  plttr  15600  pltletr  15601  latjlej1  15695  latjlej2  15696  latnlej  15698  latnlej2  15701  latmlem2  15712  latledi  15719  latjass  15725  latj32  15727  latj13  15728  ipopos  15790  tsrlemax  15850  imasmnd2  15957  grpsubsub  16127  grpnnncan2  16135  mulgnn0ass  16171  mulgsubdir  16173  imasgrp2  16185  cmn32  16816  ablsubadd  16822  imasring  17268  zntoslem  18595  xmettri3  20856  mettri3  20857  xmetrtri  20858  xmetrtri2  20859  metrtri  20860  cphdivcl  21629  cphassr  21658  grpodivdiv  25250  grpomuldivass  25251  grpopnpcan2  25255  grponnncan2  25256  ablo32  25288  ablodivdiv4  25293  ablodiv32  25294  ablonnncan  25295  nvmdi  25545  nvsubsub23  25557  nvmtri2  25575  dipdi  25758  dipassr  25761  dipsubdir  25763  dipsubdi  25764  dvrcan5  27783  cgr3tr4  29702  cgr3rflx  29704  endofsegid  29735  seglemin  29763  broutsideof2  29772  rngosubdi  30356  rngosubdir  30357  isdrngo2  30361  crngm23  30399  dmncan2  30474  mendlmod  31142  latmassOLD  34954  latm32  34956  cvrnbtwn4  35004  cvrcmp2  35009  ltcvrntr  35148  atcvrj0  35152  3dim3  35193  paddasslem17  35560  paddass  35562  lautlt  35815  lautcvr  35816  lautj  35817  lautm  35818  erngdvlem3  36716  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