Theorem mptru 1404

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

Syntax hints:   → wi 4  ⊤wtru 1396

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 1398

This theorem is referenced by:  xorbi12i  1425  dcfromcon  1491  nfbi  1635  spime  1787  eubii  2086  nfmo  2097  mobii  2114  dvelimc  2394  ralbii  2536  rexbii  2537  nfralw  2567  nfralxy  2568  nfrexw  2569  nfralya  2570  nfrexya  2571  nfreuw  2706  nfsbc1  3046  nfsbc  3049  sbcbii  3088  csbeq2i  3151  nfcsb1  3156  nfsbcw  3159  nfcsbw  3161  nfcsb  3162  nfif  3631  ssbri  4128  nfbr  4130  mpteq12i  4172  ralxfr  4557  rexxfr  4559  nfiotaw  5282  nfriota  5970  nfov  6037  mpoeq123i  6073  mpoeq3ia  6075  disjsnxp  6389  tfri1  6517  eqer  6720  0er  6722  ecopover  6788  ecopoverg  6791  nfixpxy  6872  en2i  6929  en3i  6930  ener  6939  ensymb  6940  entr  6944  djuf1olem  7231  omp1eomlem  7272  infnninf  7302  ltsopi  7518  ltsonq  7596  enq0er  7633  ltpopr  7793  ltposr  7961  axcnex  8057  axaddf  8066  axmulf  8067  ltso  8235  nfneg  8354  negiso  9113  sup3exmid  9115  xrltso  10004  frecfzennn  10660  frechashgf1o  10662  0tonninf  10674  1tonninf  10675  nninfinf  10677  facnn  10961  fac0  10962  fac1  10963  cnrecnv  11436  cau3  11641  xrnegiso  11788  sum0  11914  trireciplem  12026  trirecip  12027  ege2le3  12197  oddpwdc  12711  modxai  12954  modsubi  12957  ennnfonelem1  12993  ennnfonelemhf1o  12999  strnfvn  13068  strslss  13095  prdsvallem  13320  prdsval  13321  mndprop  13489  grpprop  13566  isgrpi  13572  ablprop  13849  ringprop  14018  rlmfn  14432  cnfldstr  14537  cncrng  14548  cnfldui  14568  zringbas  14575  zringplusg  14576  dvdsrzring  14582  expghmap  14586  fnpsr  14646  txswaphmeolem  15009  divcnap  15254  expcn  15258  elcncf1ii  15269  cnrehmeocntop  15299  hovercncf  15335  dvid  15384  dvidre  15386  dveflem  15415  dvef  15416  sincn  15458  coscn  15459  cosz12  15469  sincos6thpi  15531  lgsdir2lem5  15726  bj-sttru  16159  bj-dctru  16172  bj-sbimeh  16191  bdnthALT  16253  012of  16416  2o01f  16417  isomninnlem  16458  iooref1o  16462  iswomninnlem  16477  ismkvnnlem  16480  dceqnconst  16488  dcapnconst  16489  taupi  16501