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 207  df-tru 1545

This theorem is referenced by:  hadbi123i  1598  cadbi123i  1613  nfan  1901  nfbi  1905  spimefv  2206  spime  2394  nfsb  2528  nfmov  2561  nfmo  2563  nfeuw  2594  nfeu  2595  eqabi  2872  eqabri  2879  nfeq  2913  nfel  2914  dvelimc  2925  nfrexw  3286  nfral  3346  nfrex  3347  nfrmo  3399  nfreu  3400  rabbia2  3404  rabeqc  3413  nfrabw  3438  nfrab  3440  reuxfr  3709  reuxfr1  3712  nfsbc1  3761  nfsbcw  3764  nfsbc  3767  sbcbii  3799  csbeq2i  3859  nfcsb1  3874  nfcsbw  3877  nfcsb  3878  eqri  3956  ss2rabi  4030  nfif  4512  nfdisjw  5079  nfdisj  5080  nfbr  5147  nfopab  5169  mpteq1i  5191  mpteq2ia  5195  mpteq12i  5197  ralxfr  5361  issoi  5576  nfiotaw  6460  nfiota  6462  nfriota  7337  nfov  7398  mpoeq123i  7444  mpoeq3ia  7446  opco1i  8077  xpord2indlem  8099  on2recsfn  8605  on2recsov  8606  iseri  8673  nfixpw  8866  nfixp  8867  en2i  8939  en3i  8940  ensymb  8951  entr  8955  1sdom2dom  9166  nfttrcl  9632  djulf1o  9836  djurf1o  9837  r0weon  9934  recmulnq  10887  nrex1  10987  nfneg  11388  negiso  12134  suprzcl2  12863  supxr  13240  xrinf0  13266  fac0  14211  cnrecnv  15100  cau3  15291  cbvsum  15630  cbvsumv  15631  sum0  15656  ackbijnn  15763  flo1  15789  trireciplem  15797  trirecip  15798  ege2le3  16025  rpnnen2lem3  16153  ruclem4  16171  bitsf1ocnv  16383  prmreclem6  16861  prmrec  16862  modxai  17008  strfvn  17125  strss  17145  xpsvsca  17510  mreacs  17593  2oppccomf  17660  setc2obas  18030  setc2ohom  18031  cat1  18033  chnflenfi  18563  chninf  18570  mndprop  18697  grpprop  18894  isgrpi  18901  oppgmndb  19296  oppggrpb  19299  odfval  19473  efgrelexlemb  19691  ablprop  19734  ringprop  20237  opprrngb  20294  opprringb  20296  rlmbas  21157  rlmplusg  21158  rlm0  21159  rlmsub  21160  rlmmulr  21161  rlmsca2  21163  rlmvsca  21164  rlmtopn  21165  rlmds  21166  rlmvneg  21170  dfcnfldOLD  21337  cncrng  21355  cncrngOLD  21356  xrsmcmn  21358  cndrng  21365  cndrngOLD  21366  cnsrng  21372  absabv  21391  xrs1mnd  21407  xrs10  21408  zringcyg  21436  pzriprngALT  21462  resrng  21588  psrbagsn  22030  evlsval  22053  psr1bas2  22142  psr1bas  22143  psr1plusg  22173  psr1vsca  22174  psr1mulr  22175  ply1plusgfvi  22194  ply1mpl0  22209  ply1mpl1  22211  ordtrestixx  23178  llyidm  23444  nllyidm  23445  toplly  23446  hauslly  23448  hausnlly  23449  lly1stc  23452  kgenf  23497  txswaphmeolem  23760  fmucndlem  24246  nrgtrg  24646  cnfldnm  24734  xrsxmet  24766  divcnOLD  24825  divcn  24827  expcn  24831  expcnOLD  24833  elcncf1ii  24857  iirevcn  24892  iihalf1cn  24894  iihalf1cnOLD  24895  iihalf2cn  24897  iihalf2cnOLD  24898  iimulcn  24902  iimulcnOLD  24903  icopnfcnv  24908  iccpnfcnv  24910  cnrehmeo  24919  cnrehmeoOLD  24920  tcphsub  25189  tcphphl  25195  iscmet3i  25280  cncmet  25290  rrxprds  25357  vitali  25582  i1f0  25656  itg20  25706  cbvitgv  25746  dvid  25887  dveflem  25951  dvef  25952  dvsincos  25953  ply1divalg2  26112  coe0  26229  iaa  26301  sincn  26422  coscn  26423  reefgim  26428  pilem3  26431  resinf1o  26513  circgrp  26529  circsubm  26530  logi  26564  divlogrlim  26612  dvrelog  26614  logcn  26624  dvlog  26628  advlog  26631  cxpcn  26722  cxpcnOLD  26723  cxpcn2  26724  resqrtcn  26727  sqrtcn  26728  atansopn  26910  dvatan  26913  leibpilem2  26919  leibpi  26920  leibpisum  26921  log2cnv  26922  log2ublem2  26925  log2ub  26927  divsqrtsumlem  26958  emcllem4  26977  emcllem6  26979  emcllem7  26980  lgamf  27020  lgam1  27042  basellem6  27064  basellem7  27065  basellem8  27066  basellem9  27067  vmaf  27097  logfacrlim  27203  lgsdir2lem5  27308  chebbnd1  27451  chtppilim  27454  chto1ub  27455  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  chpo1ubb  27460  vmadivsum  27461  vmadivsumb  27462  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  logdivsum  27512  vmalogdivsum2  27517  vmalogdivsum  27518  selberglem1  27524  selberglem2  27525  selbergb  27528  selberg2lem  27529  selberg2  27530  selberg2b  27531  selberg3lem2  27537  selberg3  27538  selberg4  27540  pntrmax  27543  pntrsumo1  27544  pntrsumbnd  27545  selbergr  27547  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem4  27559  pnt2  27592  pnt  27593  dmcuts  27799  lrrecpo  27949  noxpordpo  27958  noxpordfr  27959  noxpordse  27960  n0ssno  28328  0n0s  28337  n0cut  28342  n0sge0  28346  zseo  28430  twocut  28431  nohalf  28432  halfcut  28466  bdaypw2n0bndlem  28471  0reno  28504  1reno  28505  istrkg2ld  28544  legval  28668  ttgsub  28963  cchhllem  28971  2wspdisj  30050  2wspiundisj  30051  konigsbergiedgw  30335  ipasslem7  30924  normlem6  31203  opsqrlem4  32231  fpwrelmap  32823  fpwrelmapffs  32824  sgn3da  32926  xrs0  33099  elrgspnlem2  33337  1fldgenq  33416  dfprm3  33646  zringfrac  33647  ccfldsrarelvec  33849  ccfldextdgrr  33850  constrextdg2  33927  iconstr  33944  constrsdrg  33953  2sqr3minply  33958  2sqr3nconstr  33959  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  mdetlap1  34004  circtopn  34015  cnre2csqima  34089  cnvordtrestixx  34091  mndpluscn  34104  xrge0iifcnv  34111  zlm0  34138  zlm1  34139  qqhre  34198  rrhre  34199  esumnul  34226  hasheuni  34263  sxbrsigalem2  34464  oddpwdc  34532  eulerpartlemb  34546  eulerpartgbij  34550  eulerpartlemn  34559  fib0  34577  fib1  34578  ballotlemrinv  34712  signsw0g  34734  circlemethnat  34819  dvelimalcasei  35252  dvelimexcasei  35254  subfacval2  35403  sinccvglem  35888  circum  35890  antnest  35905  antnestALT  35910  faclim  35962  faclim2  35964  cnndvlem1  36759  bj-alextruim  36880  bj-dvelimv  37101  bj-inrab2  37176  bj-rabtrAUTO  37180  bj-opelidb  37407  bj-iomnnom  37514  sucneqoni  37621  wl-df-3xor  37723  wl-3xorbi123i  37731  wl-df3maxtru1  37747  wl-cbvalnae  37788  wl-equsal  37796  poimirlem30  37901  dvtan  37921  dvasin  37955  dvacos  37956  dvreasin  37957  dvreacos  37958  efald2  38329  lcmineqlem7  42405  3lexlogpow5ineq1  42424  3lexlogpow5ineq5  42430  aks4d1p1p6  42443  cxpi11d  42713  tan3rdpi  42722  asin1half  42727  redvmptabs  42730  readvrec2  42731  readvrec  42732  resuppsinopn  42733  readvcot  42734  re1m1e0m0  42767  re0m0e0  42772  reixi  42793  subresre  42801  3cubeslem4  43046  3cubes  43047  areaquad  43573  clsk1indlem4  44400  clsk1indlem1  44401  ismnushort  44657  lhe4.4ex1a  44685  sbtT  44923  eel0TT  45059  eelTTT  45061  eelT1  45063  eelTT  45126  eelT  45128  eelT0  45130  isosctrlem1ALT  45289  disjsnxp  45430  infxr  45725  nfxneg  45819  limsup0  46052  0cnv  46100  limsup10ex  46131  liminf10ex  46132  liminfvalxr  46141  liminf0  46151  dvsinax  46271  itgsin0pilem1  46308  iblempty  46323  stowei  46422  wallispilem5  46427  wallispi  46428  stirlinglem1  46432  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlingr  46448  dirkertrigeqlem1  46456  fourierdlem62  46526  fourierdlem73  46537  fourierdlem76  46540  fourierdlem77  46541  fourierdlem103  46567  fourierdlem104  46568  fourierclim  46582  fourier  46583  fouriersw  46589  etransclem41  46633  etransclem46  46638  salexct2  46697  salexct3  46700  salgencntex  46701  salgensscntex  46702  dmvolsal  46704  bor1sal  46713  iocborel  46714  sge00  46734  sge0sn  46737  ovolval5lem3  47012  ioosshoi  47027  vonioolem2  47039  smfmullem4  47152  nthrucw  47244  cjnpoly  47249  dfafv2  47492  ichim  47817  grlimedgnedg  48491  nelsubc3  49430  fucofulem2  49670  setc2othin  49825  setcsnterm  49849  setc1obas  49851  setc1ohomfval  49852  setc1ocofval  49853  setc1oid  49854  termc2  49877  setc1onsubc  49961  onsetrec  50067  joinlmuladdmuli  50132