Theorem trud 1296

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

Step	Hyp	Ref	Expression
1		tru 1291	. 2 ⊢ ⊤
2		trud.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 7	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1288

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-tru 1290

This theorem is referenced by:  xorbi12i  1317  nfbi  1524  spime  1673  eubii  1954  nfmo  1965  mobii  1982  dvelimc  2245  ralbii  2380  rexbii  2381  nfralxy  2410  nfrexxy  2411  nfralya  2412  nfrexya  2413  nfreuxy  2537  nfsbc1  2846  nfsbc  2849  sbcbii  2887  csbeq2i  2946  nfcsb1  2951  nfcsb  2954  nfif  3405  ssbri  3862  nfbr  3864  mpteq12i  3901  ralxfr  4261  rexxfr  4263  nfiotaxy  4947  nfriota  5572  nfov  5630  mpt2eq123i  5663  mpt2eq3ia  5665  tfri1  6078  eqer  6270  0er  6272  ecopover  6336  ecopoverg  6339  en2i  6433  en3i  6434  ener  6442  ensymb  6443  entr  6447  djuf1olem  6682  ltsopi  6816  ltsonq  6894  enq0er  6931  ltpopr  7091  ltposr  7246  axcnex  7333  ltso  7500  nfneg  7616  negiso  8344  xrltso  9191  frecfzennn  9754  frechashgf1o  9756  0tonninf  9766  1tonninf  9767  facnn  10024  fac0  10025  fac1  10026  cnrecnv  10232  cau3  10436  sum0  10659  oddpwdc  11019  bj-sbimeh  11103  bdnthALT  11156