Theorem mptru 1547

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

Syntax hints:   → wi 4  ⊤wtru 1541

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 1543

This theorem is referenced by:  hadbi123i  1596  cadbi123i  1611  nfan  1899  nfbi  1903  spimefv  2199  spime  2387  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  eqabi  2863  eqabri  2871  nfeq  2905  nfel  2906  dvelimc  2917  nfrexw  3277  nfral  3337  nfrex  3338  nfrmo  3392  nfreu  3393  rabbia2  3397  rabeqc  3407  nfrabw  3432  nfrab  3434  reuxfr  3709  reuxfr1  3712  nfsbc1  3761  nfsbcw  3764  nfsbc  3767  sbcbii  3799  csbeq2i  3859  nfcsb1  3874  nfcsbw  3877  nfcsb  3878  eqri  3956  vn0  4296  nfif  4507  nfdisjw  5071  nfdisj  5072  nfbr  5139  nfopab  5161  mpteq1i  5183  mpteq2ia  5187  mpteq12i  5189  ralxfr  5353  issoi  5563  nfiotaw  6442  nfiota  6444  nfriota  7318  nfov  7379  mpoeq123i  7425  mpoeq3ia  7427  opco1i  8058  xpord2indlem  8080  on2recsfn  8585  on2recsov  8586  iseri  8652  nfixpw  8843  nfixp  8844  en2i  8915  en3i  8916  ensymb  8927  entr  8931  1sdom2dom  9143  nfttrcl  9607  djulf1o  9808  djurf1o  9809  r0weon  9906  recmulnq  10858  nrex1  10958  nfneg  11359  negiso  12105  suprzcl2  12839  supxr  13215  xrinf0  13241  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  mndprop  18634  grpprop  18831  isgrpi  18838  oppgmndb  19234  oppggrpb  19237  odfval  19411  efgrelexlemb  19629  ablprop  19672  ringprop  20175  opprrngb  20231  opprringb  20233  rlmbas  21097  rlmplusg  21098  rlm0  21099  rlmsub  21100  rlmmulr  21101  rlmsca2  21103  rlmvsca  21104  rlmtopn  21105  rlmds  21106  rlmvneg  21110  dfcnfldOLD  21277  cncrng  21295  cncrngOLD  21296  xrsmcmn  21298  cndrng  21305  cndrngOLD  21306  cnsrng  21312  absabv  21331  xrs1mnd  21347  xrs10  21348  zringcyg  21376  pzriprngALT  21402  resrng  21528  psrbagsn  21968  evlsval  21991  psr1bas2  22072  psr1bas  22073  psr1plusg  22103  psr1vsca  22104  psr1mulr  22105  ply1plusgfvi  22124  ply1mpl0  22139  ply1mpl1  22141  ordtrestixx  23107  llyidm  23373  nllyidm  23374  toplly  23375  hauslly  23377  hausnlly  23378  lly1stc  23381  kgenf  23426  txswaphmeolem  23689  fmucndlem  24176  nrgtrg  24576  cnfldnm  24664  xrsxmet  24696  divcnOLD  24755  divcn  24757  expcn  24761  expcnOLD  24763  elcncf1ii  24787  iirevcn  24822  iihalf1cn  24824  iihalf1cnOLD  24825  iihalf2cn  24827  iihalf2cnOLD  24828  iimulcn  24832  iimulcnOLD  24833  icopnfcnv  24838  iccpnfcnv  24840  cnrehmeo  24849  cnrehmeoOLD  24850  tcphsub  25119  tcphphl  25125  iscmet3i  25210  cncmet  25220  rrxprds  25287  vitali  25512  i1f0  25586  itg20  25636  cbvitgv  25676  dvid  25817  dveflem  25881  dvef  25882  dvsincos  25883  ply1divalg2  26042  coe0  26159  iaa  26231  sincn  26352  coscn  26353  reefgim  26358  pilem3  26361  resinf1o  26443  circgrp  26459  circsubm  26460  logi  26494  divlogrlim  26542  dvrelog  26544  logcn  26554  dvlog  26558  advlog  26561  cxpcn  26652  cxpcnOLD  26653  cxpcn2  26654  resqrtcn  26657  sqrtcn  26658  atansopn  26840  dvatan  26843  leibpilem2  26849  leibpi  26850  leibpisum  26851  log2cnv  26852  log2ublem2  26855  log2ub  26857  divsqrtsumlem  26888  emcllem4  26907  emcllem6  26909  emcllem7  26910  lgamf  26950  lgam1  26972  basellem6  26994  basellem7  26995  basellem8  26996  basellem9  26997  vmaf  27027  logfacrlim  27133  lgsdir2lem5  27238  chebbnd1  27381  chtppilim  27384  chto1ub  27385  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ub  27389  chpo1ubb  27390  vmadivsum  27391  vmadivsumb  27392  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  logdivsum  27442  vmalogdivsum2  27447  vmalogdivsum  27448  selberglem1  27454  selberglem2  27455  selbergb  27458  selberg2lem  27459  selberg2  27460  selberg2b  27461  selberg3lem2  27467  selberg3  27468  selberg4  27470  pntrmax  27473  pntrsumo1  27474  pntrsumbnd  27475  selbergr  27477  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem1  27486  pntrlog2bndlem4  27489  pnt2  27522  pnt  27523  dmscut  27722  lrrecpo  27853  noxpordpo  27862  noxpordfr  27863  noxpordse  27864  n0sex  28215  n0ssno  28218  0n0s  28227  n0scut  28231  n0sge0  28235  1p1e2s  28308  zseo  28314  twocut  28315  nohalf  28316  halfcut  28346  0reno  28366  istrkg2ld  28405  legval  28529  ttgsub  28824  cchhllem  28832  2wspdisj  29907  2wspiundisj  29908  konigsbergiedgw  30192  ipasslem7  30780  normlem6  31059  opsqrlem4  32087  fpwrelmap  32676  fpwrelmapffs  32677  sgn3da  32779  xrs0  32960  elrgspnlem2  33183  1fldgenq  33261  dfprm3  33490  zringfrac  33491  ccfldsrarelvec  33638  ccfldextdgrr  33639  constrextdg2  33716  iconstr  33733  constrsdrg  33742  2sqr3minply  33747  2sqr3nconstr  33748  cos9thpiminplylem3  33751  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  mdetlap1  33793  circtopn  33804  cnre2csqima  33878  cnvordtrestixx  33880  mndpluscn  33893  xrge0iifcnv  33900  zlm0  33927  zlm1  33928  qqhre  33987  rrhre  33988  esumnul  34015  hasheuni  34052  sxbrsigalem2  34254  oddpwdc  34322  eulerpartlemb  34336  eulerpartgbij  34340  eulerpartlemn  34349  fib0  34367  fib1  34368  ballotlemrinv  34502  signsw0g  34524  circlemethnat  34609  dvelimalcasei  35043  dvelimexcasei  35045  subfacval2  35160  sinccvglem  35645  circum  35647  antnest  35662  antnestALT  35667  faclim  35719  faclim2  35721  cnndvlem1  36511  bj-dvelimv  36827  bj-inrab2  36902  bj-rabtrAUTO  36906  bj-opelidb  37126  bj-iomnnom  37233  sucneqoni  37340  wl-df-3xor  37442  wl-3xorbi123i  37450  wl-df3maxtru1  37466  wl-cbvalnae  37507  wl-equsal  37515  poimirlem30  37630  dvtan  37650  dvasin  37684  dvacos  37685  dvreasin  37686  dvreacos  37687  efald2  38058  lcmineqlem7  42008  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  aks4d1p1p6  42046  cxpi11d  42316  tan3rdpi  42325  asin1half  42330  redvmptabs  42333  readvrec2  42334  readvrec  42335  resuppsinopn  42336  readvcot  42337  re1m1e0m0  42370  re0m0e0  42375  reixi  42396  subresre  42404  3cubeslem4  42662  3cubes  42663  areaquad  43189  clsk1indlem4  44017  clsk1indlem1  44018  ismnushort  44274  lhe4.4ex1a  44302  sbtT  44541  eel0TT  44677  eelTTT  44679  eelT1  44681  eelTT  44744  eelT  44746  eelT0  44748  isosctrlem1ALT  44907  disjsnxp  45048  infxr  45346  nfxneg  45440  limsup0  45675  0cnv  45723  limsup10ex  45754  liminf10ex  45755  liminfvalxr  45764  liminf0  45774  dvsinax  45894  itgsin0pilem1  45931  iblempty  45946  stowei  46045  wallispilem5  46050  wallispi  46051  stirlinglem1  46055  stirlinglem12  46066  stirlinglem13  46067  stirlinglem14  46068  stirlingr  46071  dirkertrigeqlem1  46079  fourierdlem62  46149  fourierdlem73  46160  fourierdlem76  46163  fourierdlem77  46164  fourierdlem103  46190  fourierdlem104  46191  fourierclim  46205  fourier  46206  fouriersw  46212  etransclem41  46256  etransclem46  46261  salexct2  46320  salexct3  46323  salgencntex  46324  salgensscntex  46325  dmvolsal  46327  bor1sal  46336  iocborel  46337  sge00  46357  sge0sn  46360  ovolval5lem3  46635  ioosshoi  46650  vonioolem2  46662  smfmullem4  46775  upwrdfi  46868  cjnpoly  46873  dfafv2  47116  ichim  47441  grlimedgnedg  48115  nelsubc3  49056  fucofulem2  49296  setc2othin  49451  setcsnterm  49475  setc1obas  49477  setc1ohomfval  49478  setc1ocofval  49479  setc1oid  49480  termc2  49503  setc1onsubc  49587  onsetrec  49693  joinlmuladdmuli  49758