Theorem mptru 1362

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

Syntax hints:   -> wi 4   T. wtru 1354

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 1356

This theorem is referenced by:  xorbi12i  1383  nfbi  1589  spime  1741  eubii  2035  nfmo  2046  mobii  2063  dvelimc  2341  ralbii  2483  rexbii  2484  nfralw  2514  nfralxy  2515  nfrexxy  2516  nfralya  2517  nfrexya  2518  nfreuxy  2651  nfsbc1  2980  nfsbc  2983  sbcbii  3022  csbeq2i  3084  nfcsb1  3089  nfcsbw  3093  nfcsb  3094  nfif  3562  ssbri  4045  nfbr  4047  mpteq12i  4089  ralxfr  4464  rexxfr  4466  nfiotaw  5179  nfriota  5835  nfov  5900  mpoeq123i  5933  mpoeq3ia  5935  disjsnxp  6233  tfri1  6361  eqer  6562  0er  6564  ecopover  6628  ecopoverg  6631  nfixpxy  6712  en2i  6765  en3i  6766  ener  6774  ensymb  6775  entr  6779  djuf1olem  7047  omp1eomlem  7088  infnninf  7117  ltsopi  7314  ltsonq  7392  enq0er  7429  ltpopr  7589  ltposr  7757  axcnex  7853  axaddf  7862  axmulf  7863  ltso  8029  nfneg  8148  negiso  8906  sup3exmid  8908  xrltso  9790  frecfzennn  10419  frechashgf1o  10421  0tonninf  10432  1tonninf  10433  facnn  10698  fac0  10699  fac1  10700  cnrecnv  10910  cau3  11115  xrnegiso  11261  sum0  11387  trireciplem  11499  trirecip  11500  ege2le3  11670  oddpwdc  12164  ennnfonelem1  12398  ennnfonelemhf1o  12404  strnfvn  12473  strslss  12500  mndprop  12772  grpprop  12822  isgrpi  12828  ablprop  13000  ringprop  13119  cnfldstr  13262  cncrng  13268  txswaphmeolem  13602  divcnap  13837  elcncf1ii  13849  cnrehmeocntop  13875  dvid  13944  dveflem  13969  dvef  13970  sincn  13972  coscn  13973  cosz12  13983  sincos6thpi  14045  lgsdir2lem5  14215  bj-sttru  14263  bj-dctru  14276  bj-sbimeh  14295  bdnthALT  14358  012of  14516  2o01f  14517  isomninnlem  14549  iooref1o  14553  iswomninnlem  14568  ismkvnnlem  14571  dceqnconst  14578  dcapnconst  14579  taupi  14591