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  2393  nfsb  2527  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  eqabi  2871  eqabri  2878  nfeq  2912  nfel  2913  dvelimc  2924  nfrexw  3285  nfral  3336  nfrex  3337  nfrmo  3387  nfreu  3388  rabbia2  3392  rabeqc  3401  nfrab  3427  reuxfr  3695  reuxfr1  3698  nfsbc1  3747  nfsbcw  3750  nfsbc  3753  sbcbii  3785  csbeq2i  3845  nfcsb1  3860  nfcsbw  3863  nfcsb  3864  eqri  3942  ss2abi  4006  ss2rabi  4016  nfif  4497  nfdisjw  5064  nfdisj  5065  nfbr  5132  nfopab  5154  mpteq1i  5176  mpteq2ia  5180  mpteq12i  5182  ralxfr  5356  issoi  5575  nfiotaw  6458  nfiota  6460  nfriota  7336  nfov  7397  mpoeq123i  7443  mpoeq3ia  7445  opco1i  8075  xpord2indlem  8097  on2recsfn  8603  on2recsov  8604  iseri  8671  nfixpw  8864  nfixp  8865  en2i  8937  en3i  8938  ensymb  8949  entr  8953  1sdom2dom  9164  nfttrcl  9632  djulf1o  9836  djurf1o  9837  r0weon  9934  recmulnq  10887  nrex1  10987  nfneg  11389  negiso  12136  suprzcl2  12888  supxr  13265  xrinf0  13291  fac0  14238  cnrecnv  15127  cau3  15318  cbvsum  15657  cbvsumv  15658  sum0  15683  ackbijnn  15793  flo1  15819  trireciplem  15827  trirecip  15828  ege2le3  16055  rpnnen2lem3  16183  ruclem4  16201  bitsf1ocnv  16413  prmreclem6  16892  prmrec  16893  modxai  17039  strfvn  17156  strss  17176  xpsvsca  17541  mreacs  17624  2oppccomf  17691  setc2obas  18061  setc2ohom  18062  cat1  18064  chnflenfi  18594  chninf  18601  mndprop  18728  grpprop  18928  isgrpi  18935  oppgmndb  19330  oppggrpb  19333  odfval  19507  efgrelexlemb  19725  ablprop  19768  ringprop  20271  opprrngb  20326  opprringb  20328  rlmbas  21188  rlmplusg  21189  rlm0  21190  rlmsub  21191  rlmmulr  21192  rlmsca2  21194  rlmvsca  21195  rlmtopn  21196  rlmds  21197  rlmvneg  21201  cncrng  21373  xrsmcmn  21375  cndrng  21381  cnsrng  21386  absabv  21404  xrs1mnd  21420  xrs10  21421  zringcyg  21449  pzriprngALT  21475  resrng  21601  psrbagsn  22041  evlsval  22064  psr1bas2  22153  psr1bas  22154  psr1plusg  22184  psr1vsca  22185  psr1mulr  22186  ply1plusgfvi  22205  ply1mpl0  22220  ply1mpl1  22222  ordtrestixx  23187  llyidm  23453  nllyidm  23454  toplly  23455  hauslly  23457  hausnlly  23458  lly1stc  23461  kgenf  23506  txswaphmeolem  23769  fmucndlem  24255  nrgtrg  24655  cnfldnm  24743  xrsxmet  24775  divcn  24835  expcn  24839  elcncf1ii  24863  iirevcn  24897  iihalf1cn  24899  iihalf2cn  24901  iimulcn  24905  icopnfcnv  24909  iccpnfcnv  24911  cnrehmeo  24920  tcphsub  25188  tcphphl  25194  iscmet3i  25279  cncmet  25289  rrxprds  25356  vitali  25580  i1f0  25654  itg20  25704  cbvitgv  25744  dvid  25885  dveflem  25946  dvef  25947  dvsincos  25948  ply1divalg2  26104  coe0  26221  iaa  26291  sincn  26409  coscn  26410  reefgim  26415  pilem3  26418  resinf1o  26500  circgrp  26516  circsubm  26517  logi  26551  divlogrlim  26599  dvrelog  26601  logcn  26611  dvlog  26615  advlog  26618  cxpcn  26709  cxpcn2  26710  resqrtcn  26713  sqrtcn  26714  atansopn  26896  dvatan  26899  leibpilem2  26905  leibpi  26906  leibpisum  26907  log2cnv  26908  log2ublem2  26911  log2ub  26913  divsqrtsumlem  26943  emcllem4  26962  emcllem6  26964  emcllem7  26965  lgamf  27005  lgam1  27027  basellem6  27049  basellem7  27050  basellem8  27051  basellem9  27052  vmaf  27082  logfacrlim  27187  lgsdir2lem5  27292  chebbnd1  27435  chtppilim  27438  chto1ub  27439  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  chpo1ubb  27444  vmadivsum  27445  vmadivsumb  27446  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  logdivsum  27496  vmalogdivsum2  27501  vmalogdivsum  27502  selberglem1  27508  selberglem2  27509  selbergb  27512  selberg2lem  27513  selberg2  27514  selberg2b  27515  selberg3lem2  27521  selberg3  27522  selberg4  27524  pntrmax  27527  pntrsumo1  27528  pntrsumbnd  27529  selbergr  27531  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem4  27543  pnt2  27576  pnt  27577  dmcuts  27783  lrrecpo  27933  noxpordpo  27942  noxpordfr  27943  noxpordse  27944  n0ssno  28312  0n0s  28321  n0cut  28326  n0sge0  28330  zseo  28414  twocut  28415  nohalf  28416  halfcut  28450  bdaypw2n0bndlem  28455  0reno  28488  1reno  28489  istrkg2ld  28528  legval  28652  ttgsub  28947  cchhllem  28955  2wspdisj  30033  2wspiundisj  30034  konigsbergiedgw  30318  ipasslem7  30907  normlem6  31186  opsqrlem4  32214  fpwrelmap  32806  fpwrelmapffs  32807  sgn3da  32907  xrs0  33066  elrgspnlem2  33304  1fldgenq  33383  dfprm3  33613  zringfrac  33614  ccfldsrarelvec  33815  ccfldextdgrr  33816  constrextdg2  33893  iconstr  33910  constrsdrg  33919  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  mdetlap1  33970  circtopn  33981  cnre2csqima  34055  cnvordtrestixx  34057  mndpluscn  34070  xrge0iifcnv  34077  zlm0  34104  zlm1  34105  qqhre  34164  rrhre  34165  esumnul  34192  hasheuni  34229  sxbrsigalem2  34430  oddpwdc  34498  eulerpartlemb  34512  eulerpartgbij  34516  eulerpartlemn  34525  fib0  34543  fib1  34544  ballotlemrinv  34678  signsw0g  34700  circlemethnat  34785  dvelimalcasei  35218  dvelimexcasei  35220  subfacval2  35369  sinccvglem  35854  circum  35856  antnest  35871  antnestALT  35876  faclim  35928  faclim2  35930  cnndvlem1  36797  bj-alextruim  36931  bj-dvelimv  37160  bj-inrab2  37235  bj-rabtrAUTO  37239  bj-opelidb  37466  bj-iomnnom  37573  sucneqoni  37682  wl-df-3xor  37784  wl-3xorbi123i  37792  wl-df3maxtru1  37808  wl-cbvalnae  37858  wl-equsal  37866  poimirlem30  37971  dvtan  37991  dvasin  38025  dvacos  38026  dvreasin  38027  dvreacos  38028  efald2  38399  lcmineqlem7  42474  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p6  42512  cxpi11d  42775  tan3rdpi  42784  asin1half  42789  redvmptabs  42792  readvrec2  42793  readvrec  42794  resuppsinopn  42795  readvcot  42796  re1m1e0m0  42829  re0m0e0  42834  reixi  42855  subresre  42863  3cubeslem4  43121  3cubes  43122  areaquad  43644  clsk1indlem4  44471  clsk1indlem1  44472  ismnushort  44728  lhe4.4ex1a  44756  sbtT  44994  eel0TT  45130  eelTTT  45132  eelT1  45134  eelTT  45197  eelT  45199  eelT0  45201  isosctrlem1ALT  45360  disjsnxp  45501  infxr  45796  nfxneg  45889  limsup0  46122  0cnv  46170  limsup10ex  46201  liminf10ex  46202  liminfvalxr  46211  liminf0  46221  dvsinax  46341  itgsin0pilem1  46378  iblempty  46393  stowei  46492  wallispilem5  46497  wallispi  46498  stirlinglem1  46502  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlingr  46518  dirkertrigeqlem1  46526  fourierdlem62  46596  fourierdlem73  46607  fourierdlem76  46610  fourierdlem77  46611  fourierdlem103  46637  fourierdlem104  46638  fourierclim  46652  fourier  46653  fouriersw  46659  etransclem41  46703  etransclem46  46708  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  dmvolsal  46774  bor1sal  46783  iocborel  46784  sge00  46804  sge0sn  46807  ovolval5lem3  47082  ioosshoi  47097  vonioolem2  47109  smfmullem4  47222  nthrucw  47316  goldrasin  47330  goldrapos  47331  cjnpoly  47337  dfafv2  47580  ichim  47917  grlimedgnedg  48607  nelsubc3  49546  fucofulem2  49786  setc2othin  49941  setcsnterm  49965  setc1obas  49967  setc1ohomfval  49968  setc1ocofval  49969  setc1oid  49970  termc2  49993  setc1onsubc  50077  onsetrec  50183  joinlmuladdmuli  50248