Theorem mptru 1407

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

Syntax hints:   -> wi 4   T. wtru 1399

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

This theorem depends on definitions:  df-bi 117  df-tru 1401

This theorem is referenced by:  xorbi12i  1428  dcfromcon  1494  nfbi  1638  spime  1790  eubii  2091  nfmo  2102  mobii  2119  eqabi  2367  dvelimc  2408  ralbii  2550  rexbii  2551  nfralw  2581  nfralxy  2582  nfrexw  2583  nfralya  2584  nfrexya  2585  nfreuw  2720  rabbia2  2800  nfsbc1  3062  nfsbc  3065  sbcbii  3104  csbeq2i  3167  nfcsb1  3172  nfsbcw  3175  nfcsbw  3177  nfcsb  3178  nfif  3653  ssbri  4156  nfbr  4158  mpteq12i  4200  ralxfr  4589  rexxfr  4591  nfiotaw  5318  nfriota  6015  nfov  6082  mpoeq123i  6118  mpoeq3ia  6120  disjsnxp  6435  tfri1  6598  eqer  6801  0er  6803  ecopover  6869  ecopoverg  6872  nfixpxy  6954  en2i  7011  en3i  7012  ener  7021  ensymb  7022  entr  7026  djuf1olem  7346  omp1eomlem  7387  infnninf  7417  ltsopi  7637  ltsonq  7715  enq0er  7752  ltpopr  7912  ltposr  8080  axcnex  8176  axaddf  8185  axmulf  8186  ltso  8353  nfneg  8472  negiso  9231  sup3exmid  9233  xrltso  10132  frecfzennn  10792  frechashgf1o  10794  0tonninf  10806  1tonninf  10807  nninfinf  10809  facnn  11093  fac0  11094  fac1  11095  cnrecnv  11599  cau3  11804  xrnegiso  11951  sum0  12078  trireciplem  12190  trirecip  12191  ege2le3  12361  oddpwdc  12875  modxai  13118  modsubi  13121  ballotfilemofi  13142  ballotfilem2  13149  ennnfonelem1  13175  ennnfonelemhf1o  13181  strnfvn  13250  strslss  13277  prdsvallem  13502  prdsval  13503  mndprop  13671  grpprop  13748  isgrpi  13754  ablprop  14031  ringprop  14201  rlmfn  14618  cnfldstr  14723  cncrng  14734  cnfldui  14754  zringbas  14761  zringplusg  14762  dvdsrzring  14768  expghmap  14772  fnpsr  14832  txswaphmeolem  15202  divcnap  15447  expcn  15451  elcncf1ii  15462  cnrehmeocntop  15492  hovercncf  15528  dvid  15577  dvidre  15579  dveflem  15608  dvef  15609  sincn  15651  coscn  15652  cosz12  15662  sincos6thpi  15724  lgsdir2lem5  15922  konigsbergvtx  16494  konigsbergiedg  16495  konigsbergiedgwen  16496  konigsbergumgr  16499  konigsberglem1  16500  konigsberglem2  16501  konigsberglem3  16502  konigsberglem5  16504  konigsberg  16505  bj-sttru  16529  bj-dctru  16542  bj-sbimeh  16561  bdnthALT  16622  012of  16784  2o01f  16785  isomninnlem  16831  iooref1o  16835  iswomninnlem  16851  ismkvnnlem  16854  dceqnconst  16863  dcapnconst  16864  taupi  16876