Theorem mptru 1407

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

Syntax hints:   → wi 4  ⊤wtru 1399

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 1401

This theorem is referenced by:  xorbi12i  1428  dcfromcon  1494  nfbi  1638  spime  1790  eubii  2091  nfmo  2102  mobii  2119  eqabi  2367  dvelimc  2408  ralbii  2550  rexbii  2551  nfralw  2581  nfralxy  2582  nfrexw  2583  nfralya  2584  nfrexya  2585  nfreuw  2720  rabbia2  2800  nfsbc1  3063  nfsbc  3066  sbcbii  3105  csbeq2i  3168  nfcsb1  3173  nfsbcw  3176  nfcsbw  3178  nfcsb  3179  nfif  3656  ssbri  4160  nfbr  4162  mpteq12i  4204  ralxfr  4593  rexxfr  4595  nfiotaw  5322  nfriota  6022  nfov  6089  mpoeq123i  6125  mpoeq3ia  6127  disjsnxp  6447  tfri1  6610  eqer  6813  0er  6815  ecopover  6881  ecopoverg  6884  nfixpxy  6966  en2i  7023  en3i  7024  ener  7033  ensymb  7034  entr  7038  djuf1olem  7358  omp1eomlem  7399  infnninf  7429  ltsopi  7652  ltsonq  7730  enq0er  7767  ltpopr  7927  ltposr  8095  axcnex  8191  axaddf  8200  axmulf  8201  ltso  8368  nfneg  8488  negiso  9250  sup3exmid  9252  xrltso  10152  frecfzennn  10816  frechashgf1o  10818  0tonninf  10830  1tonninf  10831  nninfinf  10833  facnn  11118  fac0  11119  fac1  11120  cnrecnv  11625  cau3  11830  xrnegiso  11977  sum0  12104  trireciplem  12216  trirecip  12217  ege2le3  12387  oddpwdc  12901  modxai  13144  modsubi  13147  ballotfilemofi  13168  ballotfilem2  13177  ballotfilemefi  13186  ballotfilemafi  13187  ballotfilembfi  13188  ballotfilemrinv  13226  ennnfonelem1  13247  ennnfonelemhf1o  13253  strnfvn  13322  strslss  13349  prdsvallem  13569  mndprop  13707  grpprop  13778  isgrpi  13784  ablprop  14055  prdsval  14120  ringprop  14288  rlmfn  14732  cnfldstr  14837  cncrng  14848  cnfldui  14868  zringbas  14875  zringplusg  14876  dvdsrzring  14882  expghmap  14886  fnpsr  14946  txswaphmeolem  15316  divcnap  15561  expcn  15565  elcncf1ii  15576  cnrehmeocntop  15606  hovercncf  15642  dvid  15691  dvidre  15693  dveflem  15722  dvef  15723  sincn  15765  coscn  15766  cosz12  15776  sincos6thpi  15838  lgsdir2lem5  16036  konigsbergvtx  16608  konigsbergiedg  16609  konigsbergiedgwen  16610  konigsbergumgr  16613  konigsberglem1  16614  konigsberglem2  16615  konigsberglem3  16616  konigsberglem5  16618  konigsberg  16619  bj-sttru  16653  bj-dctru  16666  bj-sbimeh  16685  bdnthALT  16746  012of  16908  2o01f  16909  isomninnlem  16955  iooref1o  16959  iswomninnlem  16975  ismkvnnlem  16978  dceqnconst  16986  dcapnconst  16987  taupi  16999