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  7406  ltsonq  7484  enq0er  7521  ltpopr  7681  ltposr  7849  axcnex  7945  axaddf  7954  axmulf  7955  ltso  8123  nfneg  8242  negiso  9001  sup3exmid  9003  xrltso  9890  frecfzennn  10537  frechashgf1o  10539  0tonninf  10551  1tonninf  10552  nninfinf  10554  facnn  10838  fac0  10839  fac1  10840  cnrecnv  11094  cau3  11299  xrnegiso  11446  sum0  11572  trireciplem  11684  trirecip  11685  ege2le3  11855  oddpwdc  12369  modxai  12612  modsubi  12615  ennnfonelem1  12651  ennnfonelemhf1o  12657  strnfvn  12726  strslss  12753  prdsvallem  12976  prdsval  12977  mndprop  13145  grpprop  13222  isgrpi  13228  ablprop  13505  ringprop  13674  rlmfn  14087  cnfldstr  14192  cncrng  14203  cnfldui  14223  zringbas  14230  zringplusg  14231  dvdsrzring  14237  expghmap  14241  fnpsr  14301  txswaphmeolem  14664  divcnap  14909  expcn  14913  elcncf1ii  14924  cnrehmeocntop  14954  hovercncf  14990  dvid  15039  dvidre  15041  dveflem  15070  dvef  15071  sincn  15113  coscn  15114  cosz12  15124  sincos6thpi  15186  lgsdir2lem5  15381  bj-sttru  15494  bj-dctru  15507  bj-sbimeh  15526  bdnthALT  15589  012of  15748  2o01f  15749  isomninnlem  15787  iooref1o  15791  iswomninnlem  15806  ismkvnnlem  15809  dceqnconst  15817  dcapnconst  15818  taupi  15830