Theorem mptru 1411

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-tru 1405

This theorem is used by:  xorbi12i  1432  dcfromcon  1498  nfbi  1642  spime  1794  eubii  2095  nfmo  2106  mobii  2123  eqabi  2371  dvelimc  2414  ralbii  2556  rexbii  2557  nfralw  2587  nfralxy  2588  nfrexw  2589  nfralya  2590  nfrexya  2591  nfreuw  2726  rabbia2  2806  nfsbc1  3069  nfsbc  3072  sbcbii  3111  csbeq2i  3174  nfcsb1  3179  nfsbcw  3182  nfcsbw  3184  nfcsb  3185  nfif  3669  ssbri  4175  nfbr  4177  mpteq12i  4219  ralxfr  4612  rexxfr  4614  nfiotaw  5341  nfriota  6048  nfov  6115  mpoeq123i  6151  mpoeq3ia  6153  disjsnxp  6473  tfri1  6636  eqer  6839  0er  6841  ecopover  6907  ecopoverg  6910  nfixpxy  6999  en2i  7056  en3i  7057  ener  7066  ensymb  7067  entr  7071  djuf1olem  7393  omp1eomlem  7434  infnninf  7464  ltsopi  7687  ltsonq  7765  enq0er  7802  ltpopr  7962  ltposr  8130  axcnex  8226  axaddf  8235  axmulf  8236  ltso  8403  nfneg  8524  negiso  9287  sup3exmid  9289  xrltso  10208  frecfzennn  10876  frechashgf1o  10878  0tonninf  10890  1tonninf  10891  nninfinf  10893  facnn  11179  fac0  11180  fac1  11181  cnrecnv  11690  cau3  11896  xrnegiso  12044  sum0  12171  trireciplem  12283  trirecip  12284  ege2le3  12454  modxai  13215  modsubi  13219  ballotfilemofi  13268  ballotfilem2  13277  ballotfilemefi  13286  ballotfilemafi  13287  ballotfilembfi  13288  ballotfilemrinv  13326  ennnfonelem1  13347  ennnfonelemhf1o  13353  strnfvn  13422  strslss  13449  prdsvallem  13670  mndprop  13803  grpprop  13872  isgrpi  13878  ablprop  14149  prdsval  14222  ringprop  14394  rlmfn  14839  cnfldstr  14944  cncrng  14955  cnfldui  14973  zringbas  14980  zringplusg  14981  dvdsrzring  14987  expghmap  14991  fnpsr  15100  txswaphmeolem  15470  divcnap  15715  expcn  15719  elcncf1ii  15730  cnrehmeocntop  15760  hovercncf  15796  dvid  15845  dvidre  15847  dveflem  15876  dvef  15877  sincn  15919  coscn  15920  cosz12  15931  sincos6thpi  15993  log2ublem2  16141  log2ublog2  16143  lgsdir2lem5  16249  konigsbergvtx  16821  konigsbergiedg  16822  konigsbergiedgwen  16823  konigsbergumgr  16826  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  konigsberg  16832  bj-sttru  16866  bj-dctru  16879  bj-sbimeh  16898  bdnthALT  16959  012of  17121  2o01f  17122  isomninnlem  17177  iooref1o  17181  iswomninnlem  17197  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209  taupi  17221