Theorem mptru 1544

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

Syntax hints:   → wi 4  ⊤wtru 1538

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 1540

This theorem is referenced by:  hadbi123i  1596  cadbi123i  1612  nfan  1900  nfbi  1904  spimefv  2198  spime  2407  nfsb  2565  nfmov  2644  nfmo  2646  nfeuw  2679  nfeu  2680  abeq2i  2948  abbi2i  2953  nfceqiOLD  2974  nfeq  2991  nfel  2992  dvelimc  3006  nfralw  3225  nfral  3226  nfrex  3309  nfrexg  3310  nfreuw  3374  nfrmow  3375  nfreu  3376  nfrmo  3377  nfrabw  3385  nfrab  3386  rabbia2  3477  reuxfr  3740  reuxfr1  3743  nfsbc1  3791  nfsbcw  3794  nfsbc  3797  sbcbii  3829  csbeq2i  3891  nfcsb1  3906  nfcsbw  3909  nfcsb  3910  eqri  3987  nfif  4496  nfdisjw  5043  nfdisj  5044  nfbr  5113  mpteq12i  5159  ralxfr  5315  issoi  5507  nfiotaw  6318  nfiota  6320  nfriota  7126  nfov  7186  mpoeq123i  7230  mpoeq3ia  7232  iseri  8316  nfixpw  8480  nfixp  8481  en2i  8547  en3i  8548  ensymb  8557  entr  8561  djulf1o  9341  djurf1o  9342  r0weon  9438  recmulnq  10386  nrex1  10486  nfneg  10882  negiso  11621  suprzcl2  12339  supxr  12707  xrinf0  12732  fac0  13637  cnrecnv  14524  cau3  14715  cbvsum  15052  sum0  15078  ackbijnn  15183  flo1  15209  trireciplem  15217  trirecip  15218  ege2le3  15443  rpnnen2lem3  15569  ruclem4  15587  bitsf1ocnv  15793  prmreclem6  16257  prmrec  16258  modxai  16404  strfvn  16505  strss  16534  xpsvsca  16850  mreacs  16929  2oppccomf  16995  mndprop  17937  grpprop  18119  isgrpi  18126  oppgmndb  18483  oppggrpb  18486  odfval  18660  efgrelexlemb  18876  ablprop  18918  ringprop  19334  opprringb  19382  rlmbas  19967  rlmplusg  19968  rlm0  19969  rlmsub  19970  rlmmulr  19971  rlmsca2  19973  rlmvsca  19974  rlmtopn  19975  rlmds  19976  rlmvneg  19980  psrbagsn  20275  evlsval  20299  psr1bas2  20358  psr1bas  20359  psr1plusg  20390  psr1vsca  20391  psr1mulr  20392  ply1plusgfvi  20410  ply1mpl0  20423  ply1mpl1  20425  cncrng  20566  xrsmcmn  20568  cndrng  20574  cnsrng  20579  xrs1mnd  20583  xrs10  20584  absabv  20602  zringcyg  20638  recrng  20765  ordtrestixx  21830  llyidm  22096  nllyidm  22097  toplly  22098  hauslly  22100  hausnlly  22101  lly1stc  22104  kgenf  22149  txswaphmeolem  22412  fmucndlem  22900  nrgtrg  23299  cnfldnm  23387  xrsxmet  23417  divcn  23476  expcn  23480  elcncf1ii  23504  iirevcn  23534  iihalf1cn  23536  iihalf2cn  23538  iimulcn  23542  icopnfcnv  23546  iccpnfcnv  23548  cnrehmeo  23557  tcphsub  23824  tcphphl  23830  iscmet3i  23915  cncmet  23925  rrxprds  23992  vitali  24214  i1f0  24288  itg20  24338  dvid  24515  dveflem  24576  dvef  24577  dvsincos  24578  ply1divalg2  24732  coe0  24846  iaa  24914  sincn  25032  coscn  25033  reefgim  25038  pilem3  25041  resinf1o  25120  circgrp  25136  circsubm  25137  divlogrlim  25218  dvrelog  25220  logcn  25230  dvlog  25234  advlog  25237  cxpcn  25326  cxpcn2  25327  resqrtcn  25330  sqrtcn  25331  atansopn  25510  dvatan  25513  leibpilem2  25519  leibpi  25520  leibpisum  25521  log2cnv  25522  log2ublem2  25525  log2ub  25527  divsqrtsumlem  25557  emcllem4  25576  emcllem6  25578  emcllem7  25579  lgamf  25619  lgam1  25641  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  vmaf  25696  logfacrlim  25800  lgsdir2lem5  25905  chebbnd1  26048  chtppilim  26051  chto1ub  26052  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  chpo1ubb  26057  vmadivsum  26058  vmadivsumb  26059  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  logdivsum  26109  vmalogdivsum2  26114  vmalogdivsum  26115  selberglem1  26121  selberglem2  26122  selbergb  26125  selberg2lem  26126  selberg2  26127  selberg2b  26128  selberg3lem2  26134  selberg3  26135  selberg4  26137  pntrmax  26140  pntrsumo1  26141  pntrsumbnd  26142  selbergr  26144  selberg3r  26145  selberg4r  26146  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem4  26156  pnt2  26189  pnt  26190  istrkg2ld  26246  legval  26370  ttgsub  26665  cchhllem  26673  trlsfval  27477  pthsfval  27502  spthsfval  27503  clwlks  27553  crcts  27569  cycls  27570  2wspdisj  27741  2wspiundisj  27742  eupths  27979  konigsbergiedgw  28027  ipasslem7  28613  normlem6  28892  opsqrlem4  29920  fpwrelmap  30469  fpwrelmapffs  30470  xrs0  30662  ccfldsrarelvec  31056  ccfldextdgrr  31057  mdetlap1  31091  circtopn  31101  cnre2csqima  31154  cnvordtrestixx  31156  mndpluscn  31169  xrge0iifcnv  31176  zlm0  31203  zlm1  31204  qqhre  31261  rrhre  31262  esumnul  31307  hasheuni  31344  sxbrsigalem2  31544  oddpwdc  31612  eulerpartlemb  31626  eulerpartgbij  31630  eulerpartlemn  31639  fib0  31657  fib1  31658  ballotlemrinv  31791  sgn3da  31799  signsw0g  31826  circlemethnat  31912  subfacval2  32434  sinccvglem  32915  circum  32917  logi  32966  faclim  32978  faclim2  32980  dmscut  33272  cnndvlem1  33876  bj-dvelimv  34177  bj-inrab2  34249  bj-rabtrAUTO  34253  bj-opelidb  34447  bj-iomnnom  34544  sucneqoni  34650  wl-df-had  34748  wl-hadbi123i  34753  wl-cbvalnae  34788  wl-equsal  34795  poimirlem30  34937  dvtan  34957  dvasin  34993  dvacos  34994  dvreasin  34995  dvreacos  34996  efald2  35371  re1m1e0m0  39276  re0m0e0  39281  3cubeslem4  39335  3cubes  39336  areaquad  39872  clsk1indlem4  40443  clsk1indlem1  40444  lhe4.4ex1a  40710  sbtT  40950  eel0TT  41087  eelTTT  41089  eelT1  41091  eelTT  41154  eelT  41156  eelT0  41158  isosctrlem1ALT  41317  disjsnxp  41381  infxr  41684  nfxneg  41786  limsup0  42024  0cnv  42072  limsup10ex  42103  liminf10ex  42104  liminfvalxr  42113  liminf0  42123  dvsinax  42246  itgsin0pilem1  42284  iblempty  42299  stowei  42398  wallispilem5  42403  wallispi  42404  stirlinglem1  42408  stirlinglem12  42419  stirlinglem13  42420  stirlinglem14  42421  stirlingr  42424  dirkertrigeqlem1  42432  fourierdlem62  42502  fourierdlem73  42513  fourierdlem76  42516  fourierdlem77  42517  fourierdlem103  42543  fourierdlem104  42544  fourierclim  42558  fourier  42559  fouriersw  42565  etransclem41  42609  etransclem46  42614  salexct2  42671  salexct3  42674  salgencntex  42675  salgensscntex  42676  dmvolsal  42678  bor1sal  42687  iocborel  42688  sge00  42707  sge0sn  42710  ovolval5lem3  42985  ioosshoi  43000  vonioolem2  43012  smfmullem4  43118  dfafv2  43380  onsetrec  44859  joinlmuladdmuli  44923