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  nfbi  1600  spime  1752  eubii  2051  nfmo  2062  mobii  2079  dvelimc  2358  ralbii  2500  rexbii  2501  nfralw  2531  nfralxy  2532  nfrexw  2533  nfralya  2534  nfrexya  2535  nfreuxy  2669  nfsbc1  3004  nfsbc  3007  sbcbii  3046  csbeq2i  3108  nfcsb1  3113  nfsbcw  3116  nfcsbw  3118  nfcsb  3119  nfif  3586  ssbri  4074  nfbr  4076  mpteq12i  4118  ralxfr  4498  rexxfr  4500  nfiotaw  5220  nfriota  5884  nfov  5949  mpoeq123i  5982  mpoeq3ia  5984  disjsnxp  6292  tfri1  6420  eqer  6621  0er  6623  ecopover  6689  ecopoverg  6692  nfixpxy  6773  en2i  6826  en3i  6827  ener  6835  ensymb  6836  entr  6840  djuf1olem  7114  omp1eomlem  7155  infnninf  7185  ltsopi  7382  ltsonq  7460  enq0er  7497  ltpopr  7657  ltposr  7825  axcnex  7921  axaddf  7930  axmulf  7931  ltso  8099  nfneg  8218  negiso  8976  sup3exmid  8978  xrltso  9865  frecfzennn  10500  frechashgf1o  10502  0tonninf  10514  1tonninf  10515  nninfinf  10517  facnn  10801  fac0  10802  fac1  10803  cnrecnv  11057  cau3  11262  xrnegiso  11408  sum0  11534  trireciplem  11646  trirecip  11647  ege2le3  11817  oddpwdc  12315  ennnfonelem1  12567  ennnfonelemhf1o  12573  strnfvn  12642  strslss  12669  mndprop  13025  grpprop  13093  isgrpi  13099  ablprop  13370  ringprop  13539  rlmfn  13952  cnfldstr  14057  cncrng  14068  cnfldui  14088  zringbas  14095  zringplusg  14096  dvdsrzring  14102  expghmap  14106  fnpsr  14164  txswaphmeolem  14499  divcnap  14744  expcn  14748  elcncf1ii  14759  cnrehmeocntop  14789  hovercncf  14825  dvid  14874  dvidre  14876  dveflem  14905  dvef  14906  sincn  14945  coscn  14946  cosz12  14956  sincos6thpi  15018  lgsdir2lem5  15189  bj-sttru  15302  bj-dctru  15315  bj-sbimeh  15334  bdnthALT  15397  012of  15556  2o01f  15557  isomninnlem  15590  iooref1o  15594  iswomninnlem  15609  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621  taupi  15633