Theorem mptru 1340

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

Syntax hints:   → wi 4  ⊤wtru 1332

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

This theorem depends on definitions:  df-bi 116  df-tru 1334

This theorem is referenced by:  xorbi12i  1361  nfbi  1568  spime  1719  eubii  2006  nfmo  2017  mobii  2034  dvelimc  2300  ralbii  2439  rexbii  2440  nfralxy  2469  nfrexxy  2470  nfralya  2471  nfrexya  2472  nfreuxy  2603  nfsbc1  2921  nfsbc  2924  sbcbii  2963  csbeq2i  3024  nfcsb1  3029  nfcsb  3032  nfif  3495  ssbri  3967  nfbr  3969  mpteq12i  4011  ralxfr  4382  rexxfr  4384  nfiotaw  5087  nfriota  5732  nfov  5794  mpoeq123i  5827  mpoeq3ia  5829  disjsnxp  6127  tfri1  6255  eqer  6454  0er  6456  ecopover  6520  ecopoverg  6523  nfixpxy  6604  en2i  6657  en3i  6658  ener  6666  ensymb  6667  entr  6671  djuf1olem  6931  omp1eomlem  6972  ltsopi  7121  ltsonq  7199  enq0er  7236  ltpopr  7396  ltposr  7564  axcnex  7660  axaddf  7669  axmulf  7670  ltso  7835  nfneg  7952  negiso  8706  sup3exmid  8708  xrltso  9575  frecfzennn  10192  frechashgf1o  10194  0tonninf  10205  1tonninf  10206  facnn  10466  fac0  10467  fac1  10468  cnrecnv  10675  cau3  10880  xrnegiso  11024  sum0  11150  trireciplem  11262  trirecip  11263  ege2le3  11366  oddpwdc  11841  ennnfonelem1  11909  ennnfonelemhf1o  11915  strnfvn  11969  strslss  11995  txswaphmeolem  12478  divcnap  12713  elcncf1ii  12725  cnrehmeocntop  12751  dvid  12820  dveflem  12844  dvef  12845  sincn  12847  coscn  12848  cosz12  12850  sincos6thpi  12912  bj-sbimeh  12968  bdnthALT  13022  isomninnlem  13214  taupi  13228