Theorem mptru 1404

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

Syntax hints:   -> wi 4   T. wtru 1396

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 1398

This theorem is referenced by:  xorbi12i  1425  dcfromcon  1491  nfbi  1635  spime  1787  eubii  2086  nfmo  2097  mobii  2114  dvelimc  2394  ralbii  2536  rexbii  2537  nfralw  2567  nfralxy  2568  nfrexw  2569  nfralya  2570  nfrexya  2571  nfreuw  2706  nfsbc1  3046  nfsbc  3049  sbcbii  3088  csbeq2i  3151  nfcsb1  3156  nfsbcw  3159  nfcsbw  3161  nfcsb  3162  nfif  3631  ssbri  4128  nfbr  4130  mpteq12i  4172  ralxfr  4557  rexxfr  4559  nfiotaw  5282  nfriota  5964  nfov  6031  mpoeq123i  6067  mpoeq3ia  6069  disjsnxp  6383  tfri1  6511  eqer  6712  0er  6714  ecopover  6780  ecopoverg  6783  nfixpxy  6864  en2i  6921  en3i  6922  ener  6931  ensymb  6932  entr  6936  djuf1olem  7220  omp1eomlem  7261  infnninf  7291  ltsopi  7507  ltsonq  7585  enq0er  7622  ltpopr  7782  ltposr  7950  axcnex  8046  axaddf  8055  axmulf  8056  ltso  8224  nfneg  8343  negiso  9102  sup3exmid  9104  xrltso  9992  frecfzennn  10648  frechashgf1o  10650  0tonninf  10662  1tonninf  10663  nninfinf  10665  facnn  10949  fac0  10950  fac1  10951  cnrecnv  11421  cau3  11626  xrnegiso  11773  sum0  11899  trireciplem  12011  trirecip  12012  ege2le3  12182  oddpwdc  12696  modxai  12939  modsubi  12942  ennnfonelem1  12978  ennnfonelemhf1o  12984  strnfvn  13053  strslss  13080  prdsvallem  13305  prdsval  13306  mndprop  13474  grpprop  13551  isgrpi  13557  ablprop  13834  ringprop  14003  rlmfn  14417  cnfldstr  14522  cncrng  14533  cnfldui  14553  zringbas  14560  zringplusg  14561  dvdsrzring  14567  expghmap  14571  fnpsr  14631  txswaphmeolem  14994  divcnap  15239  expcn  15243  elcncf1ii  15254  cnrehmeocntop  15284  hovercncf  15320  dvid  15369  dvidre  15371  dveflem  15400  dvef  15401  sincn  15443  coscn  15444  cosz12  15454  sincos6thpi  15516  lgsdir2lem5  15711  bj-sttru  16104  bj-dctru  16117  bj-sbimeh  16136  bdnthALT  16198  012of  16357  2o01f  16358  isomninnlem  16398  iooref1o  16402  iswomninnlem  16417  ismkvnnlem  16420  dceqnconst  16428  dcapnconst  16429  taupi  16441