Theorem mptru 1373

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

Syntax hints:   → wi 4  ⊤wtru 1365

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 1367

This theorem is referenced by:  xorbi12i  1394  dcfromcon  1459  nfbi  1603  spime  1755  eubii  2054  nfmo  2065  mobii  2082  dvelimc  2361  ralbii  2503  rexbii  2504  nfralw  2534  nfralxy  2535  nfrexw  2536  nfralya  2537  nfrexya  2538  nfreuxy  2672  nfsbc1  3007  nfsbc  3010  sbcbii  3049  csbeq2i  3111  nfcsb1  3116  nfsbcw  3119  nfcsbw  3121  nfcsb  3122  nfif  3589  ssbri  4077  nfbr  4079  mpteq12i  4121  ralxfr  4501  rexxfr  4503  nfiotaw  5223  nfriota  5887  nfov  5952  mpoeq123i  5985  mpoeq3ia  5987  disjsnxp  6295  tfri1  6423  eqer  6624  0er  6626  ecopover  6692  ecopoverg  6695  nfixpxy  6776  en2i  6829  en3i  6830  ener  6838  ensymb  6839  entr  6843  djuf1olem  7119  omp1eomlem  7160  infnninf  7190  ltsopi  7387  ltsonq  7465  enq0er  7502  ltpopr  7662  ltposr  7830  axcnex  7926  axaddf  7935  axmulf  7936  ltso  8104  nfneg  8223  negiso  8982  sup3exmid  8984  xrltso  9871  frecfzennn  10518  frechashgf1o  10520  0tonninf  10532  1tonninf  10533  nninfinf  10535  facnn  10819  fac0  10820  fac1  10821  cnrecnv  11075  cau3  11280  xrnegiso  11427  sum0  11553  trireciplem  11665  trirecip  11666  ege2le3  11836  oddpwdc  12342  modxai  12585  modsubi  12588  ennnfonelem1  12624  ennnfonelemhf1o  12630  strnfvn  12699  strslss  12726  mndprop  13082  grpprop  13150  isgrpi  13156  ablprop  13427  ringprop  13596  rlmfn  14009  cnfldstr  14114  cncrng  14125  cnfldui  14145  zringbas  14152  zringplusg  14153  dvdsrzring  14159  expghmap  14163  fnpsr  14221  txswaphmeolem  14556  divcnap  14801  expcn  14805  elcncf1ii  14816  cnrehmeocntop  14846  hovercncf  14882  dvid  14931  dvidre  14933  dveflem  14962  dvef  14963  sincn  15005  coscn  15006  cosz12  15016  sincos6thpi  15078  lgsdir2lem5  15273  bj-sttru  15386  bj-dctru  15399  bj-sbimeh  15418  bdnthALT  15481  012of  15640  2o01f  15641  isomninnlem  15674  iooref1o  15678  iswomninnlem  15693  ismkvnnlem  15696  dceqnconst  15704  dcapnconst  15705  taupi  15717