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  1468  nfbi  1612  spime  1764  eubii  2063  nfmo  2074  mobii  2091  dvelimc  2370  ralbii  2512  rexbii  2513  nfralw  2543  nfralxy  2544  nfrexw  2545  nfralya  2546  nfrexya  2547  nfreuxy  2681  nfsbc1  3016  nfsbc  3019  sbcbii  3058  csbeq2i  3120  nfcsb1  3125  nfsbcw  3128  nfcsbw  3130  nfcsb  3131  nfif  3599  ssbri  4089  nfbr  4091  mpteq12i  4133  ralxfr  4514  rexxfr  4516  nfiotaw  5237  nfriota  5911  nfov  5976  mpoeq123i  6010  mpoeq3ia  6012  disjsnxp  6325  tfri1  6453  eqer  6654  0er  6656  ecopover  6722  ecopoverg  6725  nfixpxy  6806  en2i  6863  en3i  6864  ener  6873  ensymb  6874  entr  6878  djuf1olem  7157  omp1eomlem  7198  infnninf  7228  ltsopi  7435  ltsonq  7513  enq0er  7550  ltpopr  7710  ltposr  7878  axcnex  7974  axaddf  7983  axmulf  7984  ltso  8152  nfneg  8271  negiso  9030  sup3exmid  9032  xrltso  9920  frecfzennn  10573  frechashgf1o  10575  0tonninf  10587  1tonninf  10588  nninfinf  10590  facnn  10874  fac0  10875  fac1  10876  cnrecnv  11254  cau3  11459  xrnegiso  11606  sum0  11732  trireciplem  11844  trirecip  11845  ege2le3  12015  oddpwdc  12529  modxai  12772  modsubi  12775  ennnfonelem1  12811  ennnfonelemhf1o  12817  strnfvn  12886  strslss  12913  prdsvallem  13137  prdsval  13138  mndprop  13306  grpprop  13383  isgrpi  13389  ablprop  13666  ringprop  13835  rlmfn  14248  cnfldstr  14353  cncrng  14364  cnfldui  14384  zringbas  14391  zringplusg  14392  dvdsrzring  14398  expghmap  14402  fnpsr  14462  txswaphmeolem  14825  divcnap  15070  expcn  15074  elcncf1ii  15085  cnrehmeocntop  15115  hovercncf  15151  dvid  15200  dvidre  15202  dveflem  15231  dvef  15232  sincn  15274  coscn  15275  cosz12  15285  sincos6thpi  15347  lgsdir2lem5  15542  bj-sttru  15713  bj-dctru  15726  bj-sbimeh  15745  bdnthALT  15808  012of  15967  2o01f  15968  isomninnlem  16006  iooref1o  16010  iswomninnlem  16025  ismkvnnlem  16028  dceqnconst  16036  dcapnconst  16037  taupi  16049