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

Theorem trud 1323
Description: Eliminate as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
trud.1
Assertion
Ref Expression
trud

Proof of Theorem trud
StepHypRef Expression
1 tru 1321 . 2
2 trud.1 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wtru 1316
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 177  df-tru 1319
This theorem is referenced by:  hadbi123i  1384  cadbi123i  1385  nfn  1793  nfimOLD  1814  nfan  1824  nfbi  1834  nfnfOLD  1846  sbie  2038  eubii  2213  nfeu  2220  nfmo  2221  mobii  2240  dvelimc  2510  ralbii  2638  rexbii  2639  nfral  2667  nfreu  2785  nfrmo  2786  nfrab  2792  nfsbc1  3064  nfsbc  3067  sbcbii  3101  csbeq2i  3162  nfcsb1  3167  nfcsb  3170  nfif  3686  nfiota  4343  nfbr  4683  nfov  5545  mpt2eq123i  5664  mpteq12i  5665  mpt2eq3ia  5670  ider  5943  ssetpov  5944  eqer  5961  ener  6039  lecponc  6213
  Copyright terms: Public domain W3C validator