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  3003  nfsbc  3006  sbcbii  3045  csbeq2i  3107  nfcsb1  3112  nfsbcw  3115  nfcsbw  3117  nfcsb  3118  nfif  3585  ssbri  4073  nfbr  4075  mpteq12i  4117  ralxfr  4497  rexxfr  4499  nfiotaw  5219  nfriota  5883  nfov  5948  mpoeq123i  5981  mpoeq3ia  5983  disjsnxp  6290  tfri1  6418  eqer  6619  0er  6621  ecopover  6687  ecopoverg  6690  nfixpxy  6771  en2i  6824  en3i  6825  ener  6833  ensymb  6834  entr  6838  djuf1olem  7112  omp1eomlem  7153  infnninf  7183  ltsopi  7380  ltsonq  7458  enq0er  7495  ltpopr  7655  ltposr  7823  axcnex  7919  axaddf  7928  axmulf  7929  ltso  8097  nfneg  8216  negiso  8974  sup3exmid  8976  xrltso  9862  frecfzennn  10497  frechashgf1o  10499  0tonninf  10511  1tonninf  10512  nninfinf  10514  facnn  10798  fac0  10799  fac1  10800  cnrecnv  11054  cau3  11259  xrnegiso  11405  sum0  11531  trireciplem  11643  trirecip  11644  ege2le3  11814  oddpwdc  12312  ennnfonelem1  12564  ennnfonelemhf1o  12570  strnfvn  12639  strslss  12666  mndprop  13022  grpprop  13090  isgrpi  13096  ablprop  13367  ringprop  13536  rlmfn  13949  cnfldstr  14049  cncrng  14057  cnfldui  14077  zringbas  14084  zringplusg  14085  dvdsrzring  14091  expghmap  14095  fnpsr  14153  txswaphmeolem  14488  divcnap  14723  elcncf1ii  14735  cnrehmeocntop  14764  hovercncf  14800  dvid  14847  dveflem  14872  dvef  14873  sincn  14904  coscn  14905  cosz12  14915  sincos6thpi  14977  lgsdir2lem5  15148  bj-sttru  15232  bj-dctru  15245  bj-sbimeh  15264  bdnthALT  15327  012of  15486  2o01f  15487  isomninnlem  15520  iooref1o  15524  iswomninnlem  15539  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551  taupi  15563