Theorem mptru 1547

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

Syntax hints:   → wi 4  ⊤wtru 1541

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 1543

This theorem is referenced by:  hadbi123i  1596  cadbi123i  1611  nfan  1899  nfbi  1903  spimefv  2199  spime  2387  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  eqabi  2863  eqabri  2871  nfeq  2905  nfel  2906  dvelimc  2917  nfralwOLD  3286  nfrexw  3287  nfral  3348  nfrex  3349  nfrmo  3403  nfreu  3404  rabbia2  3408  rabeqc  3418  nfrabw  3443  nfrab  3445  reuxfr  3720  reuxfr1  3723  nfsbc1  3772  nfsbcw  3775  nfsbc  3778  sbcbii  3810  csbeq2i  3870  nfcsb1  3885  nfcsbw  3888  nfcsb  3889  eqri  3967  vn0  4308  nfif  4519  nfdisjw  5086  nfdisj  5087  nfbr  5154  nfopab  5176  mpteq1i  5198  mpteq2ia  5202  mpteq12i  5204  ralxfr  5369  issoi  5582  nfiotaw  6468  nfiota  6470  nfriota  7356  nfov  7417  mpoeq123i  7465  mpoeq3ia  7467  opco1i  8104  xpord2indlem  8126  on2recsfn  8631  on2recsov  8632  iseri  8698  nfixpw  8889  nfixp  8890  en2i  8961  en3i  8962  ensymb  8973  entr  8977  1sdom2dom  9194  nfttrcl  9664  djulf1o  9865  djurf1o  9866  r0weon  9965  recmulnq  10917  nrex1  11017  nfneg  11417  negiso  12163  suprzcl2  12897  supxr  13273  xrinf0  13299  fac0  14241  cnrecnv  15131  cau3  15322  cbvsum  15661  cbvsumv  15662  sum0  15687  ackbijnn  15794  flo1  15820  trireciplem  15828  trirecip  15829  ege2le3  16056  rpnnen2lem3  16184  ruclem4  16202  bitsf1ocnv  16414  prmreclem6  16892  prmrec  16893  modxai  17039  strfvn  17156  strss  17176  xpsvsca  17540  mreacs  17619  2oppccomf  17686  setc2obas  18056  setc2ohom  18057  cat1  18059  mndprop  18687  grpprop  18884  isgrpi  18891  oppgmndb  19287  oppggrpb  19290  odfval  19462  efgrelexlemb  19680  ablprop  19723  ringprop  20199  opprrngb  20255  opprringb  20257  rlmbas  21100  rlmplusg  21101  rlm0  21102  rlmsub  21103  rlmmulr  21104  rlmsca2  21106  rlmvsca  21107  rlmtopn  21108  rlmds  21109  rlmvneg  21113  dfcnfldOLD  21280  cncrng  21300  cncrngOLD  21301  xrsmcmn  21303  cndrng  21310  cndrngOLD  21311  cnsrng  21317  xrs1mnd  21321  xrs10  21322  absabv  21341  zringcyg  21379  pzriprngALT  21405  resrng  21530  psrbagsn  21970  evlsval  21993  psr1bas2  22074  psr1bas  22075  psr1plusg  22105  psr1vsca  22106  psr1mulr  22107  ply1plusgfvi  22126  ply1mpl0  22141  ply1mpl1  22143  ordtrestixx  23109  llyidm  23375  nllyidm  23376  toplly  23377  hauslly  23379  hausnlly  23380  lly1stc  23383  kgenf  23428  txswaphmeolem  23691  fmucndlem  24178  nrgtrg  24578  cnfldnm  24666  xrsxmet  24698  divcnOLD  24757  divcn  24759  expcn  24763  expcnOLD  24765  elcncf1ii  24789  iirevcn  24824  iihalf1cn  24826  iihalf1cnOLD  24827  iihalf2cn  24829  iihalf2cnOLD  24830  iimulcn  24834  iimulcnOLD  24835  icopnfcnv  24840  iccpnfcnv  24842  cnrehmeo  24851  cnrehmeoOLD  24852  tcphsub  25121  tcphphl  25127  iscmet3i  25212  cncmet  25222  rrxprds  25289  vitali  25514  i1f0  25588  itg20  25638  cbvitgv  25678  dvid  25819  dveflem  25883  dvef  25884  dvsincos  25885  ply1divalg2  26044  coe0  26161  iaa  26233  sincn  26354  coscn  26355  reefgim  26360  pilem3  26363  resinf1o  26445  circgrp  26461  circsubm  26462  logi  26496  divlogrlim  26544  dvrelog  26546  logcn  26556  dvlog  26560  advlog  26563  cxpcn  26654  cxpcnOLD  26655  cxpcn2  26656  resqrtcn  26659  sqrtcn  26660  atansopn  26842  dvatan  26845  leibpilem2  26851  leibpi  26852  leibpisum  26853  log2cnv  26854  log2ublem2  26857  log2ub  26859  divsqrtsumlem  26890  emcllem4  26909  emcllem6  26911  emcllem7  26912  lgamf  26952  lgam1  26974  basellem6  26996  basellem7  26997  basellem8  26998  basellem9  26999  vmaf  27029  logfacrlim  27135  lgsdir2lem5  27240  chebbnd1  27383  chtppilim  27386  chto1ub  27387  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  chpo1ubb  27392  vmadivsum  27393  vmadivsumb  27394  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  logdivsum  27444  vmalogdivsum2  27449  vmalogdivsum  27450  selberglem1  27456  selberglem2  27457  selbergb  27460  selberg2lem  27461  selberg2  27462  selberg2b  27463  selberg3lem2  27469  selberg3  27470  selberg4  27472  pntrmax  27475  pntrsumo1  27476  pntrsumbnd  27477  selbergr  27479  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem4  27491  pnt2  27524  pnt  27525  dmscut  27723  lrrecpo  27848  noxpordpo  27857  noxpordfr  27858  noxpordse  27859  n0sex  28210  n0ssno  28213  0n0s  28222  n0scut  28226  n0sge0  28230  1p1e2s  28302  zseo  28308  twocut  28309  nohalf  28310  halfcut  28333  0reno  28348  istrkg2ld  28387  legval  28511  ttgsub  28806  cchhllem  28814  2wspdisj  29892  2wspiundisj  29893  konigsbergiedgw  30177  ipasslem7  30765  normlem6  31044  opsqrlem4  32072  fpwrelmap  32656  fpwrelmapffs  32657  sgn3da  32759  xrs0  32944  elrgspnlem2  33194  1fldgenq  33272  dfprm3  33524  zringfrac  33525  ccfldsrarelvec  33666  ccfldextdgrr  33667  constrextdg2  33739  iconstr  33756  constrsdrg  33765  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  mdetlap1  33816  circtopn  33827  cnre2csqima  33901  cnvordtrestixx  33903  mndpluscn  33916  xrge0iifcnv  33923  zlm0  33950  zlm1  33951  qqhre  34010  rrhre  34011  esumnul  34038  hasheuni  34075  sxbrsigalem2  34277  oddpwdc  34345  eulerpartlemb  34359  eulerpartgbij  34363  eulerpartlemn  34372  fib0  34390  fib1  34391  ballotlemrinv  34525  signsw0g  34547  circlemethnat  34632  dvelimalcasei  35066  dvelimexcasei  35068  subfacval2  35174  sinccvglem  35659  circum  35661  antnest  35676  antnestALT  35681  faclim  35733  faclim2  35735  cnndvlem1  36525  bj-dvelimv  36841  bj-inrab2  36916  bj-rabtrAUTO  36920  bj-opelidb  37140  bj-iomnnom  37247  sucneqoni  37354  wl-df-3xor  37456  wl-3xorbi123i  37464  wl-df3maxtru1  37480  wl-cbvalnae  37521  wl-equsal  37529  poimirlem30  37644  dvtan  37664  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  efald2  38072  lcmineqlem7  42023  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p6  42061  cxpi11d  42331  tan3rdpi  42340  asin1half  42345  redvmptabs  42348  readvrec2  42349  readvrec  42350  resuppsinopn  42351  readvcot  42352  re1m1e0m0  42385  re0m0e0  42390  reixi  42411  subresre  42419  3cubeslem4  42677  3cubes  42678  areaquad  43205  clsk1indlem4  44033  clsk1indlem1  44034  ismnushort  44290  lhe4.4ex1a  44318  sbtT  44557  eel0TT  44693  eelTTT  44695  eelT1  44697  eelTT  44760  eelT  44762  eelT0  44764  isosctrlem1ALT  44923  disjsnxp  45064  infxr  45363  nfxneg  45457  limsup0  45692  0cnv  45740  limsup10ex  45771  liminf10ex  45772  liminfvalxr  45781  liminf0  45791  dvsinax  45911  itgsin0pilem1  45948  iblempty  45963  stowei  46062  wallispilem5  46067  wallispi  46068  stirlinglem1  46072  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlingr  46088  dirkertrigeqlem1  46096  fourierdlem62  46166  fourierdlem73  46177  fourierdlem76  46180  fourierdlem77  46181  fourierdlem103  46207  fourierdlem104  46208  fourierclim  46222  fourier  46223  fouriersw  46229  etransclem41  46273  etransclem46  46278  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  dmvolsal  46344  bor1sal  46353  iocborel  46354  sge00  46374  sge0sn  46377  ovolval5lem3  46652  ioosshoi  46667  vonioolem2  46679  smfmullem4  46792  upwrdfi  46885  dfafv2  47130  ichim  47455  nelsubc3  49057  fucofulem2  49297  setc2othin  49452  setcsnterm  49476  setc1obas  49478  setc1ohomfval  49479  setc1ocofval  49480  setc1oid  49481  termc2  49504  setc1onsubc  49588  onsetrec  49694  joinlmuladdmuli  49759