Theorem mptru 1344

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

Syntax hints:   → wi 4  ⊤wtru 1336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-tru 1338

This theorem is referenced by:  xorbi12i  1365  nfbi  1569  spime  1721  eubii  2015  nfmo  2026  mobii  2043  dvelimc  2321  ralbii  2463  rexbii  2464  nfralw  2494  nfralxy  2495  nfrexxy  2496  nfralya  2497  nfrexya  2498  nfreuxy  2631  nfsbc1  2954  nfsbc  2957  sbcbii  2996  csbeq2i  3058  nfcsb1  3063  nfcsbw  3067  nfcsb  3068  nfif  3533  ssbri  4008  nfbr  4010  mpteq12i  4052  ralxfr  4424  rexxfr  4426  nfiotaw  5136  nfriota  5783  nfov  5845  mpoeq123i  5878  mpoeq3ia  5880  disjsnxp  6178  tfri1  6306  eqer  6505  0er  6507  ecopover  6571  ecopoverg  6574  nfixpxy  6655  en2i  6708  en3i  6709  ener  6717  ensymb  6718  entr  6722  djuf1olem  6987  omp1eomlem  7028  infnninf  7056  ltsopi  7223  ltsonq  7301  enq0er  7338  ltpopr  7498  ltposr  7666  axcnex  7762  axaddf  7771  axmulf  7772  ltso  7938  nfneg  8055  negiso  8809  sup3exmid  8811  xrltso  9685  frecfzennn  10307  frechashgf1o  10309  0tonninf  10320  1tonninf  10321  facnn  10583  fac0  10584  fac1  10585  cnrecnv  10792  cau3  10997  xrnegiso  11141  sum0  11267  trireciplem  11379  trirecip  11380  ege2le3  11550  oddpwdc  12028  ennnfonelem1  12108  ennnfonelemhf1o  12114  strnfvn  12171  strslss  12197  txswaphmeolem  12680  divcnap  12915  elcncf1ii  12927  cnrehmeocntop  12953  dvid  13022  dveflem  13047  dvef  13048  sincn  13050  coscn  13051  cosz12  13061  sincos6thpi  13123  bj-sttru  13274  bj-dctru  13284  bj-sbimeh  13305  bdnthALT  13369  012of  13527  2o01f  13528  isomninnlem  13563  iooref1o  13567  iswomninnlem  13582  ismkvnnlem  13585  dceqnconst  13592  dcapnconst  13593  taupi  13603