Theorem mptru 1406

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

Syntax hints:   -> wi 4   T. wtru 1398

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 1400

This theorem is referenced by:  xorbi12i  1427  dcfromcon  1493  nfbi  1637  spime  1789  eubii  2088  nfmo  2099  mobii  2116  dvelimc  2396  ralbii  2538  rexbii  2539  nfralw  2569  nfralxy  2570  nfrexw  2571  nfralya  2572  nfrexya  2573  nfreuw  2708  rabbia2  2787  nfsbc1  3049  nfsbc  3052  sbcbii  3091  csbeq2i  3154  nfcsb1  3159  nfsbcw  3162  nfcsbw  3164  nfcsb  3165  nfif  3634  ssbri  4133  nfbr  4135  mpteq12i  4177  ralxfr  4563  rexxfr  4565  nfiotaw  5290  nfriota  5981  nfov  6048  mpoeq123i  6084  mpoeq3ia  6086  disjsnxp  6402  tfri1  6531  eqer  6734  0er  6736  ecopover  6802  ecopoverg  6805  nfixpxy  6886  en2i  6943  en3i  6944  ener  6953  ensymb  6954  entr  6958  djuf1olem  7252  omp1eomlem  7293  infnninf  7323  ltsopi  7540  ltsonq  7618  enq0er  7655  ltpopr  7815  ltposr  7983  axcnex  8079  axaddf  8088  axmulf  8089  ltso  8257  nfneg  8376  negiso  9135  sup3exmid  9137  xrltso  10031  frecfzennn  10689  frechashgf1o  10691  0tonninf  10703  1tonninf  10704  nninfinf  10706  facnn  10990  fac0  10991  fac1  10992  cnrecnv  11488  cau3  11693  xrnegiso  11840  sum0  11967  trireciplem  12079  trirecip  12080  ege2le3  12250  oddpwdc  12764  modxai  13007  modsubi  13010  ennnfonelem1  13046  ennnfonelemhf1o  13052  strnfvn  13121  strslss  13148  prdsvallem  13373  prdsval  13374  mndprop  13542  grpprop  13619  isgrpi  13625  ablprop  13902  ringprop  14072  rlmfn  14486  cnfldstr  14591  cncrng  14602  cnfldui  14622  zringbas  14629  zringplusg  14630  dvdsrzring  14636  expghmap  14640  fnpsr  14700  txswaphmeolem  15063  divcnap  15308  expcn  15312  elcncf1ii  15323  cnrehmeocntop  15353  hovercncf  15389  dvid  15438  dvidre  15440  dveflem  15469  dvef  15470  sincn  15512  coscn  15513  cosz12  15523  sincos6thpi  15585  lgsdir2lem5  15780  konigsbergvtx  16352  konigsbergiedg  16353  konigsbergiedgwen  16354  konigsbergumgr  16357  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  konigsberg  16363  bj-sttru  16387  bj-dctru  16400  bj-sbimeh  16419  bdnthALT  16481  012of  16643  2o01f  16644  isomninnlem  16685  iooref1o  16689  iswomninnlem  16705  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717  taupi  16729