Theorem mptru 1357

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

Syntax hints:   → wi 4  ⊤wtru 1349

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 1351

This theorem is referenced by:  xorbi12i  1378  nfbi  1582  spime  1734  eubii  2028  nfmo  2039  mobii  2056  dvelimc  2334  ralbii  2476  rexbii  2477  nfralw  2507  nfralxy  2508  nfrexxy  2509  nfralya  2510  nfrexya  2511  nfreuxy  2644  nfsbc1  2972  nfsbc  2975  sbcbii  3014  csbeq2i  3076  nfcsb1  3081  nfcsbw  3085  nfcsb  3086  nfif  3554  ssbri  4033  nfbr  4035  mpteq12i  4077  ralxfr  4451  rexxfr  4453  nfiotaw  5164  nfriota  5818  nfov  5883  mpoeq123i  5916  mpoeq3ia  5918  disjsnxp  6216  tfri1  6344  eqer  6545  0er  6547  ecopover  6611  ecopoverg  6614  nfixpxy  6695  en2i  6748  en3i  6749  ener  6757  ensymb  6758  entr  6762  djuf1olem  7030  omp1eomlem  7071  infnninf  7100  ltsopi  7282  ltsonq  7360  enq0er  7397  ltpopr  7557  ltposr  7725  axcnex  7821  axaddf  7830  axmulf  7831  ltso  7997  nfneg  8116  negiso  8871  sup3exmid  8873  xrltso  9753  frecfzennn  10382  frechashgf1o  10384  0tonninf  10395  1tonninf  10396  facnn  10661  fac0  10662  fac1  10663  cnrecnv  10874  cau3  11079  xrnegiso  11225  sum0  11351  trireciplem  11463  trirecip  11464  ege2le3  11634  oddpwdc  12128  ennnfonelem1  12362  ennnfonelemhf1o  12368  strnfvn  12437  strslss  12463  mndprop  12677  grpprop  12725  isgrpi  12730  txswaphmeolem  13114  divcnap  13349  elcncf1ii  13361  cnrehmeocntop  13387  dvid  13456  dveflem  13481  dvef  13482  sincn  13484  coscn  13485  cosz12  13495  sincos6thpi  13557  lgsdir2lem5  13727  bj-sttru  13775  bj-dctru  13788  bj-sbimeh  13807  bdnthALT  13870  012of  14028  2o01f  14029  isomninnlem  14062  iooref1o  14066  iswomninnlem  14081  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092  taupi  14102