Theorem mptru 1344

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

Syntax hints:   -> wi 4   T. wtru 1336

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 1338

This theorem is referenced by:  xorbi12i  1365  nfbi  1569  spime  1721  eubii  2015  nfmo  2026  mobii  2043  dvelimc  2321  ralbii  2463  rexbii  2464  nfralw  2494  nfralxy  2495  nfrexxy  2496  nfralya  2497  nfrexya  2498  nfreuxy  2631  nfsbc1  2954  nfsbc  2957  sbcbii  2996  csbeq2i  3058  nfcsb1  3063  nfcsbw  3067  nfcsb  3068  nfif  3534  ssbri  4010  nfbr  4012  mpteq12i  4054  ralxfr  4428  rexxfr  4430  nfiotaw  5141  nfriota  5791  nfov  5853  mpoeq123i  5886  mpoeq3ia  5888  disjsnxp  6186  tfri1  6314  eqer  6514  0er  6516  ecopover  6580  ecopoverg  6583  nfixpxy  6664  en2i  6717  en3i  6718  ener  6726  ensymb  6727  entr  6731  djuf1olem  6999  omp1eomlem  7040  infnninf  7069  ltsopi  7242  ltsonq  7320  enq0er  7357  ltpopr  7517  ltposr  7685  axcnex  7781  axaddf  7790  axmulf  7791  ltso  7957  nfneg  8076  negiso  8831  sup3exmid  8833  xrltso  9709  frecfzennn  10334  frechashgf1o  10336  0tonninf  10347  1tonninf  10348  facnn  10612  fac0  10613  fac1  10614  cnrecnv  10821  cau3  11026  xrnegiso  11170  sum0  11296  trireciplem  11408  trirecip  11409  ege2le3  11579  oddpwdc  12064  ennnfonelem1  12206  ennnfonelemhf1o  12212  strnfvn  12281  strslss  12307  txswaphmeolem  12790  divcnap  13025  elcncf1ii  13037  cnrehmeocntop  13063  dvid  13132  dveflem  13157  dvef  13158  sincn  13160  coscn  13161  cosz12  13171  sincos6thpi  13233  bj-sttru  13386  bj-dctru  13396  bj-sbimeh  13417  bdnthALT  13481  012of  13638  2o01f  13639  isomninnlem  13672  iooref1o  13676  iswomninnlem  13691  ismkvnnlem  13694  dceqnconst  13701  dcapnconst  13702  taupi  13712