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

This theorem is referenced by:  hadbi123i  1597  cadbi123i  1612  nfan  1900  nfbi  1904  spimefv  2201  spime  2389  nfsb  2523  nfmov  2555  nfmo  2557  nfeuw  2588  nfeu  2589  eqabi  2866  eqabri  2874  nfeq  2908  nfel  2909  dvelimc  2920  nfrexw  3280  nfral  3340  nfrex  3341  nfrmo  3393  nfreu  3394  rabbia2  3398  rabeqc  3407  nfrabw  3432  nfrab  3434  reuxfr  3703  reuxfr1  3706  nfsbc1  3755  nfsbcw  3758  nfsbc  3761  sbcbii  3793  csbeq2i  3853  nfcsb1  3868  nfcsbw  3871  nfcsb  3872  eqri  3950  nfif  4503  nfdisjw  5068  nfdisj  5069  nfbr  5136  nfopab  5158  mpteq1i  5180  mpteq2ia  5184  mpteq12i  5186  ralxfr  5350  issoi  5558  nfiotaw  6441  nfiota  6443  nfriota  7315  nfov  7376  mpoeq123i  7422  mpoeq3ia  7424  opco1i  8055  xpord2indlem  8077  on2recsfn  8582  on2recsov  8583  iseri  8649  nfixpw  8840  nfixp  8841  en2i  8912  en3i  8913  ensymb  8924  entr  8928  1sdom2dom  9138  nfttrcl  9601  djulf1o  9805  djurf1o  9806  r0weon  9903  recmulnq  10855  nrex1  10955  nfneg  11356  negiso  12102  suprzcl2  12836  supxr  13212  xrinf0  13238  fac0  14183  cnrecnv  15072  cau3  15263  cbvsum  15602  cbvsumv  15603  sum0  15628  ackbijnn  15735  flo1  15761  trireciplem  15769  trirecip  15770  ege2le3  15997  rpnnen2lem3  16125  ruclem4  16143  bitsf1ocnv  16355  prmreclem6  16833  prmrec  16834  modxai  16980  strfvn  17097  strss  17117  xpsvsca  17481  mreacs  17564  2oppccomf  17631  setc2obas  18001  setc2ohom  18002  cat1  18004  chnflenfi  18534  chninf  18541  mndprop  18668  grpprop  18865  isgrpi  18872  oppgmndb  19267  oppggrpb  19270  odfval  19444  efgrelexlemb  19662  ablprop  19705  ringprop  20208  opprrngb  20264  opprringb  20266  rlmbas  21127  rlmplusg  21128  rlm0  21129  rlmsub  21130  rlmmulr  21131  rlmsca2  21133  rlmvsca  21134  rlmtopn  21135  rlmds  21136  rlmvneg  21140  dfcnfldOLD  21307  cncrng  21325  cncrngOLD  21326  xrsmcmn  21328  cndrng  21335  cndrngOLD  21336  cnsrng  21342  absabv  21361  xrs1mnd  21377  xrs10  21378  zringcyg  21406  pzriprngALT  21432  resrng  21558  psrbagsn  21998  evlsval  22021  psr1bas2  22102  psr1bas  22103  psr1plusg  22133  psr1vsca  22134  psr1mulr  22135  ply1plusgfvi  22154  ply1mpl0  22169  ply1mpl1  22171  ordtrestixx  23137  llyidm  23403  nllyidm  23404  toplly  23405  hauslly  23407  hausnlly  23408  lly1stc  23411  kgenf  23456  txswaphmeolem  23719  fmucndlem  24205  nrgtrg  24605  cnfldnm  24693  xrsxmet  24725  divcnOLD  24784  divcn  24786  expcn  24790  expcnOLD  24792  elcncf1ii  24816  iirevcn  24851  iihalf1cn  24853  iihalf1cnOLD  24854  iihalf2cn  24856  iihalf2cnOLD  24857  iimulcn  24861  iimulcnOLD  24862  icopnfcnv  24867  iccpnfcnv  24869  cnrehmeo  24878  cnrehmeoOLD  24879  tcphsub  25148  tcphphl  25154  iscmet3i  25239  cncmet  25249  rrxprds  25316  vitali  25541  i1f0  25615  itg20  25665  cbvitgv  25705  dvid  25846  dveflem  25910  dvef  25911  dvsincos  25912  ply1divalg2  26071  coe0  26188  iaa  26260  sincn  26381  coscn  26382  reefgim  26387  pilem3  26390  resinf1o  26472  circgrp  26488  circsubm  26489  logi  26523  divlogrlim  26571  dvrelog  26573  logcn  26583  dvlog  26587  advlog  26590  cxpcn  26681  cxpcnOLD  26682  cxpcn2  26683  resqrtcn  26686  sqrtcn  26687  atansopn  26869  dvatan  26872  leibpilem2  26878  leibpi  26879  leibpisum  26880  log2cnv  26881  log2ublem2  26884  log2ub  26886  divsqrtsumlem  26917  emcllem4  26936  emcllem6  26938  emcllem7  26939  lgamf  26979  lgam1  27001  basellem6  27023  basellem7  27024  basellem8  27025  basellem9  27026  vmaf  27056  logfacrlim  27162  lgsdir2lem5  27267  chebbnd1  27410  chtppilim  27413  chto1ub  27414  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ub  27418  chpo1ubb  27419  vmadivsum  27420  vmadivsumb  27421  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  logdivsum  27471  vmalogdivsum2  27476  vmalogdivsum  27477  selberglem1  27483  selberglem2  27484  selbergb  27487  selberg2lem  27488  selberg2  27489  selberg2b  27490  selberg3lem2  27496  selberg3  27497  selberg4  27499  pntrmax  27502  pntrsumo1  27503  pntrsumbnd  27504  selbergr  27506  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntrlog2bndlem1  27515  pntrlog2bndlem4  27518  pnt2  27551  pnt  27552  dmscut  27752  lrrecpo  27884  noxpordpo  27893  noxpordfr  27894  noxpordse  27895  n0sex  28246  n0ssno  28249  0n0s  28258  n0scut  28262  n0sge0  28266  1p1e2s  28339  zseo  28345  twocut  28346  nohalf  28347  halfcut  28378  0reno  28399  istrkg2ld  28438  legval  28562  ttgsub  28857  cchhllem  28865  2wspdisj  29943  2wspiundisj  29944  konigsbergiedgw  30228  ipasslem7  30816  normlem6  31095  opsqrlem4  32123  fpwrelmap  32716  fpwrelmapffs  32717  sgn3da  32817  xrs0  32987  elrgspnlem2  33210  1fldgenq  33288  dfprm3  33518  zringfrac  33519  ccfldsrarelvec  33684  ccfldextdgrr  33685  constrextdg2  33762  iconstr  33779  constrsdrg  33788  2sqr3minply  33793  2sqr3nconstr  33794  cos9thpiminplylem3  33797  cos9thpiminply  33801  cos9thpinconstrlem1  33802  cos9thpinconstrlem2  33803  mdetlap1  33839  circtopn  33850  cnre2csqima  33924  cnvordtrestixx  33926  mndpluscn  33939  xrge0iifcnv  33946  zlm0  33973  zlm1  33974  qqhre  34033  rrhre  34034  esumnul  34061  hasheuni  34098  sxbrsigalem2  34299  oddpwdc  34367  eulerpartlemb  34381  eulerpartgbij  34385  eulerpartlemn  34394  fib0  34412  fib1  34413  ballotlemrinv  34547  signsw0g  34569  circlemethnat  34654  dvelimalcasei  35088  dvelimexcasei  35090  subfacval2  35231  sinccvglem  35716  circum  35718  antnest  35733  antnestALT  35738  faclim  35790  faclim2  35792  cnndvlem1  36579  bj-dvelimv  36895  bj-inrab2  36970  bj-rabtrAUTO  36974  bj-opelidb  37194  bj-iomnnom  37301  sucneqoni  37408  wl-df-3xor  37510  wl-3xorbi123i  37518  wl-df3maxtru1  37534  wl-cbvalnae  37575  wl-equsal  37583  poimirlem30  37698  dvtan  37718  dvasin  37752  dvacos  37753  dvreasin  37754  dvreacos  37755  efald2  38126  lcmineqlem7  42076  3lexlogpow5ineq1  42095  3lexlogpow5ineq5  42101  aks4d1p1p6  42114  cxpi11d  42384  tan3rdpi  42393  asin1half  42398  redvmptabs  42401  readvrec2  42402  readvrec  42403  resuppsinopn  42404  readvcot  42405  re1m1e0m0  42438  re0m0e0  42443  reixi  42464  subresre  42472  3cubeslem4  42730  3cubes  42731  areaquad  43257  clsk1indlem4  44085  clsk1indlem1  44086  ismnushort  44342  lhe4.4ex1a  44370  sbtT  44608  eel0TT  44744  eelTTT  44746  eelT1  44748  eelTT  44811  eelT  44813  eelT0  44815  isosctrlem1ALT  44974  disjsnxp  45115  infxr  45413  nfxneg  45507  limsup0  45740  0cnv  45788  limsup10ex  45819  liminf10ex  45820  liminfvalxr  45829  liminf0  45839  dvsinax  45959  itgsin0pilem1  45996  iblempty  46011  stowei  46110  wallispilem5  46115  wallispi  46116  stirlinglem1  46120  stirlinglem12  46131  stirlinglem13  46132  stirlinglem14  46133  stirlingr  46136  dirkertrigeqlem1  46144  fourierdlem62  46214  fourierdlem73  46225  fourierdlem76  46228  fourierdlem77  46229  fourierdlem103  46255  fourierdlem104  46256  fourierclim  46270  fourier  46271  fouriersw  46277  etransclem41  46321  etransclem46  46326  salexct2  46385  salexct3  46388  salgencntex  46389  salgensscntex  46390  dmvolsal  46392  bor1sal  46401  iocborel  46402  sge00  46422  sge0sn  46425  ovolval5lem3  46700  ioosshoi  46715  vonioolem2  46727  smfmullem4  46840  cjnpoly  46928  dfafv2  47171  ichim  47496  grlimedgnedg  48170  nelsubc3  49111  fucofulem2  49351  setc2othin  49506  setcsnterm  49530  setc1obas  49532  setc1ohomfval  49533  setc1ocofval  49534  setc1oid  49535  termc2  49558  setc1onsubc  49642  onsetrec  49748  joinlmuladdmuli  49813