Theorem mptru 1340

Description: Eliminate T. as an antecedent. A proposition implied by T. is true. (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
mptru.1	|- ( T. -> ph )

Assertion

Ref	Expression
mptru	|- ph

Proof of Theorem mptru

Step	Hyp	Ref	Expression
1		tru 1335	. 2 |- T.
2		mptru.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 5	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-tru 1334

This theorem is referenced by:  xorbi12i  1361  nfbi  1568  spime  1719  eubii  2008  nfmo  2019  mobii  2036  dvelimc  2302  ralbii  2441  rexbii  2442  nfralxy  2471  nfrexxy  2472  nfralya  2473  nfrexya  2474  nfreuxy  2605  nfsbc1  2926  nfsbc  2929  sbcbii  2968  csbeq2i  3029  nfcsb1  3034  nfcsb  3037  nfif  3500  ssbri  3972  nfbr  3974  mpteq12i  4016  ralxfr  4387  rexxfr  4389  nfiotaw  5092  nfriota  5739  nfov  5801  mpoeq123i  5834  mpoeq3ia  5836  disjsnxp  6134  tfri1  6262  eqer  6461  0er  6463  ecopover  6527  ecopoverg  6530  nfixpxy  6611  en2i  6664  en3i  6665  ener  6673  ensymb  6674  entr  6678  djuf1olem  6938  omp1eomlem  6979  ltsopi  7128  ltsonq  7206  enq0er  7243  ltpopr  7403  ltposr  7571  axcnex  7667  axaddf  7676  axmulf  7677  ltso  7842  nfneg  7959  negiso  8713  sup3exmid  8715  xrltso  9582  frecfzennn  10199  frechashgf1o  10201  0tonninf  10212  1tonninf  10213  facnn  10473  fac0  10474  fac1  10475  cnrecnv  10682  cau3  10887  xrnegiso  11031  sum0  11157  trireciplem  11269  trirecip  11270  ege2le3  11377  oddpwdc  11852  ennnfonelem1  11920  ennnfonelemhf1o  11926  strnfvn  11980  strslss  12006  txswaphmeolem  12489  divcnap  12724  elcncf1ii  12736  cnrehmeocntop  12762  dvid  12831  dveflem  12855  dvef  12856  sincn  12858  coscn  12859  cosz12  12861  sincos6thpi  12923  bj-sbimeh  12979  bdnthALT  13033  isomninnlem  13225  taupi  13239