Theorem mptru 1298

Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
mptru.1	⊢ (⊤ → 𝜑)

Assertion

Ref	Expression
mptru	⊢ 𝜑

Proof of Theorem mptru

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

Syntax hints:   → wi 4  ⊤wtru 1290

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 1292

This theorem is referenced by:  xorbi12i  1319  nfbi  1526  spime  1676  eubii  1957  nfmo  1968  mobii  1985  dvelimc  2249  ralbii  2384  rexbii  2385  nfralxy  2414  nfrexxy  2415  nfralya  2416  nfrexya  2417  nfreuxy  2541  nfsbc1  2857  nfsbc  2860  sbcbii  2898  csbeq2i  2957  nfcsb1  2962  nfcsb  2965  nfif  3419  ssbri  3887  nfbr  3889  mpteq12i  3926  ralxfr  4288  rexxfr  4290  nfiotaxy  4984  nfriota  5617  nfov  5679  mpt2eq123i  5712  mpt2eq3ia  5714  disjsnxp  6002  tfri1  6130  eqer  6322  0er  6324  ecopover  6388  ecopoverg  6391  en2i  6485  en3i  6486  ener  6494  ensymb  6495  entr  6499  djuf1olem  6743  ltsopi  6877  ltsonq  6955  enq0er  6992  ltpopr  7152  ltposr  7307  axcnex  7394  ltso  7561  nfneg  7677  negiso  8414  xrltso  9264  frecfzennn  9829  frechashgf1o  9831  0tonninf  9841  1tonninf  9842  facnn  10131  fac0  10132  fac1  10133  cnrecnv  10340  cau3  10544  sum0  10776  trireciplem  10890  trirecip  10891  ege2le3  10957  oddpwdc  11426  strnfvn  11513  strnss  11536  elcncf1ii  11591  bj-sbimeh  11628  bdnthALT  11681