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  5970  nfov  6037  mpoeq123i  6073  mpoeq3ia  6075  disjsnxp  6389  tfri1  6517  eqer  6720  0er  6722  ecopover  6788  ecopoverg  6791  nfixpxy  6872  en2i  6929  en3i  6930  ener  6939  ensymb  6940  entr  6944  djuf1olem  7231  omp1eomlem  7272  infnninf  7302  ltsopi  7518  ltsonq  7596  enq0er  7633  ltpopr  7793  ltposr  7961  axcnex  8057  axaddf  8066  axmulf  8067  ltso  8235  nfneg  8354  negiso  9113  sup3exmid  9115  xrltso  10004  frecfzennn  10660  frechashgf1o  10662  0tonninf  10674  1tonninf  10675  nninfinf  10677  facnn  10961  fac0  10962  fac1  10963  cnrecnv  11437  cau3  11642  xrnegiso  11789  sum0  11915  trireciplem  12027  trirecip  12028  ege2le3  12198  oddpwdc  12712  modxai  12955  modsubi  12958  ennnfonelem1  12994  ennnfonelemhf1o  13000  strnfvn  13069  strslss  13096  prdsvallem  13321  prdsval  13322  mndprop  13490  grpprop  13567  isgrpi  13573  ablprop  13850  ringprop  14019  rlmfn  14433  cnfldstr  14538  cncrng  14549  cnfldui  14569  zringbas  14576  zringplusg  14577  dvdsrzring  14583  expghmap  14587  fnpsr  14647  txswaphmeolem  15010  divcnap  15255  expcn  15259  elcncf1ii  15270  cnrehmeocntop  15300  hovercncf  15336  dvid  15385  dvidre  15387  dveflem  15416  dvef  15417  sincn  15459  coscn  15460  cosz12  15470  sincos6thpi  15532  lgsdir2lem5  15727  bj-sttru  16187  bj-dctru  16200  bj-sbimeh  16219  bdnthALT  16281  012of  16444  2o01f  16445  isomninnlem  16486  iooref1o  16490  iswomninnlem  16505  ismkvnnlem  16508  dceqnconst  16516  dcapnconst  16517  taupi  16529