Theorem mptru 1341

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

Syntax hints:   → wi 4  ⊤wtru 1333

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 1335

This theorem is referenced by:  xorbi12i  1362  nfbi  1569  spime  1720  eubii  2009  nfmo  2020  mobii  2037  dvelimc  2303  ralbii  2444  rexbii  2445  nfralxy  2474  nfrexxy  2475  nfralya  2476  nfrexya  2477  nfreuxy  2608  nfsbc1  2930  nfsbc  2933  sbcbii  2972  csbeq2i  3034  nfcsb1  3039  nfcsb  3042  nfif  3505  ssbri  3980  nfbr  3982  mpteq12i  4024  ralxfr  4395  rexxfr  4397  nfiotaw  5100  nfriota  5747  nfov  5809  mpoeq123i  5842  mpoeq3ia  5844  disjsnxp  6142  tfri1  6270  eqer  6469  0er  6471  ecopover  6535  ecopoverg  6538  nfixpxy  6619  en2i  6672  en3i  6673  ener  6681  ensymb  6682  entr  6686  djuf1olem  6946  omp1eomlem  6987  ltsopi  7152  ltsonq  7230  enq0er  7267  ltpopr  7427  ltposr  7595  axcnex  7691  axaddf  7700  axmulf  7701  ltso  7866  nfneg  7983  negiso  8737  sup3exmid  8739  xrltso  9612  frecfzennn  10230  frechashgf1o  10232  0tonninf  10243  1tonninf  10244  facnn  10505  fac0  10506  fac1  10507  cnrecnv  10714  cau3  10919  xrnegiso  11063  sum0  11189  trireciplem  11301  trirecip  11302  ege2le3  11414  oddpwdc  11888  ennnfonelem1  11956  ennnfonelemhf1o  11962  strnfvn  12019  strslss  12045  txswaphmeolem  12528  divcnap  12763  elcncf1ii  12775  cnrehmeocntop  12801  dvid  12870  dveflem  12895  dvef  12896  sincn  12898  coscn  12899  cosz12  12909  sincos6thpi  12971  bj-sbimeh  13150  bdnthALT  13204  012of  13363  2o01f  13364  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423  iooref1o  13426  taupi  13430