ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  trud Unicode version

Theorem trud 1268
Description: Eliminate T. as an antecedent. A proposition implied by T. is true. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
trud.1  |-  ( T. 
->  ph )
Assertion
Ref Expression
trud  |-  ph

Proof of Theorem trud
StepHypRef Expression
1 tru 1263 . 2  |- T.
2 trud.1 . 2  |-  ( T. 
->  ph )
31, 2ax-mp 7 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   T. wtru 1260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-tru 1262
This theorem is referenced by:  xorbi12i  1290  nfbi  1497  spime  1645  eubii  1925  nfmo  1936  mobii  1953  dvelimc  2214  ralbii  2347  rexbii  2348  nfralxy  2377  nfrexxy  2378  nfralya  2379  nfrexya  2380  nfreuxy  2501  nfsbc1  2804  nfsbc  2807  sbcbii  2845  csbeq2i  2904  nfcsb1  2909  nfcsb  2912  nfif  3384  ssbri  3834  nfbr  3836  mpteq12i  3873  ralxfr  4226  rexxfr  4228  nfiotaxy  4899  nfriota  5505  nfov  5563  mpt2eq123i  5596  mpt2eq3ia  5598  tfri1  5982  eqer  6169  0er  6171  ecopover  6235  ecopoverg  6238  en2i  6281  en3i  6282  ener  6290  ensymb  6291  entr  6295  ltsopi  6476  ltsonq  6554  enq0er  6591  ltpopr  6751  ltposr  6906  axcnex  6993  ltso  7155  nfneg  7271  xrltso  8818  frecfzennn  9367  frechashgf1o  9369  facnn  9595  fac0  9596  fac1  9597  cnrecnv  9738  cau3  9942  oddpwdc  10262  bj-sbimeh  10299  bdnthALT  10342
  Copyright terms: Public domain W3C validator