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  1469  nfbi  1613  spime  1765  eubii  2064  nfmo  2075  mobii  2092  dvelimc  2372  ralbii  2514  rexbii  2515  nfralw  2545  nfralxy  2546  nfrexw  2547  nfralya  2548  nfrexya  2549  nfreuw  2683  nfsbc1  3023  nfsbc  3026  sbcbii  3065  csbeq2i  3128  nfcsb1  3133  nfsbcw  3136  nfcsbw  3138  nfcsb  3139  nfif  3608  ssbri  4104  nfbr  4106  mpteq12i  4148  ralxfr  4531  rexxfr  4533  nfiotaw  5255  nfriota  5932  nfov  5997  mpoeq123i  6031  mpoeq3ia  6033  disjsnxp  6346  tfri1  6474  eqer  6675  0er  6677  ecopover  6743  ecopoverg  6746  nfixpxy  6827  en2i  6884  en3i  6885  ener  6894  ensymb  6895  entr  6899  djuf1olem  7181  omp1eomlem  7222  infnninf  7252  ltsopi  7468  ltsonq  7546  enq0er  7583  ltpopr  7743  ltposr  7911  axcnex  8007  axaddf  8016  axmulf  8017  ltso  8185  nfneg  8304  negiso  9063  sup3exmid  9065  xrltso  9953  frecfzennn  10608  frechashgf1o  10610  0tonninf  10622  1tonninf  10623  nninfinf  10625  facnn  10909  fac0  10910  fac1  10911  cnrecnv  11336  cau3  11541  xrnegiso  11688  sum0  11814  trireciplem  11926  trirecip  11927  ege2le3  12097  oddpwdc  12611  modxai  12854  modsubi  12857  ennnfonelem1  12893  ennnfonelemhf1o  12899  strnfvn  12968  strslss  12995  prdsvallem  13219  prdsval  13220  mndprop  13388  grpprop  13465  isgrpi  13471  ablprop  13748  ringprop  13917  rlmfn  14330  cnfldstr  14435  cncrng  14446  cnfldui  14466  zringbas  14473  zringplusg  14474  dvdsrzring  14480  expghmap  14484  fnpsr  14544  txswaphmeolem  14907  divcnap  15152  expcn  15156  elcncf1ii  15167  cnrehmeocntop  15197  hovercncf  15233  dvid  15282  dvidre  15284  dveflem  15313  dvef  15314  sincn  15356  coscn  15357  cosz12  15367  sincos6thpi  15429  lgsdir2lem5  15624  bj-sttru  15876  bj-dctru  15889  bj-sbimeh  15908  bdnthALT  15970  012of  16130  2o01f  16131  isomninnlem  16171  iooref1o  16175  iswomninnlem  16190  ismkvnnlem  16193  dceqnconst  16201  dcapnconst  16202  taupi  16214