Theorem mptru 1411

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

This proof depends on syntax axioms:   -> wi 4   T. wtru 1403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-tru 1405

This theorem is used by:  xorbi12i  1432  dcfromcon  1498  nfbi  1642  spime  1794  eubii  2095  nfmo  2106  mobii  2123  eqabi  2371  dvelimc  2414  ralbii  2556  rexbii  2557  nfralw  2587  nfralxy  2588  nfrexw  2589  nfralya  2590  nfrexya  2591  nfreuw  2726  rabbia2  2806  nfsbc1  3069  nfsbc  3072  sbcbii  3111  csbeq2i  3174  nfcsb1  3179  nfsbcw  3182  nfcsbw  3184  nfcsb  3185  nfif  3669  ssbri  4176  nfbr  4178  mpteq1i  4218  mpteq12i  4221  ralxfr  4614  rexxfr  4616  nfiotaw  5344  nfriota  6051  nfov  6118  mpoeq123i  6154  mpoeq3ia  6156  disjsnxp  6477  tfri1  6640  eqer  6843  0er  6845  ecopover  6911  ecopoverg  6914  nfixpxy  7003  en2i  7060  en3i  7061  ener  7070  ensymb  7071  entr  7075  djuf1olem  7399  omp1eomlem  7440  infnninf  7470  ltsopi  7693  ltsonq  7771  enq0er  7808  ltpopr  7968  ltposr  8136  axcnex  8232  axaddf  8241  axmulf  8242  ltso  8409  nfneg  8530  negiso  9293  sup3exmid  9295  xrltso  10215  frecfzennn  10884  frechashgf1o  10886  0tonninf  10898  1tonninf  10899  nninfinf  10901  facnn  11187  fac0  11188  fac1  11189  cnrecnv  11698  cau3  11904  xrnegiso  12053  sum0  12180  trireciplem  12292  trirecip  12293  ege2le3  12463  modxai  13224  modsubi  13228  ballotfilemofi  13277  ballotfilem2  13286  ballotfilemefi  13295  ballotfilemafi  13296  ballotfilembfi  13297  ballotfilemrinv  13335  ennnfonelem1  13356  ennnfonelemhf1o  13362  strnfvn  13431  strslss  13458  prdsvallem  13680  mndprop  13813  grpprop  13882  isgrpi  13888  ablprop  14190  prdsval  14280  ringprop  14452  rlmfn  14899  cnfldstr  15004  cncrng  15015  cnfldui  15033  zringbas  15040  zringplusg  15041  dvdsrzring  15047  expghmap  15051  fnpsr  15160  txswaphmeolem  15546  divcnap  15791  expcn  15795  elcncf1ii  15806  cnrehmeocntop  15836  hovercncf  15872  dvid  15921  dvidre  15923  dveflem  15952  dvef  15953  sincn  15995  coscn  15996  cosz12  16007  sincos6thpi  16069  log2ublem2  16222  log2ublog2  16224  lgsdir2lem5  16356  konigsbergvtx  16928  konigsbergiedg  16929  konigsbergiedgwen  16930  konigsbergumgr  16933  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  konigsberg  16939  bj-sttru  16973  bj-dctru  16986  bj-sbimeh  17005  bdnthALT  17066  012of  17228  2o01f  17229  isomninnlem  17285  iooref1o  17289  iswomninnlem  17306  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318  taupi  17330