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  2651  nfsbc1  2980  nfsbc  2983  sbcbii  3022  csbeq2i  3084  nfcsb1  3089  nfcsbw  3093  nfcsb  3094  nfif  3562  ssbri  4047  nfbr  4049  mpteq12i  4091  ralxfr  4466  rexxfr  4468  nfiotaw  5182  nfriota  5839  nfov  5904  mpoeq123i  5937  mpoeq3ia  5939  disjsnxp  6237  tfri1  6365  eqer  6566  0er  6568  ecopover  6632  ecopoverg  6635  nfixpxy  6716  en2i  6769  en3i  6770  ener  6778  ensymb  6779  entr  6783  djuf1olem  7051  omp1eomlem  7092  infnninf  7121  ltsopi  7318  ltsonq  7396  enq0er  7433  ltpopr  7593  ltposr  7761  axcnex  7857  axaddf  7866  axmulf  7867  ltso  8033  nfneg  8152  negiso  8910  sup3exmid  8912  xrltso  9794  frecfzennn  10423  frechashgf1o  10425  0tonninf  10436  1tonninf  10437  facnn  10702  fac0  10703  fac1  10704  cnrecnv  10914  cau3  11119  xrnegiso  11265  sum0  11391  trireciplem  11503  trirecip  11504  ege2le3  11674  oddpwdc  12168  ennnfonelem1  12402  ennnfonelemhf1o  12408  strnfvn  12477  strslss  12504  mndprop  12796  grpprop  12848  isgrpi  12854  ablprop  13053  ringprop  13172  cnfldstr  13348  cncrng  13354  zringbas  13377  zringplusg  13378  dvdsrzring  13384  txswaphmeolem  13713  divcnap  13948  elcncf1ii  13960  cnrehmeocntop  13986  dvid  14055  dveflem  14080  dvef  14081  sincn  14083  coscn  14084  cosz12  14094  sincos6thpi  14156  lgsdir2lem5  14326  bj-sttru  14374  bj-dctru  14387  bj-sbimeh  14406  bdnthALT  14469  012of  14627  2o01f  14628  isomninnlem  14660  iooref1o  14664  iswomninnlem  14679  ismkvnnlem  14682  dceqnconst  14689  dcapnconst  14690  taupi  14702