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  24205  dfon2lem2  24211  dfon2lem4  24213  dfrdg2  24223  axextdfeq  24225  poseq  24324  wfrlem4  24330  frrlem4  24355  sltval2  24381  nosgnn0  24383  sltintdifex  24388  sltres  24389  sltsolem1  24393  bdayfo  24400  symdifV  24440  fobigcup  24511  snelsingles  24532  fullfunfnv  24556  fullfunfv  24557  dfrdg4  24560  rankaltopb  24585  axlowdimlem4  24645  axlowdimlem13  24654  axlowdimlem16  24657  axlowdim1  24659  axlowdim  24661  linedegen  24838  bpoly0  24857  rank0  24872  rankeq1o  24873  hfuni  24886  nabi1i  24902  nabi2i  24903  limsucncmpi  24956  ovoliunnfl  25001  itg2addnclem  25003  itg2addnclem2  25004  dvreasin  25026  areacirclem2  25028  areacirclem3  25029  ump  25149  vxveqv  25157  prj1b  25182  prj3  25183  domncnt  25385  ranncnt  25386  toplat  25393  rrisgrp  25441  hmeogrpi  25639  intopcoaconlem3  25642  altretop  25703  phckle  26130  psckle  26131  smbkle  26146  pgapspf  26155  gtinf  26337  fneer  26391  neibastop1  26411  opelopab3  26476  fdc  26558  cntotbnd  26623  heiborlem6  26643  rrnval  26654  reheibor  26666  prter2  26852  diophrw  26941  0dioph  26961  rabren3dioph  27001  rencldnfilem  27006  pellexlem6  27022  pellex  27023  pellfundval  27068  frmx  27101  frmy  27102  jm2.23  27192  jm2.27dlem3  27207  axac10  27229  pw2f1ocnv  27233  wepwsolem  27241  kelac2lem  27265  lmhmlnmsplit  27288  dsmmbas2  27306  pwfi2f1o  27363  frlmpwfi  27365  dgraaval  27452  dgraaf  27455  symgsssg  27511  symgfisg  27512  psgnunilem5  27520  psgnghm  27540  seff  27641  expgrowthi  27653  expgrowth  27655  refsum2cnlem1  27811  infrglb  27825  clim1fr1  27830  dvcosre  27844  stoweidlem1  27853  stoweidlem7  27859  stoweidlem26  27878  stoweidlem34  27886  stoweidlem44  27896  stoweid  27915  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  stirlinglem5  27930  stirlinglem6  27931  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  stirlingr  27942  f1oun2prg  28187  injresinjlem  28214  4fvwrd4  28220  usgraedgprv  28256  usgraexmpl  28267  wlkntrllem1  28345  wlkntrllem2  28346  wlkntrllem5  28349  0pth  28356  spthispth  28359  redwlk  28364  eupatrl  28385  constr3trllem3  28398  constr3pthlem3  28403  4cycl4dv  28413  ee233  28580  a9e2nd  28623  in1  28638  dfvd2ani  28651  dfvd2i  28653  dfvd3i  28660  dfvd3ani  28663  e0bi  28865  uun2221  28902  uun2221p1  28903  uun2221p2  28904  en3lpVD  28937  relopabVD  28993  a9e2ndVD  29000  a9e2ndALT  29023  bnj521  29081  bnj1098  29131  bnj1109  29134  bnj1131  29135  bnj1533  29200  bnj151  29225  bnj580  29261  bnj852  29269  bnj864  29270  bnj865  29271  bnj978  29297  bnj1021  29312  bnj907  29313  bnj1093  29326  bnj1145  29339  bnj1172  29347  bnj1174  29349  bnj1176  29351  bnj1186  29353  sbcoNEW7  29556  sbidmNEW7  29558  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