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  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  7295  omp1eomlem  7336  infnninf  7366  ltsopi  7583  ltsonq  7661  enq0er  7698  ltpopr  7858  ltposr  8026  axcnex  8122  axaddf  8131  axmulf  8132  ltso  8299  nfneg  8418  negiso  9177  sup3exmid  9179  xrltso  10075  frecfzennn  10734  frechashgf1o  10736  0tonninf  10748  1tonninf  10749  nninfinf  10751  facnn  11035  fac0  11036  fac1  11037  cnrecnv  11533  cau3  11738  xrnegiso  11885  sum0  12012  trireciplem  12124  trirecip  12125  ege2le3  12295  oddpwdc  12809  modxai  13052  modsubi  13055  ennnfonelem1  13091  ennnfonelemhf1o  13097  strnfvn  13166  strslss  13193  prdsvallem  13418  prdsval  13419  mndprop  13587  grpprop  13664  isgrpi  13670  ablprop  13947  ringprop  14117  rlmfn  14532  cnfldstr  14637  cncrng  14648  cnfldui  14668  zringbas  14675  zringplusg  14676  dvdsrzring  14682  expghmap  14686  fnpsr  14746  txswaphmeolem  15114  divcnap  15359  expcn  15363  elcncf1ii  15374  cnrehmeocntop  15404  hovercncf  15440  dvid  15489  dvidre  15491  dveflem  15520  dvef  15521  sincn  15563  coscn  15564  cosz12  15574  sincos6thpi  15636  lgsdir2lem5  15834  konigsbergvtx  16406  konigsbergiedg  16407  konigsbergiedgwen  16408  konigsbergumgr  16411  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  konigsberg  16417  bj-sttru  16441  bj-dctru  16454  bj-sbimeh  16473  bdnthALT  16534  012of  16696  2o01f  16697  isomninnlem  16745  iooref1o  16749  iswomninnlem  16765  ismkvnnlem  16768  dceqnconst  16776  dcapnconst  16777  taupi  16789