Theorem mptru 1411

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

This proof depends on syntax axioms:   → wi 4  ⊤wtru 1403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-tru 1405

This theorem is used by:  xorbi12i  1432  dcfromcon  1498  nfbi  1642  spime  1794  eubii  2095  nfmo  2106  mobii  2123  eqabi  2371  dvelimc  2414  ralbii  2556  rexbii  2557  nfralw  2587  nfralxy  2588  nfrexw  2589  nfralya  2590  nfrexya  2591  nfreuw  2726  rabbia2  2806  nfsbc1  3069  nfsbc  3072  sbcbii  3111  csbeq2i  3174  nfcsb1  3179  nfsbcw  3182  nfcsbw  3184  nfcsb  3185  nfif  3669  ssbri  4176  nfbr  4178  mpteq1i  4218  mpteq12i  4221  ralxfr  4614  rexxfr  4616  nfiotaw  5344  nfriota  6051  nfov  6118  mpoeq123i  6154  mpoeq3ia  6156  disjsnxp  6477  tfri1  6641  eqer  6844  0er  6846  ecopover  6912  ecopoverg  6915  nfixpxy  7005  en2i  7062  en3i  7063  ener  7072  ensymb  7073  entr  7077  djuf1olem  7399  omp1eomlem  7440  infnninf  7470  ltsopi  7693  ltsonq  7771  enq0er  7808  ltpopr  7968  ltposr  8136  axcnex  8232  axaddf  8241  axmulf  8242  ltso  8409  nfneg  8530  negiso  9293  sup3exmid  9295  xrltso  10214  frecfzennn  10883  frechashgf1o  10885  0tonninf  10897  1tonninf  10898  nninfinf  10900  facnn  11186  fac0  11187  fac1  11188  cnrecnv  11697  cau3  11903  xrnegiso  12052  sum0  12179  trireciplem  12291  trirecip  12292  ege2le3  12462  modxai  13223  modsubi  13227  ballotfilemofi  13276  ballotfilem2  13285  ballotfilemefi  13294  ballotfilemafi  13295  ballotfilembfi  13296  ballotfilemrinv  13334  ennnfonelem1  13355  ennnfonelemhf1o  13361  strnfvn  13430  strslss  13457  prdsvallem  13679  mndprop  13812  grpprop  13881  isgrpi  13887  ablprop  14189  prdsval  14279  ringprop  14451  rlmfn  14898  cnfldstr  15003  cncrng  15014  cnfldui  15032  zringbas  15039  zringplusg  15040  dvdsrzring  15046  expghmap  15050  fnpsr  15161  txswaphmeolem  15563  divcnap  15808  expcn  15812  elcncf1ii  15823  cnrehmeocntop  15853  hovercncf  15889  dvid  15938  dvidre  15940  dveflem  15969  dvef  15970  sincn  16012  coscn  16013  cosz12  16024  sincos6thpi  16086  log2ublem2  16239  log2ublog2  16241  lgsdir2lem5  16373  konigsbergvtx  16945  konigsbergiedg  16946  konigsbergiedgwen  16947  konigsbergumgr  16950  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  konigsberg  16956  bj-sttru  16990  bj-dctru  17003  bj-sbimeh  17022  bdnthALT  17083  012of  17245  2o01f  17246  isomninnlem  17302  iooref1o  17306  iswomninnlem  17323  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335  taupi  17347