Theorem mptru 1407

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

Syntax hints:   → wi 4  ⊤wtru 1399

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 1401

This theorem is referenced by:  xorbi12i  1428  dcfromcon  1494  nfbi  1638  spime  1790  eubii  2089  nfmo  2100  mobii  2117  eqabi  2365  dvelimc  2406  ralbii  2548  rexbii  2549  nfralw  2579  nfralxy  2580  nfrexw  2581  nfralya  2582  nfrexya  2583  nfreuw  2718  rabbia2  2798  nfsbc1  3060  nfsbc  3063  sbcbii  3102  csbeq2i  3165  nfcsb1  3170  nfsbcw  3173  nfcsbw  3175  nfcsb  3176  nfif  3651  ssbri  4154  nfbr  4156  mpteq12i  4198  ralxfr  4587  rexxfr  4589  nfiotaw  5316  nfriota  6013  nfov  6080  mpoeq123i  6116  mpoeq3ia  6118  disjsnxp  6433  tfri1  6596  eqer  6799  0er  6801  ecopover  6867  ecopoverg  6870  nfixpxy  6952  en2i  7009  en3i  7010  ener  7019  ensymb  7020  entr  7024  djuf1olem  7344  omp1eomlem  7385  infnninf  7415  ltsopi  7635  ltsonq  7713  enq0er  7750  ltpopr  7910  ltposr  8078  axcnex  8174  axaddf  8183  axmulf  8184  ltso  8351  nfneg  8470  negiso  9229  sup3exmid  9231  xrltso  10129  frecfzennn  10788  frechashgf1o  10790  0tonninf  10802  1tonninf  10803  nninfinf  10805  facnn  11089  fac0  11090  fac1  11091  cnrecnv  11595  cau3  11800  xrnegiso  11947  sum0  12074  trireciplem  12186  trirecip  12187  ege2le3  12357  oddpwdc  12871  modxai  13114  modsubi  13117  ballotfilemofi  13138  ballotfilem2  13142  ennnfonelem1  13158  ennnfonelemhf1o  13164  strnfvn  13233  strslss  13260  prdsvallem  13485  prdsval  13486  mndprop  13654  grpprop  13731  isgrpi  13737  ablprop  14014  ringprop  14184  rlmfn  14601  cnfldstr  14706  cncrng  14717  cnfldui  14737  zringbas  14744  zringplusg  14745  dvdsrzring  14751  expghmap  14755  fnpsr  14815  txswaphmeolem  15185  divcnap  15430  expcn  15434  elcncf1ii  15445  cnrehmeocntop  15475  hovercncf  15511  dvid  15560  dvidre  15562  dveflem  15591  dvef  15592  sincn  15634  coscn  15635  cosz12  15645  sincos6thpi  15707  lgsdir2lem5  15905  konigsbergvtx  16477  konigsbergiedg  16478  konigsbergiedgwen  16479  konigsbergumgr  16482  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  konigsberg  16488  bj-sttru  16512  bj-dctru  16525  bj-sbimeh  16544  bdnthALT  16605  012of  16767  2o01f  16768  isomninnlem  16814  iooref1o  16818  iswomninnlem  16834  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847  taupi  16859