Theorem mptru 1554

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

Syntax hints:   → wi 4  ⊤wtru 1548

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 208  df-tru 1550

This theorem is referenced by:  hadbi123i  1603  cadbi123i  1618  nfan  1906  nfbi  1910  spimefv  2210  spime  2397  nfsb  2531  nfmov  2564  nfmo  2566  nfeuw  2597  nfeu  2598  eqabi  2874  eqabri  2881  nfeq  2914  nfel  2915  dvelimc  2926  nfrexw  3287  nfral  3338  nfrex  3339  nfrmo  3389  nfreu  3390  rabbia2  3394  rabeqc  3403  nfrab  3429  reuxfr  3690  reuxfr1  3693  nfsbc1  3742  nfsbcw  3745  nfsbc  3748  sbcbii  3779  csbeq2i  3839  nfcsb1  3854  nfcsbw  3857  nfcsb  3858  eqri  3935  ss2abi  3997  ss2rabi  4007  nfif  4485  nfdisjw  5051  nfdisj  5052  nfbr  5119  nfopab  5141  mpteq1i  5163  mpteq2ia  5167  mpteq12i  5169  ralxfr  5343  issoi  5562  nfiotaw  6445  nfiota  6447  nfriota  7325  nfov  7386  mpoeq123i  7432  mpoeq3ia  7434  opco1i  8064  xpord2indlem  8087  on2recsfn  8593  on2recsov  8594  iseri  8661  nfixpw  8854  nfixp  8855  en2i  8927  en3i  8928  ensymb  8939  entr  8943  1sdom2dom  9154  nfttrcl  9623  djulf1o  9827  djurf1o  9828  r0weon  9925  recmulnq  10878  nrex1  10978  nfneg  11380  negiso  12127  suprzcl2  12879  supxr  13256  xrinf0  13282  fac0  14229  cnrecnv  15118  cau3  15309  cbvsum  15648  cbvsumv  15649  sum0  15674  ackbijnn  15784  flo1  15810  trireciplem  15818  trirecip  15819  ege2le3  16046  rpnnen2lem3  16174  ruclem4  16192  bitsf1ocnv  16404  prmreclem6  16883  prmrec  16884  modxai  17030  strfvn  17147  strss  17167  xpsvsca  17532  mreacs  17615  2oppccomf  17682  setc2obas  18052  setc2ohom  18053  cat1  18055  chnflenfi  18585  chninf  18592  mndprop  18719  grpprop  18919  isgrpi  18926  oppgmndb  19321  oppggrpb  19324  odfval  19498  efgrelexlemb  19716  ablprop  19759  ringprop  20262  opprrngb  20317  opprringb  20319  rlmbas  21183  rlmplusg  21184  rlm0  21185  rlmsub  21186  rlmmulr  21187  rlmsca2  21189  rlmvsca  21190  rlmtopn  21191  rlmds  21192  rlmvneg  21196  cncrng  21368  xrsmcmn  21370  cndrng  21376  cnsrng  21381  absabv  21399  xrs1mnd  21415  xrs10  21416  zringcyg  21444  pzriprngALT  21470  resrng  21596  psrbagsn  22039  evlsval  22062  psr1bas2  22175  psr1bas  22176  psr1plusg  22205  psr1vsca  22206  psr1mulr  22207  ply1plusgfvi  22226  ply1mpl0  22241  ply1mpl1  22243  ordtrestixx  23205  llyidm  23471  nllyidm  23472  toplly  23473  hauslly  23475  hausnlly  23476  lly1stc  23479  kgenf  23524  txswaphmeolem  23787  fmucndlem  24273  nrgtrg  24673  cnfldnm  24761  xrsxmet  24793  divcn  24853  expcn  24857  elcncf1ii  24881  iirevcn  24915  iihalf1cn  24917  iihalf2cn  24919  iimulcn  24923  icopnfcnv  24927  iccpnfcnv  24929  cnrehmeo  24938  tcphsub  25206  tcphphl  25212  iscmet3i  25297  cncmet  25307  rrxprds  25374  vitali  25598  i1f0  25672  itg20  25722  cbvitgv  25762  dvid  25903  dveflem  25964  dvef  25965  dvsincos  25966  ply1divalg2  26122  coe0  26239  iaa  26309  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  cxpcn2  26728  resqrtcn  26731  sqrtcn  26732  atansopn  26914  dvatan  26917  leibpilem2  26923  leibpi  26924  leibpisum  26925  log2cnv  26926  log2ublem2  26929  log2ub  26931  divsqrtsumlem  26961  emcllem4  26980  emcllem6  26982  emcllem7  26983  lgamf  27023  lgam1  27045  basellem6  27067  basellem7  27068  basellem8  27069  basellem9  27070  vmaf  27100  logfacrlim  27205  lgsdir2lem5  27310  chebbnd1  27453  chtppilim  27456  chto1ub  27457  chebbnd2  27458  chto1lb  27459  chpchtlim  27460  chpo1ub  27461  chpo1ubb  27462  vmadivsum  27463  vmadivsumb  27464  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  logdivsum  27514  vmalogdivsum2  27519  vmalogdivsum  27520  selberglem1  27526  selberglem2  27527  selbergb  27530  selberg2lem  27531  selberg2  27532  selberg2b  27533  selberg3lem2  27539  selberg3  27540  selberg4  27542  pntrmax  27545  pntrsumo1  27546  pntrsumbnd  27547  selbergr  27549  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem4  27561  pnt2  27594  pnt  27595  dmcuts  27801  lrrecpo  27951  noxpordpo  27960  noxpordfr  27961  noxpordse  27962  n0ssno  28330  0n0s  28339  n0cut  28344  n0sge0  28348  zseo  28432  twocut  28433  nohalf  28434  halfcut  28468  bdaypw2n0bndlem  28473  0reno  28506  1reno  28507  istrkg2ld  28546  legval  28670  ttgsub  28965  cchhllem  28973  2wspdisj  30051  2wspiundisj  30052  konigsbergiedgw  30336  ipasslem7  30925  normlem6  31204  opsqrlem4  32232  fpwrelmap  32825  fpwrelmapffs  32826  sgn3da  32926  xrs0  33085  elrgspnlem2  33324  1fldgenq  33406  dfprm3  33636  zringfrac  33637  0mplrim  33698  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  35415  sinccvglem  35900  circum  35902  antnest  35917  antnestALT  35922  faclim  35974  faclim2  35976  cnndvlem1  36843  bj-alextruim  36977  bj-dvelimv  37206  bj-inrab2  37281  bj-rabtrAUTO  37285  bj-opelidb  37512  bj-iomnnom  37619  sucneqoni  37728  wl-df-3xor  37830  wl-3xorbi123i  37838  wl-df3maxtru1  37854  wl-cbvalnae  37904  wl-equsal  37912  poimirlem30  38017  dvtan  38037  dvasin  38071  dvacos  38072  dvreasin  38073  dvreacos  38074  efald2  38445  lcmineqlem7  42520  3lexlogpow5ineq1  42539  3lexlogpow5ineq5  42545  aks4d1p1p6  42558  cxpi11d  42820  tan3rdpi  42829  asin1half  42834  redvmptabs  42837  readvrec2  42838  readvrec  42839  resuppsinopn  42840  readvcot  42841  re1m1e0m0  42874  re0m0e0  42879  reixi  42900  subresre  42908  3cubeslem4  43138  3cubes  43139  areaquad  43661  clsk1indlem4  44488  clsk1indlem1  44489  ismnushort  44745  lhe4.4ex1a  44773  sbtT  45011  eel0TT  45147  eelTTT  45149  eelT1  45151  eelTT  45214  eelT  45216  eelT0  45218  isosctrlem1ALT  45377  disjsnxp  45518  infxr  45811  nfxneg  45904  limsup0  46137  0cnv  46185  limsup10ex  46216  liminf10ex  46217  liminfvalxr  46226  liminf0  46236  dvsinax  46356  itgsin0pilem1  46393  iblempty  46408  stowei  46507  wallispilem5  46512  wallispi  46513  stirlinglem1  46517  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlingr  46533  dirkertrigeqlem1  46541  fourierdlem62  46611  fourierdlem73  46622  fourierdlem76  46625  fourierdlem77  46626  fourierdlem103  46652  fourierdlem104  46653  fourierclim  46667  fourier  46668  fouriersw  46674  etransclem41  46718  etransclem46  46723  salexct2  46782  salexct3  46785  salgencntex  46786  salgensscntex  46787  dmvolsal  46789  bor1sal  46798  iocborel  46799  sge00  46819  sge0sn  46822  ovolval5lem3  47097  ioosshoi  47112  vonioolem2  47124  smfmullem4  47237  nthrucw  47331  goldrasin  47345  goldrapos  47346  cjnpoly  47352  dfafv2  47595  ichim  47932  grlimedgnedg  48622  nelsubc3  49561  fucofulem2  49801  setc2othin  49956  setcsnterm  49980  setc1obas  49982  setc1ohomfval  49983  setc1ocofval  49984  setc1oid  49985  termc2  50008  setc1onsubc  50092  onsetrec  50198  joinlmuladdmuli  50263