MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbi Unicode version

Theorem mpbi 199
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbi.min  |-  ph
mpbi.maj  |-  ( ph  <->  ps )
Assertion
Ref Expression
mpbi  |-  ps

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2  |-  ph
2 mpbi.maj . . 3  |-  ( ph  <->  ps )
32biimpi 186 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  pm5.74i  236  notbii  287  pm5.19  349  ori  364  imori  402  pm4.71i  613  pm4.71ri  614  pm5.32i  618  pm3.24  852  pm5.16  860  biluk  899  4exmid  905  dn1  932  3ori  1242  trubifal  1341  nic-dfim  1424  nic-dfneg  1425  nic-mp  1426  nic-mpALT  1427  tbw-negdf  1454  rb-imdf  1505  mpto2  1524  mtp-xor  1525  mpgbi  1536  19.35i  1588  19.36i  1808  19.37aiv  1841  sbco  2023  sbidm  2025  eqcomi  2287  eqtri  2303  eleqtri  2355  neeqtri  2467  necomi  2528  nemtbir  2534  nrex  2645  rexlimi  2660  isseti  2794  vtocl2  2839  vtocl3  2840  eueq1  2938  euxfr2  2950  cdeqri  2977  sseqtri  3210  3sstr3i  3216  pssn2lp  3277  equncomi  3321  unssi  3350  ssini  3392  unabs  3399  inabs  3400  dfin4  3409  npss0  3493  difid  3522  disjdif  3526  difin0  3527  snid  3667  snsssn  3781  iinrab2  3965  rintn0  3992  breqtri  4046  axsep  4140  bm1.3ii  4144  ax9vsep  4145  zfnuleu  4146  notzfaus  4185  zfpow  4189  dtru  4201  dtruALT  4207  dtruALT2  4219  copsexg  4252  uniop  4269  pwundif  4300  onunisuci  4506  zfun  4513  reusv2lem4  4538  reuxfr2d  4557  op1stb  4569  tfinds2  4654  omon  4667  relop  4834  rn0  4936  dmresi  5005  issref  5056  somincom  5080  cnvcnv  5126  rescnvcnv  5135  cnvcnvres  5136  cnvsn  5155  cocnvcnv2  5184  cores2  5185  co01  5187  relcoi1  5201  cnviin  5212  iota4an  5238  fnopab  5368  mpt0  5371  fnmpti  5372  f1cnvcnv  5445  f1ovi  5512  fvco4i  5597  fmpti  5683  fvsnun2  5716  funiunfv  5774  oprabss  5933  relmptopab  6065  2nd0  6127  f1stres  6141  f2ndres  6142  relmpt2opab  6201  df1st2  6205  df2nd2  6206  fsplit  6223  reldmtpos  6242  dftpos4  6253  tpostpos  6254  tpos0  6264  smo0  6375  tfrlem14  6407  tfrlem16  6409  rdgsucg  6436  rdglimg  6438  frfnom  6447  oawordeulem  6552  uniixp  6839  dfdom2  6887  ssdomg  6907  2dom  6933  xpcomf1o  6951  sbthlem5  6975  pwdom  7013  map2xp  7031  limensuci  7037  fiint  7133  fidomdm  7138  pwfilem  7150  mptfi  7155  fisn  7180  dffi3  7184  ordtypelem6  7238  ordtypelem7  7239  wemaplem2  7262  wdompwdom  7292  harwdom  7304  suc11reg  7320  zfinf  7340  axinf2  7341  noinfep  7360  cantnfvalf  7366  cantnflt  7373  cantnf0  7376  cantnf  7395  tz9.1c  7412  tc2  7427  r111  7447  r1tr2  7449  r1ordg  7450  r1sssuc  7455  r1val1  7458  tz9.13  7463  r1elssi  7477  pwwf  7479  rankopb  7524  rankeq0b  7532  ranksuc  7537  rankxplim  7549  rankxplim3  7551  rankxpsuc  7552  cp  7561  karden  7565  card0  7591  cardlim  7605  cardom  7619  pm54.43lem  7632  infxpenlem  7641  alephsuc2  7707  alephgeom  7709  alephprc  7726  unialeph  7728  dfac4  7749  dfacacn  7767  cda1dif  7802  pm110.643  7803  infcda1  7819  ackbij1lem13  7858  ackbij2  7869  cf0  7877  cfsuc  7883  cfom  7890  cfslb2n  7894  ominf4  7938  fin23lem17  7964  fin23lem28  7966  fin23lem30  7968  fin23lem31  7969  fin23lem40  7977  isfin1-3  8012  dfacfin7  8025  fin1a2lem6  8031  itunitc1  8046  axcc3  8064  dcomex  8073  axdc2lem  8074  axcclem  8083  zfac  8086  ac3  8088  ackm  8092  axac2  8093  axac  8094  axaci  8095  cardeqv  8096  numth2  8098  numth  8099  brdom3  8153  fin71ac  8158  cardf  8172  aleph1  8193  cfpwsdom  8206  smobeth  8208  zfcndrep  8236  zfcndpow  8238  zfcndac  8241  canthp1lem2  8275  gch2  8301  wunex3  8363  tskpr  8392  inar1  8397  rankcf  8399  tskcard  8403  tskuni  8405  grothpw  8448  axgroth4  8454  grothprim  8456  inaprc  8458  dmaddpi  8514  dmmulpi  8515  1lt2pi  8529  addpqf  8568  mulpqf  8570  1lt2nq  8597  supsrlem  8733  renepnf  8879  renemnf  8880  ssxr  8892  ltxrlt  8893  subf  9053  negne0i  9121  negdii  9130  ine0  9215  mulnzcnopr  9414  recgt0ii  9662  lbinfm  9707  infmsup  9732  infmrgelb  9734  infmrlb  9735  inelr  9736  halflt1  9933  nn0ssz  10044  zeo  10097  numlt  10143  numltc  10144  uzf  10233  uzinfmi  10297  xrltnr  10462  pnfnlt  10467  nltmnf  10468  xaddf  10551  xsubge0  10581  xmulf  10592  infmxrcl  10635  infmxrlb  10652  infmxrgelb  10653  xrinfm0  10655  ixxf  10666  ixxssxr  10668  iooval2  10689  ioof  10741  unirnioo  10743  dfioo2  10744  fzval2  10785  fzf  10786  fz10  10814  fzof  10872  fzo0  10893  om2uzoi  11018  faclbnd4lem1  11306  hashkf  11339  hashgval  11340  hashinf  11342  hashclb  11352  hasheq0  11353  hashbclem  11390  wrdexg  11425  rev0  11482  sqr2gt1lt2  11760  limsupgord  11946  limsupval  11948  fclim  12027  fsumrelem  12265  ackbijnn  12286  incexclem  12295  incexc  12296  arisum2  12319  georeclim  12328  geoisumr  12334  0.999...  12337  geoihalfsum  12338  ege2le3  12371  sin0  12429  ef01bndlem  12464  cos2bnd  12468  cos01gt0  12471  sincos2sgn  12474  sin4lt0  12475  egt2lt3  12484  rpnnen2lem3  12495  rpnnen2lem9  12501  rexpen  12506  cnso  12525  nthruc  12529  dvdslelem  12573  divalglem1  12593  divalglem5  12596  divalglem6  12597  divalglem10  12601  bitsfzolem  12625  bitsfzo  12626  0bits  12630  bitsinv1lem  12632  sadcf  12644  sadcadd  12649  bitsshft  12666  smupf  12669  gcdf  12698  eucalgf  12753  isprm3  12767  2prm  12774  dfphi2  12842  odzval  12856  pcgcd1  12929  pc2dvds  12931  pockthi  12954  prmreclem2  12964  prmrec  12969  vdwapf  13019  vdwap0  13023  vdwlem6  13033  ramval  13055  ramcl2lem  13056  ramtcl2  13058  karatsuba  13099  1259lem5  13133  2503lem3  13137  4001lem4  13142  structcnvcnv  13159  structfn  13161  strlemor1  13235  strleun  13238  prdsval  13355  prdsds  13363  imasdsfn  13417  imasdsval  13418  imasvscafn  13439  xpsc0  13462  xpsc1  13463  xpsfrnel2  13467  xpsff1o  13470  sscpwex  13692  wunfunc  13773  wunnat  13830  eldmcoa  13897  coapm  13903  setcepi  13920  catcfuccl  13941  catcxpccl  13981  yonedainv  14055  plusffval  14379  grpinvfvi  14523  mulgfvi  14571  odval  14849  odf  14852  odhash3  14887  gexval  14889  sylow3lem2  14939  oppglsm  14953  efgmf  15022  efgval  15026  efgsf  15038  0frgp  15088  gsumzaddlem  15203  dmdprd  15236  dprdval  15238  invrfval  15455  drngui  15518  scaffval  15645  lssintcl  15721  mplsubrglem  16183  opsrtoslem2  16226  cnfld0  16398  cnfld1  16399  cnfldsub  16402  xrsds  16414  xrsdsreclblem  16417  ipffval  16552  ocv1  16579  eltpsi  16684  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  leordtvallem1  16940  leordtvallem2  16941  iccordt  16944  pnfnei  16950  mnfnei  16951  iscnp2  16969  discmp  17125  concompcld  17160  1stcrestlem  17178  2ndcdisj  17182  topnlly  17217  disllycmp  17224  dis1stc  17225  txuni2  17260  xkotf  17280  dfac14lem  17311  prdstps  17323  txindis  17328  tx1stc  17344  xkohaus  17347  xkoptsub  17348  cnmpt1st  17362  cnmpt2nd  17363  ptcmpfi  17504  filcon  17578  trfil1  17581  fin1aufil  17627  tgpconcompeqg  17794  tgpconcomp  17795  tsmsres  17826  met1stc  18067  dscmet  18095  nmoval  18224  retopon  18272  cnfldtopon  18292  xrsxmet  18315  xrsmopn  18318  metdsval  18351  iimulcn  18436  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  xrhmph  18445  cnheiborlem  18452  lebnumii  18464  ishtpy  18470  htpycc  18478  pco1  18513  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  cfilresi  18721  ovolval  18833  ovolf  18841  ovoliunlem3  18863  ovolicc1  18875  ovolicc2  18881  volf  18888  ioorf  18928  dyadf  18946  dyadmbl  18955  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfimaopnlem  19010  mbflimsup  19021  0plef  19027  i1fima  19033  i1fima2  19034  i1fd  19036  i1f0rn  19037  itg1ge0  19041  itg10  19043  i1f1lem  19044  i1fadd  19050  i1fmul  19051  i1fmulc  19058  mbfi1fseqlem5  19074  itg2addlem  19113  reldv  19220  dvbsss  19252  dvef  19327  dvlt0  19352  lhop1lem  19360  deg1fvi  19471  deg1nn0clb  19476  plypf1  19594  coeeulem  19606  coeeu  19607  vieta1lem2  19691  elqaalem1  19699  elqaalem3  19701  aannenlem3  19710  aalioulem2  19713  aalioulem3  19714  dvradcnv  19797  pserulm  19798  pserdvlem2  19804  abelthlem6  19812  sinhalfpilem  19834  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  pige3  19885  coseq1  19890  resinf1o  19898  tanord1  19899  tanregt0  19901  relogrn  19919  dfrelog  19923  logneg  19941  logltb  19953  logcn  19994  logf1o2  19997  dvlog  19998  efopnlem2  20004  efopn  20005  logccv  20010  dvsqr  20084  cxpcn3  20088  angpined  20127  1cubr  20138  atanre  20181  asinsin  20188  asin1  20190  reasinsin  20192  atan0  20204  atanbnd  20222  atan1  20224  log2cnv  20240  log2ublem3  20244  log2ub  20245  birthday  20249  amgmlem  20284  emcllem5  20293  emgt0  20300  harmonicbnd3  20301  ftalem3  20312  basellem4  20321  sgmf  20383  ppi1  20402  cht1  20403  vma1  20404  ppiltx  20415  sqff1o  20420  ppiublem1  20441  ppiublem2  20442  ppiub  20443  chtub  20451  dchreq  20497  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgsdir2lem2  20563  lgsdir2lem3  20564  chebbnd1  20621  chto1ub  20625  chpo1ubb  20630  pntibndlem1  20738  ex-dif  20810  ex-un  20811  ex-in  20812  ex-fl  20834  avril1  20836  ginvsn  21016  cnid  21018  mulid  21023  rngosn3  21093  vcoprnelem  21134  vcoprne  21135  vcex  21136  cnnvm  21251  ipasslem8  21415  ipasslem10  21417  hvsubf  21595  normlem1  21689  normlem6  21694  normlem7  21695  norm-ii-i  21716  norm3adifii  21727  hilid  21740  hlimf  21817  norm1exi  21829  hhssabloi  21839  hhssnv  21841  hhshsslem1  21844  shincli  21941  shsval2i  21966  shs0i  22028  chj0i  22034  chm1i  22035  chincli  22039  chdmm1i  22056  shjshsi  22071  chsup0  22127  h1de2bi  22133  spansnpji  22157  cmcmlem  22170  cmcmii  22176  cmcm2ii  22177  cmcm3ii  22178  pjidmi  22252  pjssmii  22260  pj0i  22272  pjocini  22277  mayetes3i  22309  df0op2  22332  hoaddcomi  22352  hoaddassi  22356  hocadddiri  22359  hocsubdiri  22360  hoaddid1i  22366  ho0coi  22368  hoid1i  22369  hoid1ri  22370  hodseqi  22374  honegsubi  22376  adj1o  22474  hoddii  22569  lnopunilem1  22590  lnopunilem2  22591  nmcopexi  22607  nmcopex  22609  nmcoplb  22610  nmcfnexi  22631  nmcfnex  22633  nmcfnlb  22634  adjbd1o  22665  adjcoi  22680  nmopcoadji  22681  opsqrlem6  22725  pjsdii  22735  pjddii  22736  pjidmcoi  22757  pjtoi  22759  pjin1i  22772  pjclem1  22775  stji1i  22822  largei  22847  rinvf1o  23038  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlem4  23057  ballotlem5  23058  ballotlemi  23059  ballotlemiex  23060  ballotlemi1  23061  ballotlemii  23062  ballotlemsup  23063  ballotlemimin  23064  ballotlem1c  23066  ballotlemfrcn0  23088  ballotlemirc  23090  ballotlem7  23094  ballotth  23096  or3dir  23124  reuxfr3d  23138  iuninc  23158  hashresfn  23173  pwundif2  23186  difprsn2  23191  suppss2f  23201  xppreima  23211  ofoprabco  23232  funcnvmptOLD  23234  funcnvmpt  23235  gtiso  23241  df1stres  23243  df2ndres  23244  xrofsup  23255  clduni  23289  sqsscirc1  23292  ressplusf  23298  mhmhmeotmd  23300  rmulccn  23301  raddcn  23302  xrge0base  23310  xrge00  23311  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhmeo  23318  xrge0neqmnf  23330  snct  23339  dmct  23342  disjrdx  23370  lmxrge0  23375  rnlogblem  23401  log2le1  23409  esumnul  23427  esum0  23428  esumsn  23437  esumpfinvallem  23442  esumpfinvalf  23444  esumpcvgval  23446  esumcvg  23454  sigaex  23470  sigaclfu2  23482  dmsigagen  23505  measvuni  23542  measiuns  23544  imambfm  23567  mbfmvolf  23571  br2base  23574  itgmcntTMP  23588  ind1a  23604  probdif  23623  totprobd  23629  0rrv  23654  coinfliplem  23679  coinflipprob  23680  coinfliprv  23683  subfacf  23706  subfacp1lem1  23710  subfacp1lem5  23715  subfacp1lem6  23716  subfacval3  23720  erdszelem2  23723  erdszelem9  23730  erdszelem11  23732  kur14lem4  23740  iooscon  23778  iccllyscon  23781  umgrafi  23874  konigsberg  23911  ghomgrpilem1  23992  ghomgrpilem2  23993  circum  24007  axextprim  24047  axrepprim  24048  axunprim  24049  axinfprim  24052  axacprim  24053  inffz  24095  fz0n  24097  setinds  24134  dfon2lem2  24140  dfon2lem4  24142  dfrdg2  24152  axextdfeq  24154  poseq  24253  wfrlem4  24259  frrlem4  24284  sltval2  24310  nosgnn0  24312  sltintdifex  24317  sltres  24318  sltsolem1  24322  bdayfo  24329  symdifV  24369  fobigcup  24440  snelsingles  24461  fullfunfnv  24484  fullfunfv  24485  dfrdg4  24488  rankaltopb  24513  axlowdimlem4  24573  axlowdimlem13  24582  axlowdimlem16  24585  axlowdim1  24587  axlowdim  24589  linedegen  24766  bpoly0  24785  rank0  24800  rankeq1o  24801  hfuni  24814  nabi1i  24830  nabi2i  24831  limsucncmpi  24884  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  ump  25046  vxveqv  25054  prj1b  25079  prj3  25080  domncnt  25282  ranncnt  25283  toplat  25290  rrisgrp  25338  hmeogrpi  25536  intopcoaconlem3  25539  altretop  25600  phckle  26027  psckle  26028  smbkle  26043  pgapspf  26052  gtinf  26234  fneer  26288  neibastop1  26308  opelopab3  26373  fdc  26455  cntotbnd  26520  heiborlem6  26540  rrnval  26551  reheibor  26563  prter2  26749  diophrw  26838  0dioph  26858  rabren3dioph  26898  rencldnfilem  26903  pellexlem6  26919  pellex  26920  pellfundval  26965  frmx  26998  frmy  26999  jm2.23  27089  jm2.27dlem3  27104  axac10  27126  pw2f1ocnv  27130  wepwsolem  27138  kelac2lem  27162  lmhmlnmsplit  27185  dsmmbas2  27203  pwfi2f1o  27260  frlmpwfi  27262  dgraaval  27349  dgraaf  27352  symgsssg  27408  symgfisg  27409  psgnunilem5  27417  psgnghm  27437  seff  27538  expgrowthi  27550  expgrowth  27552  refsum2cnlem1  27708  infrglb  27722  clim1fr1  27727  dvcosre  27741  stoweidlem1  27750  stoweidlem7  27756  stoweidlem26  27775  stoweidlem34  27783  stoweidlem44  27793  stoweid  27812  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  stirlinglem5  27827  stirlinglem6  27828  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839  f1oun2prg  28076  usgraedgprv  28122  usgraexmpl  28133  ee233  28281  a9e2nd  28324  in1  28339  dfvd2ani  28352  dfvd2i  28354  dfvd3i  28361  dfvd3ani  28364  e0bi  28551  uun2221  28588  uun2221p1  28589  uun2221p2  28590  en3lpVD  28621  relopabVD  28677  a9e2ndVD  28684  a9e2ndALT  28707  bnj521  28765  bnj1098  28815  bnj1109  28818  bnj1131  28819  bnj1533  28884  bnj151  28909  bnj580  28945  bnj852  28953  bnj864  28954  bnj865  28955  bnj978  28981  bnj1021  28996  bnj907  28997  bnj1093  29010  bnj1145  29023  bnj1172  29031  bnj1174  29033  bnj1176  29035  bnj1186  29037  ax12conj2  29108  cdleme0moN  30414  mapdunirnN  31840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator