Theorem trud 1323

Description: Eliminate ⊤ as an antecedent. (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 1321	. 2 ⊢ ⊤
2		trud.1	. 2 ⊢ ( ⊤ → φ)
3	1, 2	ax-mp 5	1 ⊢ φ

Syntax hints:   → wi 4   ⊤ wtru 1316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-tru 1319

This theorem is referenced by:  hadbi123i  1384  cadbi123i  1385  nfn  1793  nfimOLD  1814  nfan  1824  nfbi  1834  nfnfOLD  1846  sbie  2038  eubii  2213  nfeu  2220  nfmo  2221  mobii  2240  dvelimc  2511  ralbii  2639  rexbii  2640  nfral  2668  nfreu  2786  nfrmo  2787  nfrab  2793  nfsbc1  3065  nfsbc  3068  sbcbii  3102  csbeq2i  3163  nfcsb1  3168  nfcsb  3171  nfif  3687  nfiota  4344  nfbr  4684  nfov  5546  mpt2eq123i  5665  mpteq12i  5666  mpt2eq3ia  5671  ider  5944  ssetpov  5945  eqer  5962  ener  6040  lecponc  6214