Theorem mptru 1407

Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.)

Hypothesis

Ref	Expression
mptru.1	⊢ (⊤ → 𝜑)

Assertion

Ref	Expression
mptru	⊢ 𝜑

Proof of Theorem mptru

Step	Hyp	Ref	Expression
1		tru 1402	. 2 ⊢ ⊤
2		mptru.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤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  1790  eubii  2091  nfmo  2102  mobii  2119  eqabi  2367  dvelimc  2408  ralbii  2550  rexbii  2551  nfralw  2581  nfralxy  2582  nfrexw  2583  nfralya  2584  nfrexya  2585  nfreuw  2720  rabbia2  2800  nfsbc1  3063  nfsbc  3066  sbcbii  3105  csbeq2i  3168  nfcsb1  3173  nfsbcw  3176  nfcsbw  3178  nfcsb  3179  nfif  3655  ssbri  4159  nfbr  4161  mpteq12i  4203  ralxfr  4592  rexxfr  4594  nfiotaw  5321  nfriota  6021  nfov  6088  mpoeq123i  6124  mpoeq3ia  6126  disjsnxp  6446  tfri1  6609  eqer  6812  0er  6814  ecopover  6880  ecopoverg  6883  nfixpxy  6965  en2i  7022  en3i  7023  ener  7032  ensymb  7033  entr  7037  djuf1olem  7357  omp1eomlem  7398  infnninf  7428  ltsopi  7651  ltsonq  7729  enq0er  7766  ltpopr  7926  ltposr  8094  axcnex  8190  axaddf  8199  axmulf  8200  ltso  8367  nfneg  8486  negiso  9246  sup3exmid  9248  xrltso  10148  frecfzennn  10812  frechashgf1o  10814  0tonninf  10826  1tonninf  10827  nninfinf  10829  facnn  11114  fac0  11115  fac1  11116  cnrecnv  11620  cau3  11825  xrnegiso  11972  sum0  12099  trireciplem  12211  trirecip  12212  ege2le3  12382  oddpwdc  12896  modxai  13139  modsubi  13142  ballotfilemofi  13163  ballotfilem2  13172  ballotfilemefi  13181  ballotfilemafi  13182  ballotfilembfi  13183  ballotfilemrinv  13221  ennnfonelem1  13242  ennnfonelemhf1o  13248  strnfvn  13317  strslss  13344  prdsvallem  13564  mndprop  13702  grpprop  13773  isgrpi  13779  ablprop  14050  prdsval  14115  ringprop  14283  rlmfn  14727  cnfldstr  14832  cncrng  14843  cnfldui  14863  zringbas  14870  zringplusg  14871  dvdsrzring  14877  expghmap  14881  fnpsr  14941  txswaphmeolem  15311  divcnap  15556  expcn  15560  elcncf1ii  15571  cnrehmeocntop  15601  hovercncf  15637  dvid  15686  dvidre  15688  dveflem  15717  dvef  15718  sincn  15760  coscn  15761  cosz12  15771  sincos6thpi  15833  lgsdir2lem5  16031  konigsbergvtx  16603  konigsbergiedg  16604  konigsbergiedgwen  16605  konigsbergumgr  16608  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  konigsberg  16614  bj-sttru  16638  bj-dctru  16651  bj-sbimeh  16670  bdnthALT  16731  012of  16893  2o01f  16894  isomninnlem  16940  iooref1o  16944  iswomninnlem  16960  ismkvnnlem  16963  dceqnconst  16972  dcapnconst  16973  taupi  16985