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

Theorem 3adantl1 1152
 Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1
Assertion
Ref Expression
3adantl1

Proof of Theorem 3adantl1
StepHypRef Expression
1 3simpc 995 . 2
2 3adantl.1 . 2
31, 2sylan 471 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973 This theorem is referenced by:  3ad2antl2  1159  3ad2antl3  1160  onfununi  7031  omord2  7235  en2eqpr  8406  divmuldiv  10269  ioojoin  11680  expnlbnd  12296  swrdlend  12656  pospropd  15764  marrepcl  19066  gsummatr01lem3  19159  upxp  20124  rnelfmlem  20453  brbtwn2  24208  fh2  26537  homulass  26721  hoadddi  26722  hoadddir  26723  metf1o  30248  rngohomco  30377  rngoisoco  30385  lcmledvds  31205  elaa2  32017  op01dm  34908  paddss12  35543 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