Theorem mptru 1407

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

Syntax hints:   -> wi 4   T. wtru 1399

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 1401

This theorem is referenced by:  xorbi12i  1428  dcfromcon  1494  nfbi  1638  spime  1789  eubii  2088  nfmo  2099  mobii  2116  dvelimc  2397  ralbii  2539  rexbii  2540  nfralw  2570  nfralxy  2571  nfrexw  2572  nfralya  2573  nfrexya  2574  nfreuw  2709  rabbia2  2788  nfsbc1  3050  nfsbc  3053  sbcbii  3092  csbeq2i  3155  nfcsb1  3160  nfsbcw  3163  nfcsbw  3165  nfcsb  3166  nfif  3638  ssbri  4138  nfbr  4140  mpteq12i  4182  ralxfr  4569  rexxfr  4571  nfiotaw  5297  nfriota  5991  nfov  6058  mpoeq123i  6094  mpoeq3ia  6096  disjsnxp  6411  tfri1  6574  eqer  6777  0er  6779  ecopover  6845  ecopoverg  6848  nfixpxy  6929  en2i  6986  en3i  6987  ener  6996  ensymb  6997  entr  7001  djuf1olem  7312  omp1eomlem  7353  infnninf  7383  ltsopi  7600  ltsonq  7678  enq0er  7715  ltpopr  7875  ltposr  8043  axcnex  8139  axaddf  8148  axmulf  8149  ltso  8316  nfneg  8435  negiso  9194  sup3exmid  9196  xrltso  10092  frecfzennn  10751  frechashgf1o  10753  0tonninf  10765  1tonninf  10766  nninfinf  10768  facnn  11052  fac0  11053  fac1  11054  cnrecnv  11550  cau3  11755  xrnegiso  11902  sum0  12029  trireciplem  12141  trirecip  12142  ege2le3  12312  oddpwdc  12826  modxai  13069  modsubi  13072  ennnfonelem1  13108  ennnfonelemhf1o  13114  strnfvn  13183  strslss  13210  prdsvallem  13435  prdsval  13436  mndprop  13604  grpprop  13681  isgrpi  13687  ablprop  13964  ringprop  14134  rlmfn  14549  cnfldstr  14654  cncrng  14665  cnfldui  14685  zringbas  14692  zringplusg  14693  dvdsrzring  14699  expghmap  14703  fnpsr  14763  txswaphmeolem  15131  divcnap  15376  expcn  15380  elcncf1ii  15391  cnrehmeocntop  15421  hovercncf  15457  dvid  15506  dvidre  15508  dveflem  15537  dvef  15538  sincn  15580  coscn  15581  cosz12  15591  sincos6thpi  15653  lgsdir2lem5  15851  konigsbergvtx  16423  konigsbergiedg  16424  konigsbergiedgwen  16425  konigsbergumgr  16428  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  konigsberglem5  16433  konigsberg  16434  bj-sttru  16458  bj-dctru  16471  bj-sbimeh  16490  bdnthALT  16551  012of  16713  2o01f  16714  isomninnlem  16762  iooref1o  16766  iswomninnlem  16782  ismkvnnlem  16785  dceqnconst  16793  dcapnconst  16794  taupi  16806