Theorem mptru 1406

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

Syntax hints:   → wi 4  ⊤wtru 1398

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 1400

This theorem is referenced by:  xorbi12i  1427  dcfromcon  1493  nfbi  1637  spime  1789  eubii  2088  nfmo  2099  mobii  2116  dvelimc  2396  ralbii  2538  rexbii  2539  nfralw  2569  nfralxy  2570  nfrexw  2571  nfralya  2572  nfrexya  2573  nfreuw  2708  rabbia2  2787  nfsbc1  3049  nfsbc  3052  sbcbii  3091  csbeq2i  3154  nfcsb1  3159  nfsbcw  3162  nfcsbw  3164  nfcsb  3165  nfif  3634  ssbri  4133  nfbr  4135  mpteq12i  4177  ralxfr  4563  rexxfr  4565  nfiotaw  5290  nfriota  5981  nfov  6048  mpoeq123i  6084  mpoeq3ia  6086  disjsnxp  6402  tfri1  6531  eqer  6734  0er  6736  ecopover  6802  ecopoverg  6805  nfixpxy  6886  en2i  6943  en3i  6944  ener  6953  ensymb  6954  entr  6958  djuf1olem  7252  omp1eomlem  7293  infnninf  7323  ltsopi  7540  ltsonq  7618  enq0er  7655  ltpopr  7815  ltposr  7983  axcnex  8079  axaddf  8088  axmulf  8089  ltso  8257  nfneg  8376  negiso  9135  sup3exmid  9137  xrltso  10031  frecfzennn  10689  frechashgf1o  10691  0tonninf  10703  1tonninf  10704  nninfinf  10706  facnn  10990  fac0  10991  fac1  10992  cnrecnv  11475  cau3  11680  xrnegiso  11827  sum0  11954  trireciplem  12066  trirecip  12067  ege2le3  12237  oddpwdc  12751  modxai  12994  modsubi  12997  ennnfonelem1  13033  ennnfonelemhf1o  13039  strnfvn  13108  strslss  13135  prdsvallem  13360  prdsval  13361  mndprop  13529  grpprop  13606  isgrpi  13612  ablprop  13889  ringprop  14059  rlmfn  14473  cnfldstr  14578  cncrng  14589  cnfldui  14609  zringbas  14616  zringplusg  14617  dvdsrzring  14623  expghmap  14627  fnpsr  14687  txswaphmeolem  15050  divcnap  15295  expcn  15299  elcncf1ii  15310  cnrehmeocntop  15340  hovercncf  15376  dvid  15425  dvidre  15427  dveflem  15456  dvef  15457  sincn  15499  coscn  15500  cosz12  15510  sincos6thpi  15572  lgsdir2lem5  15767  bj-sttru  16362  bj-dctru  16375  bj-sbimeh  16394  bdnthALT  16456  012of  16618  2o01f  16619  isomninnlem  16660  iooref1o  16664  iswomninnlem  16680  ismkvnnlem  16683  dceqnconst  16691  dcapnconst  16692  taupi  16704