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

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

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