Theorem trud 1251

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

Syntax hints:   -> wi 4   T. wtru 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-tru 1245

This theorem is referenced by:  nfbi  1478  spime  1626  eubii  1906  nfmo  1917  mobii  1934  dvelimc  2195  ralbii  2324  rexbii  2325  nfralxy  2354  nfrexxy  2355  nfralya  2356  nfrexya  2357  nfreuxy  2478  nfsbc1  2775  nfsbc  2778  sbcbii  2812  csbeq2i  2870  nfcsb1  2875  nfcsb  2878  nfif  3350  ssbri  3797  nfbr  3799  mpteq12i  3836  ralxfr  4164  rexxfr  4166  nfiotaxy  4814  nfriota  5420  nfov  5478  mpt2eq123i  5510  mpt2eq3ia  5512  tfri1  5892  eqer  6074  0er  6076  ecopover  6140  ecopoverg  6143  en2i  6186  en3i  6187  ener  6195  ensymb  6196  entr  6200  ltsopi  6304  ltsonq  6382  enq0er  6417  ltpopr  6568  ltposr  6671  axcnex  6725  ltso  6873  nfneg  6985  xrltso  8467  frecfzennn  8864  frechashgf1o  8866  cnrecnv  9118  bj-sbimeh  9227  bdnthALT  9270