Theorem mptru 1411

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

Syntax hints:   -> wi 4   T. wtru 1403

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 1405

This theorem is referenced by:  xorbi12i  1432  dcfromcon  1498  nfbi  1642  spime  1794  eubii  2095  nfmo  2106  mobii  2123  eqabi  2371  dvelimc  2414  ralbii  2556  rexbii  2557  nfralw  2587  nfralxy  2588  nfrexw  2589  nfralya  2590  nfrexya  2591  nfreuw  2726  rabbia2  2806  nfsbc1  3069  nfsbc  3072  sbcbii  3111  csbeq2i  3174  nfcsb1  3179  nfsbcw  3182  nfcsbw  3184  nfcsb  3185  nfif  3666  ssbri  4170  nfbr  4172  mpteq12i  4214  ralxfr  4607  rexxfr  4609  nfiotaw  5336  nfriota  6038  nfov  6105  mpoeq123i  6141  mpoeq3ia  6143  disjsnxp  6463  tfri1  6626  eqer  6829  0er  6831  ecopover  6897  ecopoverg  6900  nfixpxy  6989  en2i  7046  en3i  7047  ener  7056  ensymb  7057  entr  7061  djuf1olem  7383  omp1eomlem  7424  infnninf  7454  ltsopi  7677  ltsonq  7755  enq0er  7792  ltpopr  7952  ltposr  8120  axcnex  8216  axaddf  8225  axmulf  8226  ltso  8393  nfneg  8513  negiso  9275  sup3exmid  9277  xrltso  10177  frecfzennn  10841  frechashgf1o  10843  0tonninf  10855  1tonninf  10856  nninfinf  10858  facnn  11143  fac0  11144  fac1  11145  cnrecnv  11654  cau3  11859  xrnegiso  12006  sum0  12133  trireciplem  12245  trirecip  12246  ege2le3  12416  oddpwdc  12930  modxai  13173  modsubi  13176  ballotfilemofi  13197  ballotfilem2  13206  ballotfilemefi  13215  ballotfilemafi  13216  ballotfilembfi  13217  ballotfilemrinv  13255  ennnfonelem1  13276  ennnfonelemhf1o  13282  strnfvn  13351  strslss  13378  prdsvallem  13598  mndprop  13731  grpprop  13800  isgrpi  13806  ablprop  14077  prdsval  14150  ringprop  14318  rlmfn  14762  cnfldstr  14867  cncrng  14878  cnfldui  14896  zringbas  14903  zringplusg  14904  dvdsrzring  14910  expghmap  14914  fnpsr  14974  txswaphmeolem  15344  divcnap  15589  expcn  15593  elcncf1ii  15604  cnrehmeocntop  15634  hovercncf  15670  dvid  15719  dvidre  15721  dveflem  15750  dvef  15751  sincn  15793  coscn  15794  cosz12  15804  sincos6thpi  15866  lgsdir2lem5  16065  konigsbergvtx  16637  konigsbergiedg  16638  konigsbergiedgwen  16639  konigsbergumgr  16642  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  konigsberg  16648  bj-sttru  16682  bj-dctru  16695  bj-sbimeh  16714  bdnthALT  16775  012of  16937  2o01f  16938  isomninnlem  16984  iooref1o  16988  iswomninnlem  17004  ismkvnnlem  17007  dceqnconst  17015  dcapnconst  17016  taupi  17028