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

Theorem mpbi 200
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 187 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  pm5.74i  237  notbii  288  pm5.19  350  ori  365  imori  403  pm4.71i  614  pm4.71ri  615  pm5.32i  619  pm3.24  853  pm5.16  861  biluk  900  4exmid  906  dn1  933  3ori  1244  trubifal  1357  nic-dfim  1440  nic-dfneg  1441  nic-mp  1442  nic-mpALT  1443  tbw-negdf  1470  rb-imdf  1521  mpto2  1540  mpto2OLD  1541  mtp-xorOLD  1543  mpgbi  1555  19.35i  1608  19.36i  1889  19.37aiv  1919  ax9  1949  sbco  2132  sbidm  2134  axi12  2383  eqcomi  2408  eqtri  2424  eleqtri  2476  neeqtri  2588  necomi  2649  nemtbir  2655  nrex  2768  rexlimi  2783  isseti  2922  vtocl2  2967  vtocl3  2968  eueq1  3067  euxfr2  3079  cdeqri  3107  sseqtri  3340  3sstr3i  3346  pssn2lp  3408  equncomi  3453  unssi  3482  ssini  3524  unabs  3531  inabs  3532  dfin4  3541  npss0  3626  difid  3656  disjdif  3660  difin0  3661  snid  3801  snsssn  3927  iinrab2  4114  rintn0  4141  breqtri  4195  axsep  4289  bm1.3ii  4293  ax9vsep  4294  zfnuleu  4295  notzfaus  4334  zfpow  4338  dtru  4350  dtruALT  4356  dtruALT2  4368  copsexg  4402  uniop  4419  pwundif  4450  onunisuci  4654  zfun  4661  reusv2lem4  4686  reuxfr2d  4705  op1stb  4717  tfinds2  4802  omon  4815  relop  4982  rn0  5086  dmresi  5155  issref  5206  somincom  5230  cnvcnv  5282  rescnvcnv  5291  cnvcnvres  5292  cnvsn  5311  cocnvcnv2  5340  cores2  5341  co01  5343  relcoi1  5357  cnviin  5368  iota4an  5396  fnopab  5528  mpt0  5531  fnmpti  5532  f1cnvcnv  5606  f1ovi  5673  fvco4i  5760  fmpti  5851  fvsnun2  5888  funiunfv  5954  oprabss  6118  relmptopab  6251  2nd0  6313  f1stres  6327  f2ndres  6328  relmpt2opab  6388  df1st2  6392  df2nd2  6393  fsplit  6410  reldmtpos  6446  dftpos4  6457  tpostpos  6458  tpos0  6468  smo0  6579  tfrlem14  6611  tfrlem16  6613  rdgsucg  6640  rdglimg  6642  frfnom  6651  oawordeulem  6756  uniixp  7044  dfdom2  7092  ssdomg  7112  2dom  7138  xpcomf1o  7156  sbthlem5  7180  pwdom  7218  map2xp  7236  limensuci  7242  fiint  7342  fidomdm  7347  pwfilem  7359  mptfi  7364  fisn  7390  dffi3  7394  ordtypelem6  7448  ordtypelem7  7449  wemaplem2  7472  wdompwdom  7502  harwdom  7514  suc11reg  7530  zfinf  7550  axinf2  7551  noinfep  7570  cantnfvalf  7576  cantnflt  7583  cantnf0  7586  cantnf  7605  tz9.1c  7622  tc2  7637  r111  7657  r1tr2  7659  r1ordg  7660  r1sssuc  7665  r1val1  7668  tz9.13  7673  r1elssi  7687  pwwf  7689  rankopb  7734  rankeq0b  7742  ranksuc  7747  rankxplim  7759  rankxplim3  7761  rankxpsuc  7762  cp  7771  karden  7775  card0  7801  cardlim  7815  cardom  7829  pm54.43lem  7842  infxpenlem  7851  alephsuc2  7917  alephgeom  7919  alephprc  7936  unialeph  7938  dfac4  7959  dfacacn  7977  cda1dif  8012  pm110.643  8013  infcda1  8029  ackbij1lem13  8068  ackbij2  8079  cf0  8087  cfsuc  8093  cfom  8100  cfslb2n  8104  ominf4  8148  fin23lem17  8174  fin23lem28  8176  fin23lem30  8178  fin23lem31  8179  fin23lem40  8187  isfin1-3  8222  dfacfin7  8235  fin1a2lem6  8241  itunitc1  8256  axcc3  8274  dcomex  8283  axdc2lem  8284  axcclem  8293  zfac  8296  ac3  8298  ackm  8301  axac2  8302  axac  8303  axaci  8304  cardeqv  8305  numth2  8307  numth  8308  brdom3  8362  fin71ac  8367  cardf  8381  aleph1  8402  cfpwsdom  8415  smobeth  8417  zfcndrep  8445  zfcndpow  8447  zfcndac  8450  canthp1lem2  8484  gch2  8510  wunex3  8572  tskpr  8601  inar1  8606  rankcf  8608  tskcard  8612  tskuni  8614  grothpw  8657  axgroth4  8663  grothprim  8665  inaprc  8667  dmaddpi  8723  dmmulpi  8724  1lt2pi  8738  addpqf  8777  mulpqf  8779  1lt2nq  8806  supsrlem  8942  renepnf  9088  renemnf  9089  ssxr  9101  ltxrlt  9102  subf  9263  negne0i  9331  negdii  9340  ine0  9425  mulnzcnopr  9624  recgt0ii  9872  lbinfm  9917  infmsup  9942  infmrgelb  9944  infmrlb  9945  inelr  9946  halflt1  10145  nn0ssz  10258  zeo  10311  numlt  10357  numltc  10358  uzf  10447  uzinfmi  10511  xrltnr  10676  pnfnlt  10681  nltmnf  10682  xaddf  10766  xsubge0  10796  xmulf  10807  infmxrcl  10851  infmxrlb  10868  infmxrgelb  10869  xrinfm0  10871  ixxf  10882  ixxssxr  10884  iooval2  10905  ioof  10958  unirnioo  10960  dfioo2  10961  fzval2  11002  fzf  11003  fz10  11031  4fvwrd4  11076  fzof  11092  fzo0  11114  injresinjlem  11154  om2uzoi  11250  faclbnd4lem1  11539  hashkf  11575  hashgval  11576  hashinf  11578  hashclb  11596  hasheq0  11599  hashnn0n0nn  11619  hashbclem  11656  wrdexg  11694  rev0  11751  f1oun2prg  11819  sqr2gt1lt2  12035  limsupgord  12221  limsupval  12223  fclim  12302  fsumrelem  12541  ackbijnn  12562  incexclem  12571  incexc  12572  arisum2  12595  georeclim  12604  geoisumr  12610  0.999...  12613  geoihalfsum  12614  ege2le3  12647  sin0  12705  ef01bndlem  12740  cos2bnd  12744  cos01gt0  12747  sincos2sgn  12750  sin4lt0  12751  egt2lt3  12760  rpnnen2lem3  12771  rpnnen2lem9  12777  rexpen  12782  cnso  12801  nthruc  12805  dvdslelem  12849  divalglem1  12869  divalglem5  12872  divalglem6  12873  divalglem10  12877  bitsfzolem  12901  bitsfzo  12902  0bits  12906  bitsinv1lem  12908  sadcf  12920  sadcadd  12925  bitsshft  12942  smupf  12945  gcdf  12974  eucalgf  13029  isprm3  13043  2prm  13050  dfphi2  13118  odzval  13132  pcgcd1  13205  pc2dvds  13207  pockthi  13230  prmreclem2  13240  prmrec  13245  vdwapf  13295  vdwap0  13299  vdwlem6  13309  ramval  13331  ramcl2lem  13332  ramtcl2  13334  karatsuba  13375  1259lem5  13409  2503lem3  13413  4001lem4  13418  structcnvcnv  13435  structfn  13437  strlemor1  13511  strleun  13514  prdsval  13633  prdsds  13641  imasdsfn  13695  imasdsval  13696  imasvscafn  13717  xpsc0  13740  xpsc1  13741  xpsfrnel2  13745  xpsff1o  13748  sscpwex  13970  wunfunc  14051  wunnat  14108  eldmcoa  14175  coapm  14181  setcepi  14198  catcfuccl  14219  catcxpccl  14259  yonedainv  14333  plusffval  14657  grpinvfvi  14801  mulgfvi  14849  odval  15127  odf  15130  odhash3  15165  gexval  15167  sylow3lem2  15217  oppglsm  15231  efgmf  15300  efgval  15304  efgsf  15316  0frgp  15366  gsumzaddlem  15481  dmdprd  15514  dprdval  15516  invrfval  15733  drngui  15796  scaffval  15923  lssintcl  15995  mplsubrglem  16457  opsrtoslem2  16500  cnfld0  16680  cnfld1  16681  cnfldsub  16684  xrsds  16696  xrsdsreclblem  16699  ipffval  16834  ocv1  16861  eltpsi  16966  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  leordtvallem1  17228  leordtvallem2  17229  iccordt  17232  pnfnei  17238  mnfnei  17239  iscnp2  17257  discmp  17415  concompcld  17450  1stcrestlem  17468  2ndcdisj  17472  topnlly  17507  disllycmp  17514  dis1stc  17515  txuni2  17550  xkotf  17570  dfac14lem  17602  prdstps  17614  txindis  17619  tx1stc  17635  xkohaus  17638  xkoptsub  17639  cnmpt1st  17653  cnmpt2nd  17654  ptcmpfi  17798  filcon  17868  trfil1  17871  fin1aufil  17917  tgpconcompeqg  18094  tgpconcomp  18095  tsmsres  18126  trust  18212  met1stc  18504  dscmet  18573  nmoval  18702  retopon  18750  cnfldtopon  18770  xrsxmet  18793  xrsmopn  18796  metdsval  18830  iimulcn  18916  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  xrhmph  18925  cnheiborlem  18932  lebnumii  18944  ishtpy  18950  htpycc  18958  pco1  18993  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  cfilresi  19201  ovolval  19323  ovolf  19331  ovoliunlem3  19353  ovolicc1  19365  ovolicc2  19371  volf  19378  ioorf  19418  dyadf  19436  dyadmbl  19445  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfimaopnlem  19500  mbflimsup  19511  0plef  19517  i1fima  19523  i1fima2  19524  i1fd  19526  i1f0rn  19527  itg1ge0  19531  itg10  19533  i1f1lem  19534  i1fadd  19540  i1fmul  19541  i1fmulc  19548  mbfi1fseqlem5  19564  itg2addlem  19603  reldv  19710  dvbsss  19742  dvef  19817  dvlt0  19842  lhop1lem  19850  deg1fvi  19961  deg1nn0clb  19966  plypf1  20084  coeeulem  20096  coeeu  20097  vieta1lem2  20181  elqaalem1  20189  elqaalem3  20191  aannenlem3  20200  aalioulem2  20203  aalioulem3  20204  dvradcnv  20290  pserulm  20291  pserdvlem2  20297  abelthlem6  20305  sinhalfpilem  20327  sincos4thpi  20374  tan4thpi  20375  sincos6thpi  20376  pige3  20378  coseq1  20383  resinf1o  20391  tanord1  20392  tanregt0  20394  relogrn  20412  dfrelog  20416  logneg  20435  logltb  20447  logcn  20491  logf1o2  20494  dvlog  20495  efopnlem2  20501  efopn  20502  logccv  20507  dvsqr  20581  cxpcn3  20585  angpined  20624  1cubr  20635  atanre  20678  asinsin  20685  asin1  20687  reasinsin  20689  atan0  20701  atanbnd  20719  atan1  20721  log2cnv  20737  log2ublem3  20741  log2ub  20742  birthday  20746  amgmlem  20781  emcllem5  20791  emgt0  20798  harmonicbnd3  20799  ftalem3  20810  basellem4  20819  sgmf  20881  ppi1  20900  cht1  20901  vma1  20902  ppiltx  20913  sqff1o  20918  ppiublem1  20939  ppiublem2  20940  ppiub  20941  chtub  20949  dchreq  20995  bposlem7  21027  bposlem8  21028  bposlem9  21029  lgsdir2lem2  21061  lgsdir2lem3  21062  chebbnd1  21119  chto1ub  21123  chpo1ubb  21128  pntibndlem1  21236  umgrafi  21310  usgraedgprv  21349  usgraexmpl  21373  usgrafilem1  21378  2trllemA  21503  wlkntrllem1  21512  wlkntrllem3  21514  0pth  21523  spthispth  21526  2pthon  21555  2pthon3v  21557  redwlk  21559  constr3trllem3  21592  constr3pthlem3  21597  4cycl4dv  21607  konigsberg  21662  ex-dif  21684  ex-un  21685  ex-in  21686  ex-fl  21708  avril1  21710  ginvsn  21890  cnid  21892  mulid  21897  rngosn3  21967  vcoprnelem  22010  vcoprne  22011  vcex  22012  cnnvm  22127  ipasslem8  22291  ipasslem10  22293  hvsubf  22471  normlem1  22565  normlem6  22570  normlem7  22571  norm-ii-i  22592  norm3adifii  22603  hilid  22616  hlimf  22693  norm1exi  22705  hhssabloi  22715  hhssnv  22717  hhshsslem1  22720  shincli  22817  shsval2i  22842  shs0i  22904  chj0i  22910  chm1i  22911  chincli  22915  chdmm1i  22932  shjshsi  22947  chsup0  23003  h1de2bi  23009  spansnpji  23033  cmcmlem  23046  cmcmii  23052  cmcm2ii  23053  cmcm3ii  23054  pjidmi  23128  pjssmii  23136  pj0i  23148  pjocini  23153  mayetes3i  23185  df0op2  23208  hoaddcomi  23228  hoaddassi  23232  hocadddiri  23235  hocsubdiri  23236  hoaddid1i  23242  ho0coi  23244  hoid1i  23245  hoid1ri  23246  hodseqi  23250  honegsubi  23252  adj1o  23350  hoddii  23445  lnopunilem1  23466  lnopunilem2  23467  nmcopexi  23483  nmcopex  23485  nmcoplb  23486  nmcfnexi  23507  nmcfnex  23509  nmcfnlb  23510  adjbd1o  23541  adjcoi  23556  nmopcoadji  23557  opsqrlem6  23601  pjsdii  23611  pjddii  23612  pjidmcoi  23633  pjtoi  23635  pjin1i  23648  pjclem1  23651  stji1i  23698  largei  23723  reuxfr3d  23929  iuninc  23964  rinvf1o  23995  suppss2f  24002  xppreima  24012  ofoprabco  24032  funcnvmptOLD  24035  gtiso  24041  df1stres  24044  df2ndres  24045  snct  24056  dmct  24059  hashresfn  24109  ressplusf  24136  xrge0base  24160  xrge00  24161  xrge0neqmnf  24165  xrnarchi  24207  unicls  24254  sqsscirc1  24259  mhmhmeotmd  24266  rmulccn  24267  raddcn  24268  xrge0iifiso  24274  xrge0iifhmeo  24275  lmxrge0  24290  cnzh  24307  rezh  24308  qqh0  24321  qqh1  24322  qqhre  24339  rrhre  24340  rnlogblem  24352  log2le1  24360  ind1a  24371  esumnul  24396  esum0  24397  esumsn  24409  esumpfinvallem  24417  esumpfinvalf  24419  esumpcvgval  24421  sigaclfu2  24457  dmsigagen  24480  imambfm  24565  mbfmvolf  24569  br2base  24572  sibfof  24607  sitmcl  24616  probdif  24631  0rrv  24662  coinfliplem  24689  coinflipprob  24690  coinfliprv  24693  ballotlem2  24699  ballotlem4  24709  ballotlem5  24710  ballotlemi  24711  ballotlemiex  24712  ballotlemi1  24713  ballotlemii  24714  ballotlemsup  24715  ballotlemimin  24716  ballotlem1c  24718  ballotlemfrcn0  24740  ballotlemirc  24742  ballotlem7  24746  ballotth  24748  subfacf  24814  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  subfacval3  24828  erdszelem2  24831  erdszelem9  24838  erdszelem11  24840  kur14lem4  24848  iooscon  24887  iccllyscon  24890  ghomgrpilem1  25049  ghomgrpilem2  25050  circum  25064  axextprim  25103  axrepprim  25104  axunprim  25105  axinfprim  25108  axacprim  25109  inffz  25153  fz0n  25155  risefall0lem  25294  binomfallfaclem2  25307  setinds  25348  dfon2lem2  25354  dfon2lem4  25356  dfrdg2  25366  axextdfeq  25368  poseq  25467  wfrlem4  25473  frrlem4  25498  sltval2  25524  nosgnn0  25526  sltintdifex  25531  sltres  25532  sltsolem1  25536  bdayfo  25543  symdifV  25583  fobigcup  25654  snelsingles  25675  fullfunfnv  25699  fullfunfv  25700  dfrdg4  25703  rankaltopb  25728  axlowdimlem4  25788  axlowdimlem13  25797  axlowdimlem16  25800  axlowdim1  25802  axlowdim  25804  linedegen  25981  rank0  26015  rankeq1o  26016  hfuni  26029  nabi1i  26045  nabi2i  26046  limsucncmpi  26099  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  itg2addnclem  26155  itg2addnclem2  26156  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  gtinf  26212  fneer  26258  neibastop1  26278  opelopab3  26308  fdc  26339  cntotbnd  26395  heiborlem6  26415  rrnval  26426  reheibor  26438  prter2  26620  diophrw  26707  0dioph  26727  rabren3dioph  26766  rencldnfilem  26771  pellexlem6  26787  pellex  26788  pellfundval  26833  frmx  26866  frmy  26867  jm2.23  26957  jm2.27dlem3  26972  axac10  26994  pw2f1ocnv  26998  wepwsolem  27006  kelac2lem  27030  lmhmlnmsplit  27053  dsmmbas2  27071  pwfi2f1o  27128  frlmpwfi  27130  dgraaval  27217  dgraaf  27220  symgsssg  27276  symgfisg  27277  psgnunilem5  27285  psgnghm  27305  seff  27406  expgrowthi  27418  expgrowth  27420  refsum2cnlem1  27575  infrglb  27589  dvcosre  27608  stoweidlem1  27617  stoweidlem7  27623  stoweidlem26  27642  stoweidlem34  27650  stoweidlem44  27660  stoweid  27679  stirlinglem5  27694  stirlinglem6  27695  axorbtnotaiffb  27738  axorbciffatcxorb  27740  abnotbtaxb  27751  resisresindm  27957  fzo0ss1  27985  frgrawopreg2  28154  ee233  28313  a9e2nd  28356  in1  28371  dfvd2ani  28384  dfvd2i  28386  dfvd3i  28393  dfvd3ani  28396  e0bi  28597  uun2221  28634  uun2221p1  28635  uun2221p2  28636  en3lpVD  28666  relopabVD  28722  a9e2ndVD  28729  a9e2ndALT  28752  bnj521  28810  bnj1098  28860  bnj1109  28863  bnj1131  28864  bnj1533  28929  bnj151  28954  bnj580  28990  bnj852  28998  bnj864  28999  bnj865  29000  bnj978  29026  bnj1021  29041  bnj907  29042  bnj1093  29055  bnj1145  29068  bnj1172  29076  bnj1174  29078  bnj1176  29080  bnj1186  29082  sbcoNEW7  29285  sbidmNEW7  29287  sbcomOLD7  29439  sb9iOLD7  29442  mapdunirnN  32133
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 178
  Copyright terms: Public domain W3C validator