Theorem mptru 1381

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

Syntax hints:   → wi 4  ⊤wtru 1373

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

This theorem depends on definitions:  df-bi 117  df-tru 1375

This theorem is referenced by:  xorbi12i  1402  dcfromcon  1467  nfbi  1611  spime  1763  eubii  2062  nfmo  2073  mobii  2090  dvelimc  2369  ralbii  2511  rexbii  2512  nfralw  2542  nfralxy  2543  nfrexw  2544  nfralya  2545  nfrexya  2546  nfreuxy  2680  nfsbc1  3015  nfsbc  3018  sbcbii  3057  csbeq2i  3119  nfcsb1  3124  nfsbcw  3127  nfcsbw  3129  nfcsb  3130  nfif  3598  ssbri  4087  nfbr  4089  mpteq12i  4131  ralxfr  4511  rexxfr  4513  nfiotaw  5233  nfriota  5899  nfov  5964  mpoeq123i  5998  mpoeq3ia  6000  disjsnxp  6313  tfri1  6441  eqer  6642  0er  6644  ecopover  6710  ecopoverg  6713  nfixpxy  6794  en2i  6847  en3i  6848  ener  6856  ensymb  6857  entr  6861  djuf1olem  7137  omp1eomlem  7178  infnninf  7208  ltsopi  7415  ltsonq  7493  enq0er  7530  ltpopr  7690  ltposr  7858  axcnex  7954  axaddf  7963  axmulf  7964  ltso  8132  nfneg  8251  negiso  9010  sup3exmid  9012  xrltso  9900  frecfzennn  10552  frechashgf1o  10554  0tonninf  10566  1tonninf  10567  nninfinf  10569  facnn  10853  fac0  10854  fac1  10855  cnrecnv  11140  cau3  11345  xrnegiso  11492  sum0  11618  trireciplem  11730  trirecip  11731  ege2le3  11901  oddpwdc  12415  modxai  12658  modsubi  12661  ennnfonelem1  12697  ennnfonelemhf1o  12703  strnfvn  12772  strslss  12799  prdsvallem  13022  prdsval  13023  mndprop  13191  grpprop  13268  isgrpi  13274  ablprop  13551  ringprop  13720  rlmfn  14133  cnfldstr  14238  cncrng  14249  cnfldui  14269  zringbas  14276  zringplusg  14277  dvdsrzring  14283  expghmap  14287  fnpsr  14347  txswaphmeolem  14710  divcnap  14955  expcn  14959  elcncf1ii  14970  cnrehmeocntop  15000  hovercncf  15036  dvid  15085  dvidre  15087  dveflem  15116  dvef  15117  sincn  15159  coscn  15160  cosz12  15170  sincos6thpi  15232  lgsdir2lem5  15427  bj-sttru  15540  bj-dctru  15553  bj-sbimeh  15572  bdnthALT  15635  012of  15794  2o01f  15795  isomninnlem  15833  iooref1o  15837  iswomninnlem  15852  ismkvnnlem  15855  dceqnconst  15863  dcapnconst  15864  taupi  15876