Theorem mptru 1404

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 1399	. 2 ⊢ ⊤
2		mptru.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1396

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 1398

This theorem is referenced by:  xorbi12i  1425  dcfromcon  1491  nfbi  1635  spime  1787  eubii  2086  nfmo  2097  mobii  2114  dvelimc  2394  ralbii  2536  rexbii  2537  nfralw  2567  nfralxy  2568  nfrexw  2569  nfralya  2570  nfrexya  2571  nfreuw  2706  rabbia2  2785  nfsbc1  3047  nfsbc  3050  sbcbii  3089  csbeq2i  3152  nfcsb1  3157  nfsbcw  3160  nfcsbw  3162  nfcsb  3163  nfif  3632  ssbri  4131  nfbr  4133  mpteq12i  4175  ralxfr  4561  rexxfr  4563  nfiotaw  5288  nfriota  5976  nfov  6043  mpoeq123i  6079  mpoeq3ia  6081  disjsnxp  6397  tfri1  6526  eqer  6729  0er  6731  ecopover  6797  ecopoverg  6800  nfixpxy  6881  en2i  6938  en3i  6939  ener  6948  ensymb  6949  entr  6953  djuf1olem  7243  omp1eomlem  7284  infnninf  7314  ltsopi  7530  ltsonq  7608  enq0er  7645  ltpopr  7805  ltposr  7973  axcnex  8069  axaddf  8078  axmulf  8079  ltso  8247  nfneg  8366  negiso  9125  sup3exmid  9127  xrltso  10021  frecfzennn  10678  frechashgf1o  10680  0tonninf  10692  1tonninf  10693  nninfinf  10695  facnn  10979  fac0  10980  fac1  10981  cnrecnv  11461  cau3  11666  xrnegiso  11813  sum0  11939  trireciplem  12051  trirecip  12052  ege2le3  12222  oddpwdc  12736  modxai  12979  modsubi  12982  ennnfonelem1  13018  ennnfonelemhf1o  13024  strnfvn  13093  strslss  13120  prdsvallem  13345  prdsval  13346  mndprop  13514  grpprop  13591  isgrpi  13597  ablprop  13874  ringprop  14043  rlmfn  14457  cnfldstr  14562  cncrng  14573  cnfldui  14593  zringbas  14600  zringplusg  14601  dvdsrzring  14607  expghmap  14611  fnpsr  14671  txswaphmeolem  15034  divcnap  15279  expcn  15283  elcncf1ii  15294  cnrehmeocntop  15324  hovercncf  15360  dvid  15409  dvidre  15411  dveflem  15440  dvef  15441  sincn  15483  coscn  15484  cosz12  15494  sincos6thpi  15556  lgsdir2lem5  15751  bj-sttru  16272  bj-dctru  16285  bj-sbimeh  16304  bdnthALT  16366  012of  16528  2o01f  16529  isomninnlem  16570  iooref1o  16574  iswomninnlem  16589  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601  taupi  16613