Theorem mptru 1352

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

Syntax hints:   → wi 4  ⊤wtru 1344

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 1346

This theorem is referenced by:  xorbi12i  1373  nfbi  1577  spime  1729  eubii  2023  nfmo  2034  mobii  2051  dvelimc  2330  ralbii  2472  rexbii  2473  nfralw  2503  nfralxy  2504  nfrexxy  2505  nfralya  2506  nfrexya  2507  nfreuxy  2640  nfsbc1  2968  nfsbc  2971  sbcbii  3010  csbeq2i  3072  nfcsb1  3077  nfcsbw  3081  nfcsb  3082  nfif  3548  ssbri  4026  nfbr  4028  mpteq12i  4070  ralxfr  4444  rexxfr  4446  nfiotaw  5157  nfriota  5807  nfov  5872  mpoeq123i  5905  mpoeq3ia  5907  disjsnxp  6205  tfri1  6333  eqer  6533  0er  6535  ecopover  6599  ecopoverg  6602  nfixpxy  6683  en2i  6736  en3i  6737  ener  6745  ensymb  6746  entr  6750  djuf1olem  7018  omp1eomlem  7059  infnninf  7088  ltsopi  7261  ltsonq  7339  enq0er  7376  ltpopr  7536  ltposr  7704  axcnex  7800  axaddf  7809  axmulf  7810  ltso  7976  nfneg  8095  negiso  8850  sup3exmid  8852  xrltso  9732  frecfzennn  10361  frechashgf1o  10363  0tonninf  10374  1tonninf  10375  facnn  10640  fac0  10641  fac1  10642  cnrecnv  10852  cau3  11057  xrnegiso  11203  sum0  11329  trireciplem  11441  trirecip  11442  ege2le3  11612  oddpwdc  12106  ennnfonelem1  12340  ennnfonelemhf1o  12346  strnfvn  12415  strslss  12441  txswaphmeolem  12960  divcnap  13195  elcncf1ii  13207  cnrehmeocntop  13233  dvid  13302  dveflem  13327  dvef  13328  sincn  13330  coscn  13331  cosz12  13341  sincos6thpi  13403  lgsdir2lem5  13573  bj-sttru  13621  bj-dctru  13634  bj-sbimeh  13653  bdnthALT  13717  012of  13875  2o01f  13876  isomninnlem  13909  iooref1o  13913  iswomninnlem  13928  ismkvnnlem  13931  dceqnconst  13938  dcapnconst  13939  taupi  13949