Theorem mptru 1548

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

Syntax hints:   → wi 4  ⊤wtru 1542

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 1544

This theorem is referenced by:  hadbi123i  1597  cadbi123i  1612  nfan  1902  nfbi  1906  spimefv  2191  spime  2388  nfsb  2522  nfmov  2554  nfmo  2556  nfeuw  2587  nfeu  2588  eqabi  2869  eqabri  2877  nfeq  2916  nfel  2917  dvelimc  2931  nfralwOLD  3309  nfrexw  3310  nfral  3370  nfrex  3371  nfreuwOLD  3422  nfrmowOLD  3423  nfrmo  3430  nfreu  3431  rabbia2  3435  rabeqc  3444  nfrabw  3468  nfrabwOLD  3469  nfrab  3472  reuxfr  3744  reuxfr1  3747  nfsbc1  3795  nfsbcw  3798  nfsbc  3801  sbcbii  3836  csbeq2i  3900  nfcsb1  3916  nfcsbw  3919  nfcsb  3920  eqri  4001  vn0  4337  nfif  4557  nfdisjw  5124  nfdisj  5125  nfbr  5194  nfopab  5216  mpteq1i  5243  mpteq2ia  5250  mpteq12i  5253  ralxfr  5411  issoi  5621  nfiotaw  6496  nfiota  6498  nfriota  7374  nfov  7435  mpoeq123i  7481  mpoeq3ia  7483  opco1i  8107  xpord2indlem  8129  dfwrecsOLD  8294  on2recsfn  8662  on2recsov  8663  iseri  8726  nfixpw  8906  nfixp  8907  en2i  8982  en3i  8983  ensymb  8994  entr  8998  1sdom2dom  9243  nfttrcl  9702  djulf1o  9903  djurf1o  9904  r0weon  10003  recmulnq  10955  nrex1  11055  nfneg  11452  negiso  12190  suprzcl2  12918  supxr  13288  xrinf0  13313  fac0  14232  cnrecnv  15108  cau3  15298  cbvsum  15637  sum0  15663  ackbijnn  15770  flo1  15796  trireciplem  15804  trirecip  15805  ege2le3  16029  rpnnen2lem3  16155  ruclem4  16173  bitsf1ocnv  16381  prmreclem6  16850  prmrec  16851  modxai  16997  strfvn  17115  strss  17136  xpsvsca  17519  mreacs  17598  2oppccomf  17667  setc2obas  18040  setc2ohom  18041  cat1  18043  mndprop  18647  grpprop  18834  isgrpi  18841  oppgmndb  19216  oppggrpb  19219  odfval  19394  efgrelexlemb  19612  ablprop  19655  ringprop  20097  opprringb  20154  rlmbas  20809  rlmplusg  20810  rlm0  20811  rlmsub  20812  rlmmulr  20813  rlmsca2  20815  rlmvsca  20816  rlmtopn  20817  rlmds  20818  rlmvneg  20822  cncrng  20958  xrsmcmn  20960  cndrng  20966  cnsrng  20971  xrs1mnd  20975  xrs10  20976  absabv  20994  zringcyg  21030  resrng  21165  psrbagsn  21615  evlsval  21640  psr1bas2  21705  psr1bas  21706  psr1plusg  21735  psr1vsca  21736  psr1mulr  21737  ply1plusgfvi  21755  ply1mpl0  21768  ply1mpl1  21770  ordtrestixx  22717  llyidm  22983  nllyidm  22984  toplly  22985  hauslly  22987  hausnlly  22988  lly1stc  22991  kgenf  23036  txswaphmeolem  23299  fmucndlem  23787  nrgtrg  24198  cnfldnm  24286  xrsxmet  24316  divcn  24375  expcn  24379  elcncf1ii  24403  iirevcn  24437  iihalf1cn  24439  iihalf2cn  24441  iimulcn  24445  icopnfcnv  24449  iccpnfcnv  24451  cnrehmeo  24460  tcphsub  24729  tcphphl  24735  iscmet3i  24820  cncmet  24830  rrxprds  24897  vitali  25121  i1f0  25195  itg20  25246  dvid  25426  dveflem  25487  dvef  25488  dvsincos  25489  ply1divalg2  25647  coe0  25761  iaa  25829  sincn  25947  coscn  25948  reefgim  25953  pilem3  25956  resinf1o  26036  circgrp  26052  circsubm  26053  divlogrlim  26134  dvrelog  26136  logcn  26146  dvlog  26150  advlog  26153  cxpcn  26242  cxpcn2  26243  resqrtcn  26246  sqrtcn  26247  atansopn  26426  dvatan  26429  leibpilem2  26435  leibpi  26436  leibpisum  26437  log2cnv  26438  log2ublem2  26441  log2ub  26443  divsqrtsumlem  26473  emcllem4  26492  emcllem6  26494  emcllem7  26495  lgamf  26535  lgam1  26557  basellem6  26579  basellem7  26580  basellem8  26581  basellem9  26582  vmaf  26612  logfacrlim  26716  lgsdir2lem5  26821  chebbnd1  26964  chtppilim  26967  chto1ub  26968  chebbnd2  26969  chto1lb  26970  chpchtlim  26971  chpo1ub  26972  chpo1ubb  26973  vmadivsum  26974  vmadivsumb  26975  mudivsum  27022  mulogsumlem  27023  mulogsum  27024  logdivsum  27025  vmalogdivsum2  27030  vmalogdivsum  27031  selberglem1  27037  selberglem2  27038  selbergb  27041  selberg2lem  27042  selberg2  27043  selberg2b  27044  selberg3lem2  27050  selberg3  27051  selberg4  27053  pntrmax  27056  pntrsumo1  27057  pntrsumbnd  27058  selbergr  27060  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntrlog2bndlem1  27069  pntrlog2bndlem4  27072  pnt2  27105  pnt  27106  dmscut  27301  lrrecpo  27414  noxpordpo  27423  noxpordfr  27424  noxpordse  27425  istrkg2ld  27700  legval  27824  ttgsub  28123  cchhllem  28133  cchhllemOLD  28134  2wspdisj  29205  2wspiundisj  29206  konigsbergiedgw  29490  ipasslem7  30076  normlem6  30355  opsqrlem4  31383  fpwrelmap  31945  fpwrelmapffs  31946  xrs0  32163  1fldgenq  32400  ccfldsrarelvec  32733  ccfldextdgrr  32734  mdetlap1  32794  circtopn  32805  cnre2csqima  32879  cnvordtrestixx  32881  mndpluscn  32894  xrge0iifcnv  32901  zlm0  32928  zlm1  32929  qqhre  32988  rrhre  32989  esumnul  33034  hasheuni  33071  sxbrsigalem2  33273  oddpwdc  33341  eulerpartlemb  33355  eulerpartgbij  33359  eulerpartlemn  33368  fib0  33386  fib1  33387  ballotlemrinv  33520  sgn3da  33528  signsw0g  33555  circlemethnat  33641  subfacval2  34166  sinccvglem  34645  circum  34647  logi  34692  faclim  34704  faclim2  34706  mpomulcn  35150  gg-divcn  35151  gg-expcn  35152  gg-iihalf1cn  35155  gg-iihalf2cn  35156  gg-iimulcn  35157  gg-cnrehmeo  35159  gg-cxpcn  35172  cnndvlem1  35401  bj-dvelimv  35720  bj-inrab2  35796  bj-rabtrAUTO  35800  bj-opelidb  36021  bj-iomnnom  36128  sucneqoni  36235  wl-df-3xor  36337  wl-3xorbi123i  36345  wl-df3maxtru1  36361  wl-cbvalnae  36390  wl-equsal  36397  poimirlem30  36506  dvtan  36526  dvasin  36560  dvacos  36561  dvreasin  36562  dvreacos  36563  efald2  36934  lcmineqlem7  40888  3lexlogpow5ineq1  40907  3lexlogpow5ineq5  40913  aks4d1p1p6  40926  re1m1e0m0  41266  re0m0e0  41271  reixi  41291  subresre  41299  3cubeslem4  41412  3cubes  41413  areaquad  41950  clsk1indlem4  42780  clsk1indlem1  42781  ismnushort  43045  lhe4.4ex1a  43073  sbtT  43313  eel0TT  43450  eelTTT  43452  eelT1  43454  eelTT  43517  eelT  43519  eelT0  43521  isosctrlem1ALT  43680  disjsnxp  43742  infxr  44063  nfxneg  44157  limsup0  44396  0cnv  44444  limsup10ex  44475  liminf10ex  44476  liminfvalxr  44485  liminf0  44495  dvsinax  44615  itgsin0pilem1  44652  iblempty  44667  stowei  44766  wallispilem5  44771  wallispi  44772  stirlinglem1  44776  stirlinglem12  44787  stirlinglem13  44788  stirlinglem14  44789  stirlingr  44792  dirkertrigeqlem1  44800  fourierdlem62  44870  fourierdlem73  44881  fourierdlem76  44884  fourierdlem77  44885  fourierdlem103  44911  fourierdlem104  44912  fourierclim  44926  fourier  44927  fouriersw  44933  etransclem41  44977  etransclem46  44982  salexct2  45041  salexct3  45044  salgencntex  45045  salgensscntex  45046  dmvolsal  45048  bor1sal  45057  iocborel  45058  sge00  45078  sge0sn  45081  ovolval5lem3  45356  ioosshoi  45371  vonioolem2  45383  smfmullem4  45496  upwrdfi  45587  dfafv2  45826  ichim  46111  opprrngb  46661  setc2othin  47629  onsetrec  47706  joinlmuladdmuli  47773