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

Theorem trud 1235
Description: Eliminate as an antecedent. A proposition implied by is true. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypothesis
Ref Expression
trud.1 ( ⊤ → φ)
Assertion
Ref Expression
trud φ

Proof of Theorem trud
StepHypRef Expression
1 tru 1230 . 2
2 trud.1 . 2 ( ⊤ → φ)
31, 2ax-mp 7 1 φ
Colors of variables: wff set class
Syntax hints:  wi 4  wtru 1227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-tru 1229
This theorem is referenced by:  nfbi  1457  spime  1605  eubii  1885  nfmo  1896  mobii  1913  dvelimc  2174  ralbii  2302  rexbii  2303  nfralxy  2332  nfrexxy  2333  nfralya  2334  nfrexya  2335  nfreuxy  2456  nfsbc1  2752  nfsbc  2755  sbcbii  2789  csbeq2i  2847  nfcsb1  2852  nfcsb  2855  nfif  3325  ssbri  3772  nfbr  3774  mpteq12i  3811  ralxfr  4139  rexxfr  4141  nfiotaxy  4789  nfriota  5392  nfov  5450  mpt2eq123i  5482  mpt2eq3ia  5484  eqer  6040  0er  6042  ecopover  6106  ecopoverg  6109  ltsopi  6169  ltsonq  6246  enq0er  6279  ltpopr  6421  ltposr  6504  axcnex  6553  ltso  6699  nfneg  6811  xrltso  8260  bj-sbimeh  8433  bdnthALT  8476
  Copyright terms: Public domain W3C validator