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  2652  nfsbc1  2981  nfsbc  2984  sbcbii  3023  csbeq2i  3085  nfcsb1  3090  nfcsbw  3094  nfcsb  3095  nfif  3563  ssbri  4048  nfbr  4050  mpteq12i  4092  ralxfr  4467  rexxfr  4469  nfiotaw  5183  nfriota  5840  nfov  5905  mpoeq123i  5938  mpoeq3ia  5940  disjsnxp  6238  tfri1  6366  eqer  6567  0er  6569  ecopover  6633  ecopoverg  6636  nfixpxy  6717  en2i  6770  en3i  6771  ener  6779  ensymb  6780  entr  6784  djuf1olem  7052  omp1eomlem  7093  infnninf  7122  ltsopi  7319  ltsonq  7397  enq0er  7434  ltpopr  7594  ltposr  7762  axcnex  7858  axaddf  7867  axmulf  7868  ltso  8035  nfneg  8154  negiso  8912  sup3exmid  8914  xrltso  9796  frecfzennn  10426  frechashgf1o  10428  0tonninf  10439  1tonninf  10440  facnn  10707  fac0  10708  fac1  10709  cnrecnv  10919  cau3  11124  xrnegiso  11270  sum0  11396  trireciplem  11508  trirecip  11509  ege2le3  11679  oddpwdc  12174  ennnfonelem1  12408  ennnfonelemhf1o  12414  strnfvn  12483  strslss  12510  mndprop  12842  grpprop  12894  isgrpi  12900  ablprop  13100  ringprop  13219  cnfldstr  13460  cncrng  13466  zringbas  13489  zringplusg  13490  dvdsrzring  13496  txswaphmeolem  13823  divcnap  14058  elcncf1ii  14070  cnrehmeocntop  14096  dvid  14165  dveflem  14190  dvef  14191  sincn  14193  coscn  14194  cosz12  14204  sincos6thpi  14266  lgsdir2lem5  14436  bj-sttru  14495  bj-dctru  14508  bj-sbimeh  14527  bdnthALT  14590  012of  14748  2o01f  14749  isomninnlem  14781  iooref1o  14785  iswomninnlem  14800  ismkvnnlem  14803  dceqnconst  14810  dcapnconst  14811  taupi  14823