Theorem mptru 1381

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

Syntax hints:   → wi 4  ⊤wtru 1373

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 1375

This theorem is referenced by:  xorbi12i  1402  dcfromcon  1467  nfbi  1611  spime  1763  eubii  2062  nfmo  2073  mobii  2090  dvelimc  2369  ralbii  2511  rexbii  2512  nfralw  2542  nfralxy  2543  nfrexw  2544  nfralya  2545  nfrexya  2546  nfreuxy  2680  nfsbc1  3015  nfsbc  3018  sbcbii  3057  csbeq2i  3119  nfcsb1  3124  nfsbcw  3127  nfcsbw  3129  nfcsb  3130  nfif  3598  ssbri  4087  nfbr  4089  mpteq12i  4131  ralxfr  4512  rexxfr  4514  nfiotaw  5235  nfriota  5908  nfov  5973  mpoeq123i  6007  mpoeq3ia  6009  disjsnxp  6322  tfri1  6450  eqer  6651  0er  6653  ecopover  6719  ecopoverg  6722  nfixpxy  6803  en2i  6860  en3i  6861  ener  6870  ensymb  6871  entr  6875  djuf1olem  7154  omp1eomlem  7195  infnninf  7225  ltsopi  7432  ltsonq  7510  enq0er  7547  ltpopr  7707  ltposr  7875  axcnex  7971  axaddf  7980  axmulf  7981  ltso  8149  nfneg  8268  negiso  9027  sup3exmid  9029  xrltso  9917  frecfzennn  10569  frechashgf1o  10571  0tonninf  10583  1tonninf  10584  nninfinf  10586  facnn  10870  fac0  10871  fac1  10872  cnrecnv  11163  cau3  11368  xrnegiso  11515  sum0  11641  trireciplem  11753  trirecip  11754  ege2le3  11924  oddpwdc  12438  modxai  12681  modsubi  12684  ennnfonelem1  12720  ennnfonelemhf1o  12726  strnfvn  12795  strslss  12822  prdsvallem  13046  prdsval  13047  mndprop  13215  grpprop  13292  isgrpi  13298  ablprop  13575  ringprop  13744  rlmfn  14157  cnfldstr  14262  cncrng  14273  cnfldui  14293  zringbas  14300  zringplusg  14301  dvdsrzring  14307  expghmap  14311  fnpsr  14371  txswaphmeolem  14734  divcnap  14979  expcn  14983  elcncf1ii  14994  cnrehmeocntop  15024  hovercncf  15060  dvid  15109  dvidre  15111  dveflem  15140  dvef  15141  sincn  15183  coscn  15184  cosz12  15194  sincos6thpi  15256  lgsdir2lem5  15451  bj-sttru  15609  bj-dctru  15622  bj-sbimeh  15641  bdnthALT  15704  012of  15863  2o01f  15864  isomninnlem  15902  iooref1o  15906  iswomninnlem  15921  ismkvnnlem  15924  dceqnconst  15932  dcapnconst  15933  taupi  15945