Theorem mptru 1549

Description: Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. This is modus ponens ax-mp 5 when the minor hypothesis is ⊤ (which holds by tru 1546). (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 1546	. 2 ⊢ ⊤
2		mptru.1	. 2 ⊢ (⊤ → 𝜑)
3	1, 2	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   → wi 4  ⊤wtru 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-tru 1545

This theorem is referenced by:  hadbi123i  1598  cadbi123i  1613  nfan  1903  nfbi  1907  spimefv  2192  spime  2389  nfsb  2523  nfmov  2555  nfmo  2557  nfeuw  2588  nfeu  2589  eqabi  2870  eqabri  2878  nfeq  2917  nfel  2918  dvelimc  2932  nfralwOLD  3310  nfrexw  3311  nfral  3371  nfrex  3372  nfreuwOLD  3423  nfrmowOLD  3424  nfrmo  3431  nfreu  3432  rabbia2  3436  rabeqc  3445  nfrabw  3469  nfrabwOLD  3470  nfrab  3473  reuxfr  3746  reuxfr1  3749  nfsbc1  3797  nfsbcw  3800  nfsbc  3803  sbcbii  3838  csbeq2i  3902  nfcsb1  3918  nfcsbw  3921  nfcsb  3922  eqri  4003  vn0  4339  nfif  4559  nfdisjw  5126  nfdisj  5127  nfbr  5196  nfopab  5218  mpteq1i  5245  mpteq2ia  5252  mpteq12i  5255  ralxfr  5413  issoi  5623  nfiotaw  6500  nfiota  6502  nfriota  7378  nfov  7439  mpoeq123i  7485  mpoeq3ia  7487  opco1i  8111  xpord2indlem  8133  dfwrecsOLD  8298  on2recsfn  8666  on2recsov  8667  iseri  8730  nfixpw  8910  nfixp  8911  en2i  8986  en3i  8987  ensymb  8998  entr  9002  1sdom2dom  9247  nfttrcl  9706  djulf1o  9907  djurf1o  9908  r0weon  10007  recmulnq  10959  nrex1  11059  nfneg  11456  negiso  12194  suprzcl2  12922  supxr  13292  xrinf0  13317  fac0  14236  cnrecnv  15112  cau3  15302  cbvsum  15641  sum0  15667  ackbijnn  15774  flo1  15800  trireciplem  15808  trirecip  15809  ege2le3  16033  rpnnen2lem3  16159  ruclem4  16177  bitsf1ocnv  16385  prmreclem6  16854  prmrec  16855  modxai  17001  strfvn  17119  strss  17140  xpsvsca  17523  mreacs  17602  2oppccomf  17671  setc2obas  18044  setc2ohom  18045  cat1  18047  mndprop  18651  grpprop  18838  isgrpi  18845  oppgmndb  19222  oppggrpb  19225  odfval  19400  efgrelexlemb  19618  ablprop  19661  ringprop  20104  opprringb  20162  rlmbas  20817  rlmplusg  20818  rlm0  20819  rlmsub  20820  rlmmulr  20821  rlmsca2  20823  rlmvsca  20824  rlmtopn  20825  rlmds  20826  rlmvneg  20830  cncrng  20966  xrsmcmn  20968  cndrng  20974  cnsrng  20979  xrs1mnd  20983  xrs10  20984  absabv  21002  zringcyg  21039  resrng  21174  psrbagsn  21624  evlsval  21649  psr1bas2  21714  psr1bas  21715  psr1plusg  21744  psr1vsca  21745  psr1mulr  21746  ply1plusgfvi  21764  ply1mpl0  21777  ply1mpl1  21779  ordtrestixx  22726  llyidm  22992  nllyidm  22993  toplly  22994  hauslly  22996  hausnlly  22997  lly1stc  23000  kgenf  23045  txswaphmeolem  23308  fmucndlem  23796  nrgtrg  24207  cnfldnm  24295  xrsxmet  24325  divcn  24384  expcn  24388  elcncf1ii  24412  iirevcn  24446  iihalf1cn  24448  iihalf2cn  24450  iimulcn  24454  icopnfcnv  24458  iccpnfcnv  24460  cnrehmeo  24469  tcphsub  24738  tcphphl  24744  iscmet3i  24829  cncmet  24839  rrxprds  24906  vitali  25130  i1f0  25204  itg20  25255  dvid  25435  dveflem  25496  dvef  25497  dvsincos  25498  ply1divalg2  25656  coe0  25770  iaa  25838  sincn  25956  coscn  25957  reefgim  25962  pilem3  25965  resinf1o  26045  circgrp  26061  circsubm  26062  divlogrlim  26143  dvrelog  26145  logcn  26155  dvlog  26159  advlog  26162  cxpcn  26253  cxpcn2  26254  resqrtcn  26257  sqrtcn  26258  atansopn  26437  dvatan  26440  leibpilem2  26446  leibpi  26447  leibpisum  26448  log2cnv  26449  log2ublem2  26452  log2ub  26454  divsqrtsumlem  26484  emcllem4  26503  emcllem6  26505  emcllem7  26506  lgamf  26546  lgam1  26568  basellem6  26590  basellem7  26591  basellem8  26592  basellem9  26593  vmaf  26623  logfacrlim  26727  lgsdir2lem5  26832  chebbnd1  26975  chtppilim  26978  chto1ub  26979  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  chpo1ubb  26984  vmadivsum  26985  vmadivsumb  26986  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  logdivsum  27036  vmalogdivsum2  27041  vmalogdivsum  27042  selberglem1  27048  selberglem2  27049  selbergb  27052  selberg2lem  27053  selberg2  27054  selberg2b  27055  selberg3lem2  27061  selberg3  27062  selberg4  27064  pntrmax  27067  pntrsumo1  27068  pntrsumbnd  27069  selbergr  27071  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntrlog2bndlem1  27080  pntrlog2bndlem4  27083  pnt2  27116  pnt  27117  dmscut  27312  lrrecpo  27425  noxpordpo  27434  noxpordfr  27435  noxpordse  27436  istrkg2ld  27711  legval  27835  ttgsub  28134  cchhllem  28144  cchhllemOLD  28145  2wspdisj  29216  2wspiundisj  29217  konigsbergiedgw  29501  ipasslem7  30089  normlem6  30368  opsqrlem4  31396  fpwrelmap  31958  fpwrelmapffs  31959  xrs0  32176  1fldgenq  32412  ccfldsrarelvec  32745  ccfldextdgrr  32746  mdetlap1  32806  circtopn  32817  cnre2csqima  32891  cnvordtrestixx  32893  mndpluscn  32906  xrge0iifcnv  32913  zlm0  32940  zlm1  32941  qqhre  33000  rrhre  33001  esumnul  33046  hasheuni  33083  sxbrsigalem2  33285  oddpwdc  33353  eulerpartlemb  33367  eulerpartgbij  33371  eulerpartlemn  33380  fib0  33398  fib1  33399  ballotlemrinv  33532  sgn3da  33540  signsw0g  33567  circlemethnat  33653  subfacval2  34178  sinccvglem  34657  circum  34659  logi  34704  faclim  34716  faclim2  34718  mpomulcn  35162  gg-divcn  35163  gg-expcn  35164  gg-iihalf1cn  35167  gg-iihalf2cn  35168  gg-iimulcn  35169  gg-cnrehmeo  35171  gg-cxpcn  35184  cnndvlem1  35413  bj-dvelimv  35732  bj-inrab2  35808  bj-rabtrAUTO  35812  bj-opelidb  36033  bj-iomnnom  36140  sucneqoni  36247  wl-df-3xor  36349  wl-3xorbi123i  36357  wl-df3maxtru1  36373  wl-cbvalnae  36402  wl-equsal  36409  poimirlem30  36518  dvtan  36538  dvasin  36572  dvacos  36573  dvreasin  36574  dvreacos  36575  efald2  36946  lcmineqlem7  40900  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1p6  40938  re1m1e0m0  41270  re0m0e0  41275  reixi  41295  subresre  41303  3cubeslem4  41427  3cubes  41428  areaquad  41965  clsk1indlem4  42795  clsk1indlem1  42796  ismnushort  43060  lhe4.4ex1a  43088  sbtT  43328  eel0TT  43465  eelTTT  43467  eelT1  43469  eelTT  43532  eelT  43534  eelT0  43536  isosctrlem1ALT  43695  disjsnxp  43757  infxr  44077  nfxneg  44171  limsup0  44410  0cnv  44458  limsup10ex  44489  liminf10ex  44490  liminfvalxr  44499  liminf0  44509  dvsinax  44629  itgsin0pilem1  44666  iblempty  44681  stowei  44780  wallispilem5  44785  wallispi  44786  stirlinglem1  44790  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlingr  44806  dirkertrigeqlem1  44814  fourierdlem62  44884  fourierdlem73  44895  fourierdlem76  44898  fourierdlem77  44899  fourierdlem103  44925  fourierdlem104  44926  fourierclim  44940  fourier  44941  fouriersw  44947  etransclem41  44991  etransclem46  44996  salexct2  45055  salexct3  45058  salgencntex  45059  salgensscntex  45060  dmvolsal  45062  bor1sal  45071  iocborel  45072  sge00  45092  sge0sn  45095  ovolval5lem3  45370  ioosshoi  45385  vonioolem2  45397  smfmullem4  45510  upwrdfi  45601  dfafv2  45840  ichim  46125  opprrngb  46675  pzriprngALT  46819  setc2othin  47676  onsetrec  47753  joinlmuladdmuli  47820