Theorem mptru 1406

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

Syntax hints:   → wi 4  ⊤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  5980  nfov  6047  mpoeq123i  6083  mpoeq3ia  6085  disjsnxp  6401  tfri1  6530  eqer  6733  0er  6735  ecopover  6801  ecopoverg  6804  nfixpxy  6885  en2i  6942  en3i  6943  ener  6952  ensymb  6953  entr  6957  djuf1olem  7251  omp1eomlem  7292  infnninf  7322  ltsopi  7539  ltsonq  7617  enq0er  7654  ltpopr  7814  ltposr  7982  axcnex  8078  axaddf  8087  axmulf  8088  ltso  8256  nfneg  8375  negiso  9134  sup3exmid  9136  xrltso  10030  frecfzennn  10687  frechashgf1o  10689  0tonninf  10701  1tonninf  10702  nninfinf  10704  facnn  10988  fac0  10989  fac1  10990  cnrecnv  11470  cau3  11675  xrnegiso  11822  sum0  11948  trireciplem  12060  trirecip  12061  ege2le3  12231  oddpwdc  12745  modxai  12988  modsubi  12991  ennnfonelem1  13027  ennnfonelemhf1o  13033  strnfvn  13102  strslss  13129  prdsvallem  13354  prdsval  13355  mndprop  13523  grpprop  13600  isgrpi  13606  ablprop  13883  ringprop  14052  rlmfn  14466  cnfldstr  14571  cncrng  14582  cnfldui  14602  zringbas  14609  zringplusg  14610  dvdsrzring  14616  expghmap  14620  fnpsr  14680  txswaphmeolem  15043  divcnap  15288  expcn  15292  elcncf1ii  15303  cnrehmeocntop  15333  hovercncf  15369  dvid  15418  dvidre  15420  dveflem  15449  dvef  15450  sincn  15492  coscn  15493  cosz12  15503  sincos6thpi  15565  lgsdir2lem5  15760  bj-sttru  16336  bj-dctru  16349  bj-sbimeh  16368  bdnthALT  16430  012of  16592  2o01f  16593  isomninnlem  16634  iooref1o  16638  iswomninnlem  16653  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665  taupi  16677