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

Theorem 3adantr1 1155
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
Hypothesis
Ref Expression
3adantr.1
Assertion
Ref Expression
3adantr1

Proof of Theorem 3adantr1
StepHypRef Expression
1 3simpc 995 . 2
2 3adantr.1 . 2
31, 2sylan2 474 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3ad2antr3  1163  3adant3r1  1205  swopo  4815  omeulem1  7250  divmuldiv  10269  imasmnd2  15957  imasgrp2  16185  srgbinomlem2  17192  imasring  17268  abvdiv  17486  mdetunilem9  19122  lly1stc  19997  icccvx  21450  dchrpt  23542  vcsubdir  25449  dipsubdir  25763  fdc  30238  unichnidl  30428  dmncan1  30473  pexmidlem6N  35699  erngdvlem3  36716  erngdvlem3-rN  36724  dvalveclem  36752  dvhvaddass  36824  dvhlveclem  36835
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