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

Theorem trud 1252
 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 1247 . 2
2 trud.1 . 2 (⊤ → 𝜑)
31, 2ax-mp 7 1 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4  ⊤wtru 1244 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 1246 This theorem is referenced by:  xorbi12i  1274  nfbi  1481  spime  1629  eubii  1909  nfmo  1920  mobii  1937  dvelimc  2198  ralbii  2330  rexbii  2331  nfralxy  2360  nfrexxy  2361  nfralya  2362  nfrexya  2363  nfreuxy  2484  nfsbc1  2781  nfsbc  2784  sbcbii  2818  csbeq2i  2876  nfcsb1  2881  nfcsb  2884  nfif  3356  ssbri  3806  nfbr  3808  mpteq12i  3845  ralxfr  4198  rexxfr  4200  nfiotaxy  4871  nfriota  5477  nfov  5535  mpt2eq123i  5568  mpt2eq3ia  5570  tfri1  5951  eqer  6138  0er  6140  ecopover  6204  ecopoverg  6207  en2i  6250  en3i  6251  ener  6259  ensymb  6260  entr  6264  ltsopi  6418  ltsonq  6496  enq0er  6533  ltpopr  6693  ltposr  6848  axcnex  6935  ltso  7096  nfneg  7208  xrltso  8717  frecfzennn  9203  frechashgf1o  9205  cnrecnv  9510  cau3  9711  bj-sbimeh  9912  bdnthALT  9955
 Copyright terms: Public domain W3C validator