NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3adant1 Unicode version

Theorem 3adant1 973
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1
Assertion
Ref Expression
3adant1

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 954 . 2
2 3adant.1 . 2
31, 2syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358   w3a 934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
This theorem is referenced by:  3ad2ant2  977  3ad2ant3  978  rsp2e  2677  sbciegft  3076  otkelins2kg  4253  otkelins3kg  4254  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  ltfintr  4459  ncfinlower  4483  tfin11  4493  sfindbl  4530  vfinncvntnn  4548  fununiq  5517  mpt2eq3ia  5670  clos1basesuc  5882  enadj  6060  lectr  6211  leltctr  6212  lecponc  6213  taddc  6229  letc  6231  ce2le  6233  addcdi  6250  addcdir  6251  ncslemuc  6255  nchoicelem17  6305
  Copyright terms: Public domain W3C validator