Theorem mptru 1362

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

Syntax hints:   → wi 4  ⊤wtru 1354

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 1356

This theorem is referenced by:  xorbi12i  1383  nfbi  1589  spime  1741  eubii  2035  nfmo  2046  mobii  2063  dvelimc  2341  ralbii  2483  rexbii  2484  nfralw  2514  nfralxy  2515  nfrexxy  2516  nfralya  2517  nfrexya  2518  nfreuxy  2652  nfsbc1  2982  nfsbc  2985  sbcbii  3024  csbeq2i  3086  nfcsb1  3091  nfcsbw  3095  nfcsb  3096  nfif  3564  ssbri  4049  nfbr  4051  mpteq12i  4093  ralxfr  4468  rexxfr  4470  nfiotaw  5184  nfriota  5842  nfov  5907  mpoeq123i  5940  mpoeq3ia  5942  disjsnxp  6240  tfri1  6368  eqer  6569  0er  6571  ecopover  6635  ecopoverg  6638  nfixpxy  6719  en2i  6772  en3i  6773  ener  6781  ensymb  6782  entr  6786  djuf1olem  7054  omp1eomlem  7095  infnninf  7124  ltsopi  7321  ltsonq  7399  enq0er  7436  ltpopr  7596  ltposr  7764  axcnex  7860  axaddf  7869  axmulf  7870  ltso  8037  nfneg  8156  negiso  8914  sup3exmid  8916  xrltso  9798  frecfzennn  10428  frechashgf1o  10430  0tonninf  10441  1tonninf  10442  facnn  10709  fac0  10710  fac1  10711  cnrecnv  10921  cau3  11126  xrnegiso  11272  sum0  11398  trireciplem  11510  trirecip  11511  ege2le3  11681  oddpwdc  12176  ennnfonelem1  12410  ennnfonelemhf1o  12416  strnfvn  12485  strslss  12512  mndprop  12847  grpprop  12899  isgrpi  12905  ablprop  13105  ringprop  13224  cnfldstr  13542  cncrng  13548  zringbas  13571  zringplusg  13572  dvdsrzring  13578  txswaphmeolem  13905  divcnap  14140  elcncf1ii  14152  cnrehmeocntop  14178  dvid  14247  dveflem  14272  dvef  14273  sincn  14275  coscn  14276  cosz12  14286  sincos6thpi  14348  lgsdir2lem5  14518  bj-sttru  14577  bj-dctru  14590  bj-sbimeh  14609  bdnthALT  14672  012of  14830  2o01f  14831  isomninnlem  14863  iooref1o  14867  iswomninnlem  14882  ismkvnnlem  14885  dceqnconst  14893  dcapnconst  14894  taupi  14906