Theorem mptru 1373

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

Syntax hints:   → wi 4  ⊤wtru 1365

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 1367

This theorem is referenced by:  xorbi12i  1394  dcfromcon  1459  nfbi  1603  spime  1755  eubii  2054  nfmo  2065  mobii  2082  dvelimc  2361  ralbii  2503  rexbii  2504  nfralw  2534  nfralxy  2535  nfrexw  2536  nfralya  2537  nfrexya  2538  nfreuxy  2672  nfsbc1  3007  nfsbc  3010  sbcbii  3049  csbeq2i  3111  nfcsb1  3116  nfsbcw  3119  nfcsbw  3121  nfcsb  3122  nfif  3590  ssbri  4078  nfbr  4080  mpteq12i  4122  ralxfr  4502  rexxfr  4504  nfiotaw  5224  nfriota  5890  nfov  5955  mpoeq123i  5989  mpoeq3ia  5991  disjsnxp  6304  tfri1  6432  eqer  6633  0er  6635  ecopover  6701  ecopoverg  6704  nfixpxy  6785  en2i  6838  en3i  6839  ener  6847  ensymb  6848  entr  6852  djuf1olem  7128  omp1eomlem  7169  infnninf  7199  ltsopi  7404  ltsonq  7482  enq0er  7519  ltpopr  7679  ltposr  7847  axcnex  7943  axaddf  7952  axmulf  7953  ltso  8121  nfneg  8240  negiso  8999  sup3exmid  9001  xrltso  9888  frecfzennn  10535  frechashgf1o  10537  0tonninf  10549  1tonninf  10550  nninfinf  10552  facnn  10836  fac0  10837  fac1  10838  cnrecnv  11092  cau3  11297  xrnegiso  11444  sum0  11570  trireciplem  11682  trirecip  11683  ege2le3  11853  oddpwdc  12367  modxai  12610  modsubi  12613  ennnfonelem1  12649  ennnfonelemhf1o  12655  strnfvn  12724  strslss  12751  prdsvallem  12974  prdsval  12975  mndprop  13143  grpprop  13220  isgrpi  13226  ablprop  13503  ringprop  13672  rlmfn  14085  cnfldstr  14190  cncrng  14201  cnfldui  14221  zringbas  14228  zringplusg  14229  dvdsrzring  14235  expghmap  14239  fnpsr  14297  txswaphmeolem  14640  divcnap  14885  expcn  14889  elcncf1ii  14900  cnrehmeocntop  14930  hovercncf  14966  dvid  15015  dvidre  15017  dveflem  15046  dvef  15047  sincn  15089  coscn  15090  cosz12  15100  sincos6thpi  15162  lgsdir2lem5  15357  bj-sttru  15470  bj-dctru  15483  bj-sbimeh  15502  bdnthALT  15565  012of  15724  2o01f  15725  isomninnlem  15761  iooref1o  15765  iswomninnlem  15780  ismkvnnlem  15783  dceqnconst  15791  dcapnconst  15792  taupi  15804