Theorem mptru 1298

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 1293	. 2 |- T.
2		mptru.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 7	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1290

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

This theorem depends on definitions:  df-bi 115  df-tru 1292

This theorem is referenced by:  xorbi12i  1319  nfbi  1526  spime  1676  eubii  1957  nfmo  1968  mobii  1985  dvelimc  2249  ralbii  2384  rexbii  2385  nfralxy  2414  nfrexxy  2415  nfralya  2416  nfrexya  2417  nfreuxy  2541  nfsbc1  2857  nfsbc  2860  sbcbii  2898  csbeq2i  2957  nfcsb1  2962  nfcsb  2965  nfif  3419  ssbri  3887  nfbr  3889  mpteq12i  3926  ralxfr  4288  rexxfr  4290  nfiotaxy  4984  nfriota  5617  nfov  5679  mpt2eq123i  5712  mpt2eq3ia  5714  disjsnxp  6002  tfri1  6130  eqer  6324  0er  6326  ecopover  6390  ecopoverg  6393  en2i  6487  en3i  6488  ener  6496  ensymb  6497  entr  6501  djuf1olem  6745  ltsopi  6879  ltsonq  6957  enq0er  6994  ltpopr  7154  ltposr  7309  axcnex  7396  ltso  7563  nfneg  7679  negiso  8416  xrltso  9266  frecfzennn  9833  frechashgf1o  9835  0tonninf  9845  1tonninf  9846  facnn  10135  fac0  10136  fac1  10137  cnrecnv  10344  cau3  10548  sum0  10780  trireciplem  10894  trirecip  10895  ege2le3  10961  oddpwdc  11430  strnfvn  11517  strslss  11541  elcncf1ii  11636  bj-sbimeh  11673  bdnthALT  11726