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  5363  issoi  5578  nfiotaw  6462  nfiota  6464  nfriota  7339  nfov  7400  mpoeq123i  7446  mpoeq3ia  7448  opco1i  8079  xpord2indlem  8101  on2recsfn  8607  on2recsov  8608  iseri  8675  nfixpw  8868  nfixp  8869  en2i  8941  en3i  8942  ensymb  8953  entr  8957  1sdom2dom  9168  nfttrcl  9634  djulf1o  9838  djurf1o  9839  r0weon  9936  recmulnq  10889  nrex1  10989  nfneg  11390  negiso  12136  suprzcl2  12865  supxr  13242  xrinf0  13268  fac0  14213  cnrecnv  15102  cau3  15293  cbvsum  15632  cbvsumv  15633  sum0  15658  ackbijnn  15765  flo1  15791  trireciplem  15799  trirecip  15800  ege2le3  16027  rpnnen2lem3  16155  ruclem4  16173  bitsf1ocnv  16385  prmreclem6  16863  prmrec  16864  modxai  17010  strfvn  17127  strss  17147  xpsvsca  17512  mreacs  17595  2oppccomf  17662  setc2obas  18032  setc2ohom  18033  cat1  18035  chnflenfi  18565  chninf  18572  mndprop  18699  grpprop  18899  isgrpi  18906  oppgmndb  19301  oppggrpb  19304  odfval  19478  efgrelexlemb  19696  ablprop  19739  ringprop  20242  opprrngb  20299  opprringb  20301  rlmbas  21162  rlmplusg  21163  rlm0  21164  rlmsub  21165  rlmmulr  21166  rlmsca2  21168  rlmvsca  21169  rlmtopn  21170  rlmds  21171  rlmvneg  21175  dfcnfldOLD  21342  cncrng  21360  cncrngOLD  21361  xrsmcmn  21363  cndrng  21370  cndrngOLD  21371  cnsrng  21377  absabv  21396  xrs1mnd  21412  xrs10  21413  zringcyg  21441  pzriprngALT  21467  resrng  21593  psrbagsn  22035  evlsval  22058  psr1bas2  22147  psr1bas  22148  psr1plusg  22178  psr1vsca  22179  psr1mulr  22180  ply1plusgfvi  22199  ply1mpl0  22214  ply1mpl1  22216  ordtrestixx  23183  llyidm  23449  nllyidm  23450  toplly  23451  hauslly  23453  hausnlly  23454  lly1stc  23457  kgenf  23502  txswaphmeolem  23765  fmucndlem  24251  nrgtrg  24651  cnfldnm  24739  xrsxmet  24771  divcnOLD  24830  divcn  24832  expcn  24836  expcnOLD  24838  elcncf1ii  24862  iirevcn  24897  iihalf1cn  24899  iihalf1cnOLD  24900  iihalf2cn  24902  iihalf2cnOLD  24903  iimulcn  24907  iimulcnOLD  24908  icopnfcnv  24913  iccpnfcnv  24915  cnrehmeo  24924  cnrehmeoOLD  24925  tcphsub  25194  tcphphl  25200  iscmet3i  25285  cncmet  25295  rrxprds  25362  vitali  25587  i1f0  25661  itg20  25711  cbvitgv  25751  dvid  25892  dveflem  25956  dvef  25957  dvsincos  25958  ply1divalg2  26117  coe0  26234  iaa  26306  sincn  26427  coscn  26428  reefgim  26433  pilem3  26436  resinf1o  26518  circgrp  26534  circsubm  26535  logi  26569  divlogrlim  26617  dvrelog  26619  logcn  26629  dvlog  26633  advlog  26636  cxpcn  26727  cxpcnOLD  26728  cxpcn2  26729  resqrtcn  26732  sqrtcn  26733  atansopn  26915  dvatan  26918  leibpilem2  26924  leibpi  26925  leibpisum  26926  log2cnv  26927  log2ublem2  26930  log2ub  26932  divsqrtsumlem  26963  emcllem4  26982  emcllem6  26984  emcllem7  26985  lgamf  27025  lgam1  27047  basellem6  27069  basellem7  27070  basellem8  27071  basellem9  27072  vmaf  27102  logfacrlim  27208  lgsdir2lem5  27313  chebbnd1  27456  chtppilim  27459  chto1ub  27460  chebbnd2  27461  chto1lb  27462  chpchtlim  27463  chpo1ub  27464  chpo1ubb  27465  vmadivsum  27466  vmadivsumb  27467  mudivsum  27514  mulogsumlem  27515  mulogsum  27516  logdivsum  27517  vmalogdivsum2  27522  vmalogdivsum  27523  selberglem1  27529  selberglem2  27530  selbergb  27533  selberg2lem  27534  selberg2  27535  selberg2b  27536  selberg3lem2  27542  selberg3  27543  selberg4  27545  pntrmax  27548  pntrsumo1  27549  pntrsumbnd  27550  selbergr  27552  selberg3r  27553  selberg4r  27554  selberg34r  27555  pntrlog2bndlem1  27561  pntrlog2bndlem4  27564  pnt2  27597  pnt  27598  dmcuts  27804  lrrecpo  27954  noxpordpo  27963  noxpordfr  27964  noxpordse  27965  n0ssno  28333  0n0s  28342  n0cut  28347  n0sge0  28351  zseo  28435  twocut  28436  nohalf  28437  halfcut  28471  bdaypw2n0bndlem  28476  0reno  28509  1reno  28510  istrkg2ld  28549  istrkg2ldOLD  28550  legval  28674  ttgsub  28969  cchhllem  28977  2wspdisj  30056  2wspiundisj  30057  konigsbergiedgw  30341  ipasslem7  30930  normlem6  31209  opsqrlem4  32237  fpwrelmap  32829  fpwrelmapffs  32830  sgn3da  32932  xrs0  33105  elrgspnlem2  33343  1fldgenq  33422  dfprm3  33652  zringfrac  33653  ccfldsrarelvec  33855  ccfldextdgrr  33856  constrextdg2  33933  iconstr  33950  constrsdrg  33959  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  mdetlap1  34010  circtopn  34021  cnre2csqima  34095  cnvordtrestixx  34097  mndpluscn  34110  xrge0iifcnv  34117  zlm0  34144  zlm1  34145  qqhre  34204  rrhre  34205  esumnul  34232  hasheuni  34269  sxbrsigalem2  34470  oddpwdc  34538  eulerpartlemb  34552  eulerpartgbij  34556  eulerpartlemn  34565  fib0  34583  fib1  34584  ballotlemrinv  34718  signsw0g  34740  circlemethnat  34825  dvelimalcasei  35258  dvelimexcasei  35260  subfacval2  35409  sinccvglem  35894  circum  35896  antnest  35911  antnestALT  35916  faclim  35968  faclim2  35970  cnndvlem1  36765  bj-alextruim  36899  bj-dvelimv  37128  bj-inrab2  37203  bj-rabtrAUTO  37207  bj-opelidb  37434  bj-iomnnom  37541  sucneqoni  37648  wl-df-3xor  37750  wl-3xorbi123i  37758  wl-df3maxtru1  37774  wl-cbvalnae  37817  wl-equsal  37825  poimirlem30  37930  dvtan  37950  dvasin  37984  dvacos  37985  dvreasin  37986  dvreacos  37987  efald2  38358  lcmineqlem7  42434  3lexlogpow5ineq1  42453  3lexlogpow5ineq5  42459  aks4d1p1p6  42472  cxpi11d  42742  tan3rdpi  42751  asin1half  42756  redvmptabs  42759  readvrec2  42760  readvrec  42761  resuppsinopn  42762  readvcot  42763  re1m1e0m0  42796  re0m0e0  42801  reixi  42822  subresre  42830  3cubeslem4  43075  3cubes  43076  areaquad  43602  clsk1indlem4  44429  clsk1indlem1  44430  ismnushort  44686  lhe4.4ex1a  44714  sbtT  44952  eel0TT  45088  eelTTT  45090  eelT1  45092  eelTT  45155  eelT  45157  eelT0  45159  isosctrlem1ALT  45318  disjsnxp  45459  infxr  45754  nfxneg  45848  limsup0  46081  0cnv  46129  limsup10ex  46160  liminf10ex  46161  liminfvalxr  46170  liminf0  46180  dvsinax  46300  itgsin0pilem1  46337  iblempty  46352  stowei  46451  wallispilem5  46456  wallispi  46457  stirlinglem1  46461  stirlinglem12  46472  stirlinglem13  46473  stirlinglem14  46474  stirlingr  46477  dirkertrigeqlem1  46485  fourierdlem62  46555  fourierdlem73  46566  fourierdlem76  46569  fourierdlem77  46570  fourierdlem103  46596  fourierdlem104  46597  fourierclim  46611  fourier  46612  fouriersw  46618  etransclem41  46662  etransclem46  46667  salexct2  46726  salexct3  46729  salgencntex  46730  salgensscntex  46731  dmvolsal  46733  bor1sal  46742  iocborel  46743  sge00  46763  sge0sn  46766  ovolval5lem3  47041  ioosshoi  47056  vonioolem2  47068  smfmullem4  47181  nthrucw  47273  cjnpoly  47278  dfafv2  47521  ichim  47846  grlimedgnedg  48520  nelsubc3  49459  fucofulem2  49699  setc2othin  49854  setcsnterm  49878  setc1obas  49880  setc1ohomfval  49881  setc1ocofval  49882  setc1oid  49883  termc2  49906  setc1onsubc  49990  onsetrec  50096  joinlmuladdmuli  50161