Theorem mptru 1550

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

Syntax hints:   → wi 4  ⊤wtru 1544

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 210  df-tru 1546

This theorem is referenced by:  hadbi123i  1602  cadbi123i  1618  nfan  1907  nfbi  1911  spimefv  2198  spime  2390  nfsb  2528  nfmov  2561  nfmo  2563  nfeuw  2594  nfeu  2595  abeq2i  2875  abbi2i  2879  nfeq  2920  nfel  2921  dvelimc  2935  nfralw  3150  nfral  3151  nfrex  3238  nfrexg  3239  nfreuw  3301  nfrmow  3302  nfreu  3303  nfrmo  3304  nfrabw  3312  nfrab  3313  rabbia2  3402  reuxfr  3680  reuxfr1  3683  nfsbc1  3731  nfsbcw  3734  nfsbc  3737  sbcbii  3773  csbeq2i  3837  nfcsb1  3853  nfcsbw  3856  nfcsb  3857  eqri  3938  vn0  4270  nfif  4486  nfdisjw  5047  nfdisj  5048  nfbr  5117  nfopab  5139  mpteq1i  5165  mpteq2ia  5172  mpteq12i  5175  ralxfr  5331  issoi  5527  nfiotaw  6377  nfiota  6379  nfriota  7222  nfov  7282  mpoeq123i  7326  mpoeq3ia  7328  opco1i  7934  iseri  8460  nfixpw  8639  nfixp  8640  en2i  8710  en3i  8711  ensymb  8720  entr  8724  djulf1o  9576  djurf1o  9577  r0weon  9674  recmulnq  10626  nrex1  10726  nfneg  11122  negiso  11860  suprzcl2  12582  supxr  12951  xrinf0  12976  fac0  13893  cnrecnv  14779  cau3  14970  cbvsum  15310  sum0  15336  ackbijnn  15443  flo1  15469  trireciplem  15477  trirecip  15478  ege2le3  15702  rpnnen2lem3  15828  ruclem4  15846  bitsf1ocnv  16054  prmreclem6  16525  prmrec  16526  modxai  16672  strfvn  16790  strss  16811  xpsvsca  17180  mreacs  17259  2oppccomf  17328  setc2obas  17700  setc2ohom  17701  cat1  17703  mndprop  18301  grpprop  18485  isgrpi  18492  oppgmndb  18852  oppggrpb  18855  odfval  19030  efgrelexlemb  19246  ablprop  19288  ringprop  19713  opprringb  19764  rlmbas  20353  rlmplusg  20354  rlm0  20355  rlmsub  20356  rlmmulr  20357  rlmsca2  20359  rlmvsca  20360  rlmtopn  20361  rlmds  20362  rlmvneg  20366  cncrng  20506  xrsmcmn  20508  cndrng  20514  cnsrng  20519  xrs1mnd  20523  xrs10  20524  absabv  20542  zringcyg  20578  recrng  20713  psrbagsn  21156  evlsval  21181  psr1bas2  21246  psr1bas  21247  psr1plusg  21278  psr1vsca  21279  psr1mulr  21280  ply1plusgfvi  21298  ply1mpl0  21311  ply1mpl1  21313  ordtrestixx  22256  llyidm  22522  nllyidm  22523  toplly  22524  hauslly  22526  hausnlly  22527  lly1stc  22530  kgenf  22575  txswaphmeolem  22838  fmucndlem  23326  nrgtrg  23735  cnfldnm  23823  xrsxmet  23853  divcn  23912  expcn  23916  elcncf1ii  23940  iirevcn  23974  iihalf1cn  23976  iihalf2cn  23978  iimulcn  23982  icopnfcnv  23986  iccpnfcnv  23988  cnrehmeo  23997  tcphsub  24265  tcphphl  24271  iscmet3i  24356  cncmet  24366  rrxprds  24433  vitali  24657  i1f0  24731  itg20  24782  dvid  24962  dveflem  25023  dvef  25024  dvsincos  25025  ply1divalg2  25183  coe0  25297  iaa  25365  sincn  25483  coscn  25484  reefgim  25489  pilem3  25492  resinf1o  25572  circgrp  25588  circsubm  25589  divlogrlim  25670  dvrelog  25672  logcn  25682  dvlog  25686  advlog  25689  cxpcn  25778  cxpcn2  25779  resqrtcn  25782  sqrtcn  25783  atansopn  25962  dvatan  25965  leibpilem2  25971  leibpi  25972  leibpisum  25973  log2cnv  25974  log2ublem2  25977  log2ub  25979  divsqrtsumlem  26009  emcllem4  26028  emcllem6  26030  emcllem7  26031  lgamf  26071  lgam1  26093  basellem6  26115  basellem7  26116  basellem8  26117  basellem9  26118  vmaf  26148  logfacrlim  26252  lgsdir2lem5  26357  chebbnd1  26500  chtppilim  26503  chto1ub  26504  chebbnd2  26505  chto1lb  26506  chpchtlim  26507  chpo1ub  26508  chpo1ubb  26509  vmadivsum  26510  vmadivsumb  26511  mudivsum  26558  mulogsumlem  26559  mulogsum  26560  logdivsum  26561  vmalogdivsum2  26566  vmalogdivsum  26567  selberglem1  26573  selberglem2  26574  selbergb  26577  selberg2lem  26578  selberg2  26579  selberg2b  26580  selberg3lem2  26586  selberg3  26587  selberg4  26589  pntrmax  26592  pntrsumo1  26593  pntrsumbnd  26594  selbergr  26596  selberg3r  26597  selberg4r  26598  selberg34r  26599  pntrlog2bndlem1  26605  pntrlog2bndlem4  26608  pnt2  26641  pnt  26642  istrkg2ld  26700  legval  26824  ttgsub  27122  cchhllem  27132  cchhllemOLD  27133  trlsfval  27940  pthsfval  27965  spthsfval  27966  clwlks  28016  crcts  28032  cycls  28033  2wspdisj  28203  2wspiundisj  28204  eupths  28440  konigsbergiedgw  28488  ipasslem7  29074  normlem6  29353  opsqrlem4  30381  fpwrelmap  30945  fpwrelmapffs  30946  xrs0  31161  ccfldsrarelvec  31618  ccfldextdgrr  31619  mdetlap1  31653  circtopn  31664  cnre2csqima  31738  cnvordtrestixx  31740  mndpluscn  31753  xrge0iifcnv  31760  zlm0  31787  zlm1  31788  qqhre  31845  rrhre  31846  esumnul  31891  hasheuni  31928  sxbrsigalem2  32128  oddpwdc  32196  eulerpartlemb  32210  eulerpartgbij  32214  eulerpartlemn  32223  fib0  32241  fib1  32242  ballotlemrinv  32375  sgn3da  32383  signsw0g  32410  circlemethnat  32496  subfacval2  33024  sinccvglem  33505  circum  33507  logi  33581  faclim  33593  faclim2  33595  nfttrcl  33672  xpord2ind  33696  xpord3ind  33702  on2recsfn  33728  on2recsov  33729  dmscut  33907  lrrecpo  34000  noxpordpo  34009  noxpordfr  34010  noxpordse  34011  cnndvlem1  34619  bj-dvelimv  34939  bj-inrab2  35018  bj-rabtrAUTO  35022  dfwrecs2  35144  bj-opelidb  35226  bj-iomnnom  35333  sucneqoni  35443  wl-df-3xor  35545  wl-3xorbi123i  35553  wl-df3maxtru1  35569  wl-cbvalnae  35598  wl-equsal  35605  poimirlem30  35713  dvtan  35733  dvasin  35767  dvacos  35768  dvreasin  35769  dvreacos  35770  efald2  36142  lcmineqlem7  39950  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  aks4d1p1p6  39987  re1m1e0m0  40273  re0m0e0  40278  reixi  40297  subresre  40305  3cubeslem4  40399  3cubes  40400  areaquad  40935  clsk1indlem4  41516  clsk1indlem1  41517  ismnushort  41781  lhe4.4ex1a  41809  sbtT  42049  eel0TT  42186  eelTTT  42188  eelT1  42190  eelTT  42253  eelT  42255  eelT0  42257  isosctrlem1ALT  42416  disjsnxp  42480  infxr  42769  nfxneg  42864  limsup0  43098  0cnv  43146  limsup10ex  43177  liminf10ex  43178  liminfvalxr  43187  liminf0  43197  dvsinax  43317  itgsin0pilem1  43354  iblempty  43369  stowei  43468  wallispilem5  43473  wallispi  43474  stirlinglem1  43478  stirlinglem12  43489  stirlinglem13  43490  stirlinglem14  43491  stirlingr  43494  dirkertrigeqlem1  43502  fourierdlem62  43572  fourierdlem73  43583  fourierdlem76  43586  fourierdlem77  43587  fourierdlem103  43613  fourierdlem104  43614  fourierclim  43628  fourier  43629  fouriersw  43635  etransclem41  43679  etransclem46  43684  salexct2  43741  salexct3  43744  salgencntex  43745  salgensscntex  43746  dmvolsal  43748  bor1sal  43757  iocborel  43758  sge00  43777  sge0sn  43780  ovolval5lem3  44055  ioosshoi  44070  vonioolem2  44082  smfmullem4  44188  dfafv2  44484  ichim  44770  setc2othin  46198  onsetrec  46272  joinlmuladdmuli  46336