Theorem mptru 1382

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

Syntax hints:   -> wi 4   T. wtru 1374

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 1376

This theorem is referenced by:  xorbi12i  1403  dcfromcon  1468  nfbi  1612  spime  1764  eubii  2063  nfmo  2074  mobii  2091  dvelimc  2370  ralbii  2512  rexbii  2513  nfralw  2543  nfralxy  2544  nfrexw  2545  nfralya  2546  nfrexya  2547  nfreuxy  2681  nfsbc1  3016  nfsbc  3019  sbcbii  3058  csbeq2i  3120  nfcsb1  3125  nfsbcw  3128  nfcsbw  3130  nfcsb  3131  nfif  3599  ssbri  4088  nfbr  4090  mpteq12i  4132  ralxfr  4513  rexxfr  4515  nfiotaw  5236  nfriota  5909  nfov  5974  mpoeq123i  6008  mpoeq3ia  6010  disjsnxp  6323  tfri1  6451  eqer  6652  0er  6654  ecopover  6720  ecopoverg  6723  nfixpxy  6804  en2i  6861  en3i  6862  ener  6871  ensymb  6872  entr  6876  djuf1olem  7155  omp1eomlem  7196  infnninf  7226  ltsopi  7433  ltsonq  7511  enq0er  7548  ltpopr  7708  ltposr  7876  axcnex  7972  axaddf  7981  axmulf  7982  ltso  8150  nfneg  8269  negiso  9028  sup3exmid  9030  xrltso  9918  frecfzennn  10571  frechashgf1o  10573  0tonninf  10585  1tonninf  10586  nninfinf  10588  facnn  10872  fac0  10873  fac1  10874  cnrecnv  11221  cau3  11426  xrnegiso  11573  sum0  11699  trireciplem  11811  trirecip  11812  ege2le3  11982  oddpwdc  12496  modxai  12739  modsubi  12742  ennnfonelem1  12778  ennnfonelemhf1o  12784  strnfvn  12853  strslss  12880  prdsvallem  13104  prdsval  13105  mndprop  13273  grpprop  13350  isgrpi  13356  ablprop  13633  ringprop  13802  rlmfn  14215  cnfldstr  14320  cncrng  14331  cnfldui  14351  zringbas  14358  zringplusg  14359  dvdsrzring  14365  expghmap  14369  fnpsr  14429  txswaphmeolem  14792  divcnap  15037  expcn  15041  elcncf1ii  15052  cnrehmeocntop  15082  hovercncf  15118  dvid  15167  dvidre  15169  dveflem  15198  dvef  15199  sincn  15241  coscn  15242  cosz12  15252  sincos6thpi  15314  lgsdir2lem5  15509  bj-sttru  15676  bj-dctru  15689  bj-sbimeh  15708  bdnthALT  15771  012of  15930  2o01f  15931  isomninnlem  15969  iooref1o  15973  iswomninnlem  15988  ismkvnnlem  15991  dceqnconst  15999  dcapnconst  16000  taupi  16012