Theorem trud 1293

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

Hypothesis

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

Assertion

Ref	Expression
trud	|- ph

Proof of Theorem trud

Step	Hyp	Ref	Expression
1		tru 1288	. 2 |- T.
2		trud.1	. 2 |- ( T. -> ph )
3	1, 2	ax-mp 7	1 |- ph

Syntax hints:   -> wi 4   T. wtru 1285

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 1287

This theorem is referenced by:  xorbi12i  1314  nfbi  1521  spime  1669  eubii  1950  nfmo  1961  mobii  1978  dvelimc  2239  ralbii  2372  rexbii  2373  nfralxy  2402  nfrexxy  2403  nfralya  2404  nfrexya  2405  nfreuxy  2528  nfsbc1  2832  nfsbc  2835  sbcbii  2873  csbeq2i  2932  nfcsb1  2937  nfcsb  2940  nfif  3377  ssbri  3827  nfbr  3829  mpteq12i  3866  ralxfr  4216  rexxfr  4218  nfiotaxy  4891  nfriota  5497  nfov  5555  mpt2eq123i  5588  mpt2eq3ia  5590  tfri1  5974  eqer  6161  0er  6163  ecopover  6227  ecopoverg  6230  en2i  6273  en3i  6274  ener  6282  ensymb  6283  entr  6287  ltsopi  6510  ltsonq  6588  enq0er  6625  ltpopr  6785  ltposr  6940  axcnex  7027  ltso  7189  nfneg  7305  negiso  8033  xrltso  8871  frecfzennn  9419  frechashgf1o  9421  facnn  9654  fac0  9655  fac1  9656  cnrecnv  9797  cau3  10001  oddpwdc  10552  bj-sbimeh  10583  bdnthALT  10626