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  7394  omp1eomlem  7435  infnninf  7465  ltsopi  7688  ltsonq  7766  enq0er  7803  ltpopr  7963  ltposr  8131  axcnex  8227  axaddf  8236  axmulf  8237  ltso  8404  nfneg  8525  negiso  9288  sup3exmid  9290  xrltso  10209  frecfzennn  10878  frechashgf1o  10880  0tonninf  10892  1tonninf  10893  nninfinf  10895  facnn  11181  fac0  11182  fac1  11183  cnrecnv  11692  cau3  11898  xrnegiso  12047  sum0  12174  trireciplem  12286  trirecip  12287  ege2le3  12457  modxai  13218  modsubi  13222  ballotfilemofi  13271  ballotfilem2  13280  ballotfilemefi  13289  ballotfilemafi  13290  ballotfilembfi  13291  ballotfilemrinv  13329  ennnfonelem1  13350  ennnfonelemhf1o  13356  strnfvn  13425  strslss  13452  prdsvallem  13674  mndprop  13807  grpprop  13876  isgrpi  13882  ablprop  14184  prdsval  14257  ringprop  14429  rlmfn  14874  cnfldstr  14979  cncrng  14990  cnfldui  15008  zringbas  15015  zringplusg  15016  dvdsrzring  15022  expghmap  15026  fnpsr  15135  txswaphmeolem  15512  divcnap  15757  expcn  15761  elcncf1ii  15772  cnrehmeocntop  15802  hovercncf  15838  dvid  15887  dvidre  15889  dveflem  15918  dvef  15919  sincn  15961  coscn  15962  cosz12  15973  sincos6thpi  16035  log2ublem2  16183  log2ublog2  16185  lgsdir2lem5  16317  konigsbergvtx  16889  konigsbergiedg  16890  konigsbergiedgwen  16891  konigsbergumgr  16894  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  konigsberg  16900  bj-sttru  16934  bj-dctru  16947  bj-sbimeh  16966  bdnthALT  17027  012of  17189  2o01f  17190  isomninnlem  17245  iooref1o  17249  iswomninnlem  17266  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278  taupi  17290