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  4558  rexxfr  4560  nfiotaw  5285  nfriota  5973  nfov  6040  mpoeq123i  6076  mpoeq3ia  6078  disjsnxp  6394  tfri1  6522  eqer  6725  0er  6727  ecopover  6793  ecopoverg  6796  nfixpxy  6877  en2i  6934  en3i  6935  ener  6944  ensymb  6945  entr  6949  djuf1olem  7236  omp1eomlem  7277  infnninf  7307  ltsopi  7523  ltsonq  7601  enq0er  7638  ltpopr  7798  ltposr  7966  axcnex  8062  axaddf  8071  axmulf  8072  ltso  8240  nfneg  8359  negiso  9118  sup3exmid  9120  xrltso  10009  frecfzennn  10665  frechashgf1o  10667  0tonninf  10679  1tonninf  10680  nninfinf  10682  facnn  10966  fac0  10967  fac1  10968  cnrecnv  11442  cau3  11647  xrnegiso  11794  sum0  11920  trireciplem  12032  trirecip  12033  ege2le3  12203  oddpwdc  12717  modxai  12960  modsubi  12963  ennnfonelem1  12999  ennnfonelemhf1o  13005  strnfvn  13074  strslss  13101  prdsvallem  13326  prdsval  13327  mndprop  13495  grpprop  13572  isgrpi  13578  ablprop  13855  ringprop  14024  rlmfn  14438  cnfldstr  14543  cncrng  14554  cnfldui  14574  zringbas  14581  zringplusg  14582  dvdsrzring  14588  expghmap  14592  fnpsr  14652  txswaphmeolem  15015  divcnap  15260  expcn  15264  elcncf1ii  15275  cnrehmeocntop  15305  hovercncf  15341  dvid  15390  dvidre  15392  dveflem  15421  dvef  15422  sincn  15464  coscn  15465  cosz12  15475  sincos6thpi  15537  lgsdir2lem5  15732  bj-sttru  16213  bj-dctru  16226  bj-sbimeh  16245  bdnthALT  16307  012of  16470  2o01f  16471  isomninnlem  16512  iooref1o  16516  iswomninnlem  16531  ismkvnnlem  16534  dceqnconst  16542  dcapnconst  16543  taupi  16555