Theorem mptru 1404

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

Syntax hints:   → wi 4  ⊤wtru 1396

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 1398

This theorem is referenced by:  xorbi12i  1425  dcfromcon  1491  nfbi  1635  spime  1787  eubii  2086  nfmo  2097  mobii  2114  dvelimc  2394  ralbii  2536  rexbii  2537  nfralw  2567  nfralxy  2568  nfrexw  2569  nfralya  2570  nfrexya  2571  nfreuw  2706  nfsbc1  3046  nfsbc  3049  sbcbii  3088  csbeq2i  3151  nfcsb1  3156  nfsbcw  3159  nfcsbw  3161  nfcsb  3162  nfif  3631  ssbri  4127  nfbr  4129  mpteq12i  4171  ralxfr  4556  rexxfr  4558  nfiotaw  5281  nfriota  5963  nfov  6030  mpoeq123i  6066  mpoeq3ia  6068  disjsnxp  6381  tfri1  6509  eqer  6710  0er  6712  ecopover  6778  ecopoverg  6781  nfixpxy  6862  en2i  6919  en3i  6920  ener  6929  ensymb  6930  entr  6934  djuf1olem  7216  omp1eomlem  7257  infnninf  7287  ltsopi  7503  ltsonq  7581  enq0er  7618  ltpopr  7778  ltposr  7946  axcnex  8042  axaddf  8051  axmulf  8052  ltso  8220  nfneg  8339  negiso  9098  sup3exmid  9100  xrltso  9988  frecfzennn  10643  frechashgf1o  10645  0tonninf  10657  1tonninf  10658  nninfinf  10660  facnn  10944  fac0  10945  fac1  10946  cnrecnv  11416  cau3  11621  xrnegiso  11768  sum0  11894  trireciplem  12006  trirecip  12007  ege2le3  12177  oddpwdc  12691  modxai  12934  modsubi  12937  ennnfonelem1  12973  ennnfonelemhf1o  12979  strnfvn  13048  strslss  13075  prdsvallem  13300  prdsval  13301  mndprop  13469  grpprop  13546  isgrpi  13552  ablprop  13829  ringprop  13998  rlmfn  14411  cnfldstr  14516  cncrng  14527  cnfldui  14547  zringbas  14554  zringplusg  14555  dvdsrzring  14561  expghmap  14565  fnpsr  14625  txswaphmeolem  14988  divcnap  15233  expcn  15237  elcncf1ii  15248  cnrehmeocntop  15278  hovercncf  15314  dvid  15363  dvidre  15365  dveflem  15394  dvef  15395  sincn  15437  coscn  15438  cosz12  15448  sincos6thpi  15510  lgsdir2lem5  15705  bj-sttru  16062  bj-dctru  16075  bj-sbimeh  16094  bdnthALT  16156  012of  16316  2o01f  16317  isomninnlem  16357  iooref1o  16361  iswomninnlem  16376  ismkvnnlem  16379  dceqnconst  16387  dcapnconst  16388  taupi  16400