Theorem trud 1294

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 1289	. 2 ⊢ ⊤
2		trud.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 7	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1286

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 1288

This theorem is referenced by:  xorbi12i  1315  nfbi  1522  spime  1670  eubii  1951  nfmo  1962  mobii  1979  dvelimc  2240  ralbii  2373  rexbii  2374  nfralxy  2403  nfrexxy  2404  nfralya  2405  nfrexya  2406  nfreuxy  2529  nfsbc1  2833  nfsbc  2836  sbcbii  2874  csbeq2i  2933  nfcsb1  2938  nfcsb  2941  nfif  3385  ssbri  3835  nfbr  3837  mpteq12i  3874  ralxfr  4224  rexxfr  4226  nfiotaxy  4901  nfriota  5508  nfov  5566  mpt2eq123i  5599  mpt2eq3ia  5601  tfri1  6014  eqer  6204  0er  6206  ecopover  6270  ecopoverg  6273  en2i  6317  en3i  6318  ener  6326  ensymb  6327  entr  6331  ltsopi  6572  ltsonq  6650  enq0er  6687  ltpopr  6847  ltposr  7002  axcnex  7089  ltso  7256  nfneg  7372  negiso  8100  xrltso  8947  frecfzennn  9508  frechashgf1o  9510  facnn  9751  fac0  9752  fac1  9753  cnrecnv  9935  cau3  10139  oddpwdc  10696  bj-sbimeh  10734  bdnthALT  10784