Theorem mptru 1543

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

Syntax hints:   → wi 4  ⊤wtru 1537

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 209  df-tru 1539

This theorem is referenced by:  hadbi123i  1595  cadbi123i  1611  nfan  1899  nfbi  1903  spimefv  2197  spime  2406  nfsb  2564  nfmov  2643  nfmo  2645  nfeuw  2678  nfeu  2679  abeq2i  2951  abbi2i  2956  nfceqiOLD  2977  nfeq  2994  nfel  2995  dvelimc  3009  nfralw  3228  nfral  3229  nfrex  3312  nfrexg  3313  nfreuw  3377  nfrmow  3378  nfreu  3379  nfrmo  3380  nfrabw  3388  nfrab  3389  rabbia2  3480  reuxfr  3743  reuxfr1  3746  nfsbc1  3794  nfsbcw  3797  nfsbc  3800  sbcbii  3832  csbeq2i  3894  nfcsb1  3909  nfcsbw  3912  nfcsb  3913  eqri  3990  nfif  4499  nfdisjw  5046  nfdisj  5047  nfbr  5116  mpteq12i  5162  ralxfr  5318  issoi  5510  nfiotaw  6321  nfiota  6323  nfriota  7129  nfov  7189  mpoeq123i  7233  mpoeq3ia  7235  iseri  8319  nfixpw  8483  nfixp  8484  en2i  8550  en3i  8551  ensymb  8560  entr  8564  djulf1o  9344  djurf1o  9345  r0weon  9441  recmulnq  10389  nrex1  10489  nfneg  10885  negiso  11624  suprzcl2  12341  supxr  12709  xrinf0  12734  fac0  13639  cnrecnv  14527  cau3  14718  cbvsum  15055  sum0  15081  ackbijnn  15186  flo1  15212  trireciplem  15220  trirecip  15221  ege2le3  15446  rpnnen2lem3  15572  ruclem4  15590  bitsf1ocnv  15796  prmreclem6  16260  prmrec  16261  modxai  16407  strfvn  16508  strss  16537  xpsvsca  16853  mreacs  16932  2oppccomf  16998  mndprop  17940  grpprop  18122  isgrpi  18129  oppgmndb  18486  oppggrpb  18489  odfval  18663  efgrelexlemb  18879  ablprop  18921  ringprop  19337  opprringb  19385  rlmbas  19970  rlmplusg  19971  rlm0  19972  rlmsub  19973  rlmmulr  19974  rlmsca2  19976  rlmvsca  19977  rlmtopn  19978  rlmds  19979  rlmvneg  19983  psrbagsn  20278  evlsval  20302  psr1bas2  20361  psr1bas  20362  psr1plusg  20393  psr1vsca  20394  psr1mulr  20395  ply1plusgfvi  20413  ply1mpl0  20426  ply1mpl1  20428  cncrng  20569  xrsmcmn  20571  cndrng  20577  cnsrng  20582  xrs1mnd  20586  xrs10  20587  absabv  20605  zringcyg  20641  recrng  20768  ordtrestixx  21833  llyidm  22099  nllyidm  22100  toplly  22101  hauslly  22103  hausnlly  22104  lly1stc  22107  kgenf  22152  txswaphmeolem  22415  fmucndlem  22903  nrgtrg  23302  cnfldnm  23390  xrsxmet  23420  divcn  23479  expcn  23483  elcncf1ii  23507  iirevcn  23537  iihalf1cn  23539  iihalf2cn  23541  iimulcn  23545  icopnfcnv  23549  iccpnfcnv  23551  cnrehmeo  23560  tcphsub  23827  tcphphl  23833  iscmet3i  23918  cncmet  23928  rrxprds  23995  vitali  24217  i1f0  24291  itg20  24341  dvid  24518  dveflem  24579  dvef  24580  dvsincos  24581  ply1divalg2  24735  coe0  24849  iaa  24917  sincn  25035  coscn  25036  reefgim  25041  pilem3  25044  resinf1o  25123  circgrp  25139  circsubm  25140  divlogrlim  25221  dvrelog  25223  logcn  25233  dvlog  25237  advlog  25240  cxpcn  25329  cxpcn2  25330  resqrtcn  25333  sqrtcn  25334  atansopn  25513  dvatan  25516  leibpilem2  25522  leibpi  25523  leibpisum  25524  log2cnv  25525  log2ublem2  25528  log2ub  25530  divsqrtsumlem  25560  emcllem4  25579  emcllem6  25581  emcllem7  25582  lgamf  25622  lgam1  25644  basellem6  25666  basellem7  25667  basellem8  25668  basellem9  25669  vmaf  25699  logfacrlim  25803  lgsdir2lem5  25908  chebbnd1  26051  chtppilim  26054  chto1ub  26055  chebbnd2  26056  chto1lb  26057  chpchtlim  26058  chpo1ub  26059  chpo1ubb  26060  vmadivsum  26061  vmadivsumb  26062  mudivsum  26109  mulogsumlem  26110  mulogsum  26111  logdivsum  26112  vmalogdivsum2  26117  vmalogdivsum  26118  selberglem1  26124  selberglem2  26125  selbergb  26128  selberg2lem  26129  selberg2  26130  selberg2b  26131  selberg3lem2  26137  selberg3  26138  selberg4  26140  pntrmax  26143  pntrsumo1  26144  pntrsumbnd  26145  selbergr  26147  selberg3r  26148  selberg4r  26149  selberg34r  26150  pntrlog2bndlem1  26156  pntrlog2bndlem4  26159  pnt2  26192  pnt  26193  istrkg2ld  26249  legval  26373  ttgsub  26668  cchhllem  26676  trlsfval  27480  pthsfval  27505  spthsfval  27506  clwlks  27556  crcts  27572  cycls  27573  2wspdisj  27744  2wspiundisj  27745  eupths  27982  konigsbergiedgw  28030  ipasslem7  28616  normlem6  28895  opsqrlem4  29923  fpwrelmap  30472  fpwrelmapffs  30473  xrs0  30666  ccfldsrarelvec  31060  ccfldextdgrr  31061  mdetlap1  31095  circtopn  31105  cnre2csqima  31158  cnvordtrestixx  31160  mndpluscn  31173  xrge0iifcnv  31180  zlm0  31207  zlm1  31208  qqhre  31265  rrhre  31266  esumnul  31311  hasheuni  31348  sxbrsigalem2  31548  oddpwdc  31616  eulerpartlemb  31630  eulerpartgbij  31634  eulerpartlemn  31643  fib0  31661  fib1  31662  ballotlemrinv  31795  sgn3da  31803  signsw0g  31830  circlemethnat  31916  subfacval2  32438  sinccvglem  32919  circum  32921  logi  32970  faclim  32982  faclim2  32984  dmscut  33276  cnndvlem1  33880  bj-dvelimv  34181  bj-inrab2  34250  bj-rabtrAUTO  34254  bj-opelidb  34448  bj-iomnnom  34545  sucneqoni  34651  wl-cbvalnae  34777  wl-equsal  34784  poimirlem30  34926  dvtan  34946  dvasin  34982  dvacos  34983  dvreasin  34984  dvreacos  34985  efald2  35360  re1m1e0m0  39233  re0m0e0  39238  3cubeslem4  39292  3cubes  39293  areaquad  39829  clsk1indlem4  40400  clsk1indlem1  40401  lhe4.4ex1a  40667  sbtT  40907  eel0TT  41044  eelTTT  41046  eelT1  41048  eelTT  41111  eelT  41113  eelT0  41115  isosctrlem1ALT  41274  disjsnxp  41338  infxr  41641  nfxneg  41743  limsup0  41981  0cnv  42029  limsup10ex  42060  liminf10ex  42061  liminfvalxr  42070  liminf0  42080  dvsinax  42203  itgsin0pilem1  42241  iblempty  42256  stowei  42356  wallispilem5  42361  wallispi  42362  stirlinglem1  42366  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlingr  42382  dirkertrigeqlem1  42390  fourierdlem62  42460  fourierdlem73  42471  fourierdlem76  42474  fourierdlem77  42475  fourierdlem103  42501  fourierdlem104  42502  fourierclim  42516  fourier  42517  fouriersw  42523  etransclem41  42567  etransclem46  42572  salexct2  42629  salexct3  42632  salgencntex  42633  salgensscntex  42634  dmvolsal  42636  bor1sal  42645  iocborel  42646  sge00  42665  sge0sn  42668  ovolval5lem3  42943  ioosshoi  42958  vonioolem2  42970  smfmullem4  43076  dfafv2  43338  onsetrec  44817  joinlmuladdmuli  44881