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

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

Proof of Theorem 3adant3r2
StepHypRef Expression
1 3exp.1 . . 3
213expb 1197 . 2
323adantr2 1156 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  plttr  15600  latjlej2  15696  latmlem1  15711  latmlem2  15712  latledi  15719  latmlej11  15720  latmlej12  15721  ipopos  15790  grppnpcan2  16132  mulgsubdir  16173  imasring  17268  zntoslem  18595  mettri2  20844  mettri  20855  xmetrtri  20858  xmetrtri2  20859  metrtri  20860  grpopnpcan2  25255  grponnncan2  25256  ablomuldiv  25291  ablonnncan1  25297  nvmdi  25545  dipdi  25758  dipassr  25761  dipsubdir  25763  dipsubdi  25764  btwncomim  29663  cgr3tr4  29702  cgr3rflx  29704  colinbtwnle  29768  rngosubdi  30356  rngosubdir  30357  dmncan1  30473  dmncan2  30474  mendlmod  31142  omlfh1N  34983  omlfh3N  34984  cvrnbtwn3  35001  cvrnbtwn4  35004  cvrcmp2  35009  hlatjrot  35097  cvrat3  35166  lplnribN  35275  ltrn2ateq  35905  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