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

Theorem trud 1237
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 1232 . 2
2 trud.1 . 2 ( ⊤ → φ)
31, 2ax-mp 7 1 φ
Colors of variables: wff set class
Syntax hints:  wi 4  wtru 1229
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 1231
This theorem is referenced by:  nfbi  1463  spime  1611  eubii  1891  nfmo  1902  mobii  1919  dvelimc  2180  ralbii  2308  rexbii  2309  nfralxy  2338  nfrexxy  2339  nfralya  2340  nfrexya  2341  nfreuxy  2462  nfsbc1  2758  nfsbc  2761  sbcbii  2795  csbeq2i  2853  nfcsb1  2858  nfcsb  2861  nfif  3333  ssbri  3780  nfbr  3782  mpteq12i  3819  ralxfr  4148  rexxfr  4150  nfiotaxy  4798  nfriota  5401  nfov  5459  mpt2eq123i  5491  mpt2eq3ia  5493  eqer  6049  0er  6051  ecopover  6115  ecopoverg  6118  ltsopi  6180  ltsonq  6257  enq0er  6290  ltpopr  6432  ltposr  6510  axcnex  6555  ltso  6696  nfneg  6801  bj-sbimeh  7166  bdnthALT  7209
  Copyright terms: Public domain W3C validator