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

Theorem 3adant1l 1220
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1
Assertion
Ref Expression
3adant1l

Proof of Theorem 3adant1l
StepHypRef Expression
1 3adant1l.1 . . . 4
213expb 1197 . . 3
32adantll 713 . 2
433impb 1192 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3adant2l  1222  3adant3l  1224  cfsmolem  8671  axdc3lem4  8854  issubmnd  15948  maducoeval2  19142  cramerlem3  19191  restnlly  19983  efgh  22928  hasheuni  28091  pellex  30771  mendlmod  31142  ssfiunibd  31509  mullimc  31622  mullimcf  31629  limclner  31657
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