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  mpto2OLD  1525  mtp-xorOLD  1527  mpgbi  1539  19.35i  1591  19.36i  1820  19.37aiv  1853  sbco  2036  sbidm  2038  eqcomi  2300  eqtri  2316  eleqtri  2368  neeqtri  2480  necomi  2541  nemtbir  2547  nrex  2658  rexlimi  2673  isseti  2807  vtocl2  2852  vtocl3  2853  eueq1  2951  euxfr2  2963  cdeqri  2990  sseqtri  3223  3sstr3i  3229  pssn2lp  3290  equncomi  3334  unssi  3363  ssini  3405  unabs  3412  inabs  3413  dfin4  3422  npss0  3506  difid  3535  disjdif  3539  difin0  3540  snid  3680  snsssn  3797  iinrab2  3981  rintn0  4008  breqtri  4062  axsep  4156  bm1.3ii  4160  ax9vsep  4161  zfnuleu  4162  notzfaus  4201  zfpow  4205  dtru  4217  dtruALT  4223  dtruALT2  4235  copsexg  4268  uniop  4285  pwundif  4316  onunisuci  4522  zfun  4529  reusv2lem4  4554  reuxfr2d  4573  op1stb  4585  tfinds2  4670  omon  4683  relop  4850  rn0  4952  dmresi  5021  issref  5072  somincom  5096  cnvcnv  5142  rescnvcnv  5151  cnvcnvres  5152  cnvsn  5171  cocnvcnv2  5200  cores2  5201  co01  5203  relcoi1  5217  cnviin  5228  iota4an  5254  fnopab  5384  mpt0  5387  fnmpti  5388  f1cnvcnv  5461  f1ovi  5528  fvco4i  5613  fmpti  5699  fvsnun2  5732  funiunfv  5790  oprabss  5949  relmptopab  6081  2nd0  6143  f1stres  6157  f2ndres  6158  relmpt2opab  6217  df1st2  6221  df2nd2  6222  fsplit  6239  reldmtpos  6258  dftpos4  6269  tpostpos  6270  tpos0  6280  smo0  6391  tfrlem14  6423  tfrlem16  6425  rdgsucg  6452  rdglimg  6454  frfnom  6463  oawordeulem  6568  uniixp  6855  dfdom2  6903  ssdomg  6923  2dom  6949  xpcomf1o  6967  sbthlem5  6991  pwdom  7029  map2xp  7047  limensuci  7053  fiint  7149  fidomdm  7154  pwfilem  7166  mptfi  7171  fisn  7196  dffi3  7200  ordtypelem6  7254  ordtypelem7  7255  wemaplem2  7278  wdompwdom  7308  harwdom  7320  suc11reg  7336  zfinf  7356  axinf2  7357  noinfep  7376  cantnfvalf  7382  cantnflt  7389  cantnf0  7392  cantnf  7411  tz9.1c  7428  tc2  7443  r111  7463  r1tr2  7465  r1ordg  7466  r1sssuc  7471  r1val1  7474  tz9.13  7479  r1elssi  7493  pwwf  7495  rankopb  7540  rankeq0b  7548  ranksuc  7553  rankxplim  7565  rankxplim3  7567  rankxpsuc  7568  cp  7577  karden  7581  card0  7607  cardlim  7621  cardom  7635  pm54.43lem  7648  infxpenlem  7657  alephsuc2  7723  alephgeom  7725  alephprc  7742  unialeph  7744  dfac4  7765  dfacacn  7783  cda1dif  7818  pm110.643  7819  infcda1  7835  ackbij1lem13  7874  ackbij2  7885  cf0  7893  cfsuc  7899  cfom  7906  cfslb2n  7910  ominf4  7954  fin23lem17  7980  fin23lem28  7982  fin23lem30  7984  fin23lem31  7985  fin23lem40  7993  isfin1-3  8028  dfacfin7  8041  fin1a2lem6  8047  itunitc1  8062  axcc3  8080  dcomex  8089  axdc2lem  8090  axcclem  8099  zfac  8102  ac3  8104  ackm  8108  axac2  8109  axac  8110  axaci  8111  cardeqv  8112  numth2  8114  numth  8115  brdom3  8169  fin71ac  8174  cardf  8188  aleph1  8209  cfpwsdom  8222  smobeth  8224  zfcndrep  8252  zfcndpow  8254  zfcndac  8257  canthp1lem2  8291  gch2  8317  wunex3  8379  tskpr  8408  inar1  8413  rankcf  8415  tskcard  8419  tskuni  8421  grothpw  8464  axgroth4  8470  grothprim  8472  inaprc  8474  dmaddpi  8530  dmmulpi  8531  1lt2pi  8545  addpqf  8584  mulpqf  8586  1lt2nq  8613  supsrlem  8749  renepnf  8895  renemnf  8896  ssxr  8908  ltxrlt  8909  subf  9069  negne0i  9137  negdii  9146  ine0  9231  mulnzcnopr  9430  recgt0ii  9678  lbinfm  9723  infmsup  9748  infmrgelb  9750  infmrlb  9751  inelr  9752  halflt1  9949  nn0ssz  10060  zeo  10113  numlt  10159  numltc  10160  uzf  10249  uzinfmi  10313  xrltnr  10478  pnfnlt  10483  nltmnf  10484  xaddf  10567  xsubge0  10597  xmulf  10608  infmxrcl  10651  infmxrlb  10668  infmxrgelb  10669  xrinfm0  10671  ixxf  10682  ixxssxr  10684  iooval2  10705  ioof  10757  unirnioo  10759  dfioo2  10760  fzval2  10801  fzf  10802  fz10  10830  fzof  10888  fzo0  10909  om2uzoi  11034  faclbnd4lem1  11322  hashkf  11355  hashgval  11356  hashinf  11358  hashclb  11368  hasheq0  11369  hashbclem  11406  wrdexg  11441  rev0  11498  sqr2gt1lt2  11776  limsupgord  11962  limsupval  11964  fclim  12043  fsumrelem  12281  ackbijnn  12302  incexclem  12311  incexc  12312  arisum2  12335  georeclim  12344  geoisumr  12350  0.999...  12353  geoihalfsum  12354  ege2le3  12387  sin0  12445  ef01bndlem  12480  cos2bnd  12484  cos01gt0  12487  sincos2sgn  12490  sin4lt0  12491  egt2lt3  12500  rpnnen2lem3  12511  rpnnen2lem9  12517  rexpen  12522  cnso  12541  nthruc  12545  dvdslelem  12589  divalglem1  12609  divalglem5  12612  divalglem6  12613  divalglem10  12617  bitsfzolem  12641  bitsfzo  12642  0bits  12646  bitsinv1lem  12648  sadcf  12660  sadcadd  12665  bitsshft  12682  smupf  12685  gcdf  12714  eucalgf  12769  isprm3  12783  2prm  12790  dfphi2  12858  odzval  12872  pcgcd1  12945  pc2dvds  12947  pockthi  12970  prmreclem2  12980  prmrec  12985  vdwapf  13035  vdwap0  13039  vdwlem6  13049  ramval  13071  ramcl2lem  13072  ramtcl2  13074  karatsuba  13115  1259lem5  13149  2503lem3  13153  4001lem4  13158  structcnvcnv  13175  structfn  13177  strlemor1  13251  strleun  13254  prdsval  13371  prdsds  13379  imasdsfn  13433  imasdsval  13434  imasvscafn  13455  xpsc0  13478  xpsc1  13479  xpsfrnel2  13483  xpsff1o  13486  sscpwex  13708  wunfunc  13789  wunnat  13846  eldmcoa  13913  coapm  13919  setcepi  13936  catcfuccl  13957  catcxpccl  13997  yonedainv  14071  plusffval  14395  grpinvfvi  14539  mulgfvi  14587  odval  14865  odf  14868  odhash3  14903  gexval  14905  sylow3lem2  14955  oppglsm  14969  efgmf  15038  efgval  15042  efgsf  15054  0frgp  15104  gsumzaddlem  15219  dmdprd  15252  dprdval  15254  invrfval  15471  drngui  15534  scaffval  15661  lssintcl  15737  mplsubrglem  16199  opsrtoslem2  16242  cnfld0  16414  cnfld1  16415  cnfldsub  16418  xrsds  16430  xrsdsreclblem  16433  ipffval  16568  ocv1  16595  eltpsi  16700  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  leordtvallem1  16956  leordtvallem2  16957  iccordt  16960  pnfnei  16966  mnfnei  16967  iscnp2  16985  discmp  17141  concompcld  17176  1stcrestlem  17194  2ndcdisj  17198  topnlly  17233  disllycmp  17240  dis1stc  17241  txuni2  17276  xkotf  17296  dfac14lem  17327  prdstps  17339  txindis  17344  tx1stc  17360  xkohaus  17363  xkoptsub  17364  cnmpt1st  17378  cnmpt2nd  17379  ptcmpfi  17520  filcon  17594  trfil1  17597  fin1aufil  17643  tgpconcompeqg  17810  tgpconcomp  17811  tsmsres  17842  met1stc  18083  dscmet  18111  nmoval  18240  retopon  18288  cnfldtopon  18308  xrsxmet  18331  xrsmopn  18334  metdsval  18367  iimulcn  18452  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  xrhmph  18461  cnheiborlem  18468  lebnumii  18480  ishtpy  18486  htpycc  18494  pco1  18529  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  cfilresi  18737  ovolval  18849  ovolf  18857  ovoliunlem3  18879  ovolicc1  18891  ovolicc2  18897  volf  18904  ioorf  18944  dyadf  18962  dyadmbl  18971  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfimaopnlem  19026  mbflimsup  19037  0plef  19043  i1fima  19049  i1fima2  19050  i1fd  19052  i1f0rn  19053  itg1ge0  19057  itg10  19059  i1f1lem  19060  i1fadd  19066  i1fmul  19067  i1fmulc  19074  mbfi1fseqlem5  19090  itg2addlem  19129  reldv  19236  dvbsss  19268  dvef  19343  dvlt0  19368  lhop1lem  19376  deg1fvi  19487  deg1nn0clb  19492  plypf1  19610  coeeulem  19622  coeeu  19623  vieta1lem2  19707  elqaalem1  19715  elqaalem3  19717  aannenlem3  19726  aalioulem2  19729  aalioulem3  19730  dvradcnv  19813  pserulm  19814  pserdvlem2  19820  abelthlem6  19828  sinhalfpilem  19850  sincos4thpi  19897  tan4thpi  19898  sincos6thpi  19899  pige3  19901  coseq1  19906  resinf1o  19914  tanord1  19915  tanregt0  19917  relogrn  19935  dfrelog  19939  logneg  19957  logltb  19969  logcn  20010  logf1o2  20013  dvlog  20014  efopnlem2  20020  efopn  20021  logccv  20026  dvsqr  20100  cxpcn3  20104  angpined  20143  1cubr  20154  atanre  20197  asinsin  20204  asin1  20206  reasinsin  20208  atan0  20220  atanbnd  20238  atan1  20240  log2cnv  20256  log2ublem3  20260  log2ub  20261  birthday  20265  amgmlem  20300  emcllem5  20309  emgt0  20316  harmonicbnd3  20317  ftalem3  20328  basellem4  20337  sgmf  20399  ppi1  20418  cht1  20419  vma1  20420  ppiltx  20431  sqff1o  20436  ppiublem1  20457  ppiublem2  20458  ppiub  20459  chtub  20467  dchreq  20513  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgsdir2lem2  20579  lgsdir2lem3  20580  chebbnd1  20637  chto1ub  20641  chpo1ubb  20646  pntibndlem1  20754  ex-dif  20826  ex-un  20827  ex-in  20828  ex-fl  20850  avril1  20852  ginvsn  21032  cnid  21034  mulid  21039  rngosn3  21109  vcoprnelem  21150  vcoprne  21151  vcex  21152  cnnvm  21267  ipasslem8  21431  ipasslem10  21433  hvsubf  21611  normlem1  21705  normlem6  21710  normlem7  21711  norm-ii-i  21732  norm3adifii  21743  hilid  21756  hlimf  21833  norm1exi  21845  hhssabloi  21855  hhssnv  21857  hhshsslem1  21860  shincli  21957  shsval2i  21982  shs0i  22044  chj0i  22050  chm1i  22051  chincli  22055  chdmm1i  22072  shjshsi  22087  chsup0  22143  h1de2bi  22149  spansnpji  22173  cmcmlem  22186  cmcmii  22192  cmcm2ii  22193  cmcm3ii  22194  pjidmi  22268  pjssmii  22276  pj0i  22288  pjocini  22293  mayetes3i  22325  df0op2  22348  hoaddcomi  22368  hoaddassi  22372  hocadddiri  22375  hocsubdiri  22376  hoaddid1i  22382  ho0coi  22384  hoid1i  22385  hoid1ri  22386  hodseqi  22390  honegsubi  22392  adj1o  22490  hoddii  22585  lnopunilem1  22606  lnopunilem2  22607  nmcopexi  22623  nmcopex  22625  nmcoplb  22626  nmcfnexi  22647  nmcfnex  22649  nmcfnlb  22650  adjbd1o  22681  adjcoi  22696  nmopcoadji  22697  opsqrlem6  22741  pjsdii  22751  pjddii  22752  pjidmcoi  22773  pjtoi  22775  pjin1i  22788  pjclem1  22791  stji1i  22838  largei  22863  rinvf1o  23054  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlem4  23073  ballotlem5  23074  ballotlemi  23075  ballotlemiex  23076  ballotlemi1  23077  ballotlemii  23078  ballotlemsup  23079  ballotlemimin  23080  ballotlem1c  23082  ballotlemfrcn0  23104  ballotlemirc  23106  ballotlem7  23110  ballotth  23112  or3dir  23140  reuxfr3d  23154  iuninc  23174  hashresfn  23189  pwundif2  23202  suppss2f  23216  xppreima  23226  ofoprabco  23247  funcnvmptOLD  23249  funcnvmpt  23250  gtiso  23256  df1stres  23258  df2ndres  23259  xrofsup  23270  clduni  23304  sqsscirc1  23307  ressplusf  23313  mhmhmeotmd  23315  rmulccn  23316  raddcn  23317  xrge0base  23325  xrge00  23326  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhmeo  23333  xrge0neqmnf  23345  snct  23354  dmct  23357  disjrdx  23385  lmxrge0  23390  rnlogblem  23416  log2le1  23424  esumnul  23442  esum0  23443  esumsn  23452  esumpfinvallem  23457  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  sigaex  23485  sigaclfu2  23497  dmsigagen  23520  measvuni  23557  measiuns  23559  imambfm  23582  mbfmvolf  23586  br2base  23589  itgmcntTMP  23603  ind1a  23619  probdif  23638  totprobd  23644  0rrv  23669  coinfliplem  23694  coinflipprob  23695  coinfliprv  23698  subfacf  23721  subfacp1lem1  23725  subfacp1lem5  23730  subfacp1lem6  23731  subfacval3  23735  erdszelem2  23738  erdszelem9  23745  erdszelem11  23747  kur14lem4  23755  iooscon  23793  iccllyscon  23796  umgrafi  23889  konigsberg  23926  ghomgrpilem1  24007  ghomgrpilem2  24008  circum  24022  axextprim  24062  axrepprim  24063  axunprim  24064  axinfprim  24067  axacprim  24068  inffz  24110  fz0n  24112  setinds  24204  dfon2lem2  24210  dfon2lem4  24212  dfrdg2  24222  axextdfeq  24224  poseq  24323  wfrlem4  24329  frrlem4  24354  sltval2  24380  nosgnn0  24382  sltintdifex  24387  sltres  24388  sltsolem1  24392  bdayfo  24399  symdifV  24439  fobigcup  24510  snelsingles  24531  fullfunfnv  24555  fullfunfv  24556  dfrdg4  24559  rankaltopb  24584  axlowdimlem4  24644  axlowdimlem13  24653  axlowdimlem16  24656  axlowdim1  24658  axlowdim  24660  linedegen  24837  bpoly0  24856  rank0  24871  rankeq1o  24872  hfuni  24885  nabi1i  24901  nabi2i  24902  limsucncmpi  24955  ovoliunnfl  25000  itg2addnclem  25002  itg2addnclem2  25003  dvreasin  25025  areacirclem2  25027  areacirclem3  25028  ump  25148  vxveqv  25156  prj1b  25181  prj3  25182  domncnt  25384  ranncnt  25385  toplat  25392  rrisgrp  25440  hmeogrpi  25638  intopcoaconlem3  25641  altretop  25702  phckle  26129  psckle  26130  smbkle  26145  pgapspf  26154  gtinf  26336  fneer  26390  neibastop1  26410  opelopab3  26475  fdc  26557  cntotbnd  26622  heiborlem6  26642  rrnval  26653  reheibor  26665  prter2  26851  diophrw  26940  0dioph  26960  rabren3dioph  27000  rencldnfilem  27005  pellexlem6  27021  pellex  27022  pellfundval  27067  frmx  27100  frmy  27101  jm2.23  27191  jm2.27dlem3  27206  axac10  27228  pw2f1ocnv  27232  wepwsolem  27240  kelac2lem  27264  lmhmlnmsplit  27287  dsmmbas2  27305  pwfi2f1o  27362  frlmpwfi  27364  dgraaval  27451  dgraaf  27454  symgsssg  27510  symgfisg  27511  psgnunilem5  27519  psgnghm  27539  seff  27640  expgrowthi  27652  expgrowth  27654  refsum2cnlem1  27810  infrglb  27824  clim1fr1  27829  dvcosre  27843  stoweidlem1  27852  stoweidlem7  27858  stoweidlem26  27877  stoweidlem34  27885  stoweidlem44  27895  stoweid  27914  wallispilem4  27919  wallispilem5  27920  wallispi  27921  wallispi2lem1  27922  stirlinglem5  27929  stirlinglem6  27930  stirlinglem13  27937  stirlinglem14  27938  stirlinglem15  27939  stirlingr  27941  f1oun2prg  28186  injresinjlem  28213  4fvwrd4  28219  usgraedgprv  28255  usgraexmpl  28266  wlkntrllem1  28344  wlkntrllem2  28345  wlkntrllem5  28348  0pth  28355  spthispth  28358  redwlk  28363  eupatrl  28384  constr3trllem3  28397  constr3pthlem3  28402  4cycl4dv  28412  ee233  28579  a9e2nd  28622  in1  28637  dfvd2ani  28650  dfvd2i  28652  dfvd3i  28659  dfvd3ani  28662  e0bi  28864  uun2221  28901  uun2221p1  28902  uun2221p2  28903  en3lpVD  28936  relopabVD  28992  a9e2ndVD  28999  a9e2ndALT  29022  bnj521  29080  bnj1098  29130  bnj1109  29133  bnj1131  29134  bnj1533  29199  bnj151  29224  bnj580  29260  bnj852  29268  bnj864  29269  bnj865  29270  bnj978  29296  bnj1021  29311  bnj907  29312  bnj1093  29325  bnj1145  29338  bnj1172  29346  bnj1174  29348  bnj1176  29350  bnj1186  29352  sbcoNEW7  29555  sbidmNEW7  29557  sbcomOLD7  29709  sb9iOLD7  29712  ax12conj2  29730  cdleme0moN  31036  mapdunirnN  32462
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