Theorem mptru 1382

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

Syntax hints:   → wi 4  ⊤wtru 1374

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 1376

This theorem is referenced by:  xorbi12i  1403  dcfromcon  1469  nfbi  1613  spime  1765  eubii  2064  nfmo  2075  mobii  2092  dvelimc  2371  ralbii  2513  rexbii  2514  nfralw  2544  nfralxy  2545  nfrexw  2546  nfralya  2547  nfrexya  2548  nfreuxy  2682  nfsbc1  3020  nfsbc  3023  sbcbii  3062  csbeq2i  3124  nfcsb1  3129  nfsbcw  3132  nfcsbw  3134  nfcsb  3135  nfif  3604  ssbri  4096  nfbr  4098  mpteq12i  4140  ralxfr  4521  rexxfr  4523  nfiotaw  5245  nfriota  5922  nfov  5987  mpoeq123i  6021  mpoeq3ia  6023  disjsnxp  6336  tfri1  6464  eqer  6665  0er  6667  ecopover  6733  ecopoverg  6736  nfixpxy  6817  en2i  6874  en3i  6875  ener  6884  ensymb  6885  entr  6889  djuf1olem  7170  omp1eomlem  7211  infnninf  7241  ltsopi  7453  ltsonq  7531  enq0er  7568  ltpopr  7728  ltposr  7896  axcnex  7992  axaddf  8001  axmulf  8002  ltso  8170  nfneg  8289  negiso  9048  sup3exmid  9050  xrltso  9938  frecfzennn  10593  frechashgf1o  10595  0tonninf  10607  1tonninf  10608  nninfinf  10610  facnn  10894  fac0  10895  fac1  10896  cnrecnv  11296  cau3  11501  xrnegiso  11648  sum0  11774  trireciplem  11886  trirecip  11887  ege2le3  12057  oddpwdc  12571  modxai  12814  modsubi  12817  ennnfonelem1  12853  ennnfonelemhf1o  12859  strnfvn  12928  strslss  12955  prdsvallem  13179  prdsval  13180  mndprop  13348  grpprop  13425  isgrpi  13431  ablprop  13708  ringprop  13877  rlmfn  14290  cnfldstr  14395  cncrng  14406  cnfldui  14426  zringbas  14433  zringplusg  14434  dvdsrzring  14440  expghmap  14444  fnpsr  14504  txswaphmeolem  14867  divcnap  15112  expcn  15116  elcncf1ii  15127  cnrehmeocntop  15157  hovercncf  15193  dvid  15242  dvidre  15244  dveflem  15273  dvef  15274  sincn  15316  coscn  15317  cosz12  15327  sincos6thpi  15389  lgsdir2lem5  15584  bj-sttru  15815  bj-dctru  15828  bj-sbimeh  15847  bdnthALT  15909  012of  16069  2o01f  16070  isomninnlem  16110  iooref1o  16114  iswomninnlem  16129  ismkvnnlem  16132  dceqnconst  16140  dcapnconst  16141  taupi  16153