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  4175  nfbr  4177  mpteq12i  4219  ralxfr  4612  rexxfr  4614  nfiotaw  5341  nfriota  6048  nfov  6115  mpoeq123i  6151  mpoeq3ia  6153  disjsnxp  6473  tfri1  6636  eqer  6839  0er  6841  ecopover  6907  ecopoverg  6910  nfixpxy  6999  en2i  7056  en3i  7057  ener  7066  ensymb  7067  entr  7071  djuf1olem  7393  omp1eomlem  7434  infnninf  7464  ltsopi  7687  ltsonq  7765  enq0er  7802  ltpopr  7962  ltposr  8130  axcnex  8226  axaddf  8235  axmulf  8236  ltso  8403  nfneg  8523  negiso  9285  sup3exmid  9287  xrltso  10198  frecfzennn  10863  frechashgf1o  10865  0tonninf  10877  1tonninf  10878  nninfinf  10880  facnn  11165  fac0  11166  fac1  11167  cnrecnv  11676  cau3  11881  xrnegiso  12028  sum0  12155  trireciplem  12267  trirecip  12268  ege2le3  12438  oddpwdc  12952  modxai  13195  modsubi  13198  ballotfilemofi  13219  ballotfilem2  13228  ballotfilemefi  13237  ballotfilemafi  13238  ballotfilembfi  13239  ballotfilemrinv  13277  ennnfonelem1  13298  ennnfonelemhf1o  13304  strnfvn  13373  strslss  13400  prdsvallem  13621  mndprop  13754  grpprop  13823  isgrpi  13829  ablprop  14100  prdsval  14173  ringprop  14345  rlmfn  14790  cnfldstr  14895  cncrng  14906  cnfldui  14924  zringbas  14931  zringplusg  14932  dvdsrzring  14938  expghmap  14942  fnpsr  15051  txswaphmeolem  15421  divcnap  15666  expcn  15670  elcncf1ii  15681  cnrehmeocntop  15711  hovercncf  15747  dvid  15796  dvidre  15798  dveflem  15827  dvef  15828  sincn  15870  coscn  15871  cosz12  15881  sincos6thpi  15943  log2ublem2  16084  log2ublog2  16086  lgsdir2lem5  16151  konigsbergvtx  16723  konigsbergiedg  16724  konigsbergiedgwen  16725  konigsbergumgr  16728  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  konigsberg  16734  bj-sttru  16768  bj-dctru  16781  bj-sbimeh  16800  bdnthALT  16861  012of  17023  2o01f  17024  isomninnlem  17079  iooref1o  17083  iswomninnlem  17099  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111  taupi  17123