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  2140  sbidm  2142  axi12  2391  eqcomi  2416  eqtri  2432  eleqtri  2484  neeqtri  2596  necomi  2657  nemtbir  2663  nrex  2776  rexlimi  2791  isseti  2930  vtocl2  2975  vtocl3  2976  eueq1  3075  euxfr2  3087  cdeqri  3115  sseqtri  3348  3sstr3i  3354  pssn2lp  3416  equncomi  3461  unssi  3490  ssini  3532  unabs  3539  inabs  3540  dfin4  3549  npss0  3634  difid  3664  disjdif  3668  difin0  3669  snid  3809  snsssn  3935  iinrab2  4122  rintn0  4149  breqtri  4203  axsep  4297  bm1.3ii  4301  ax9vsep  4302  zfnuleu  4303  notzfaus  4342  zfpow  4346  dtru  4358  dtruALT  4364  dtruALT2  4376  copsexg  4410  uniop  4427  pwundif  4458  onunisuci  4662  zfun  4669  reusv2lem4  4694  reuxfr2d  4713  op1stb  4725  tfinds2  4810  omon  4823  relop  4990  rn0  5094  dmresi  5163  issref  5214  somincom  5238  cnvcnv  5290  rescnvcnv  5299  cnvcnvres  5300  cnvsn  5319  cocnvcnv2  5348  cores2  5349  co01  5351  relcoi1  5365  cnviin  5376  iota4an  5404  fnopab  5536  mpt0  5539  fnmpti  5540  f1cnvcnv  5614  f1ovi  5681  fvco4i  5768  fmpti  5859  fvsnun2  5896  funiunfv  5962  oprabss  6126  relmptopab  6259  2nd0  6321  f1stres  6335  f2ndres  6336  relmpt2opab  6396  df1st2  6400  df2nd2  6401  fsplit  6418  reldmtpos  6454  dftpos4  6465  tpostpos  6466  tpos0  6476  smo0  6587  tfrlem14  6619  tfrlem16  6621  rdgsucg  6648  rdglimg  6650  frfnom  6659  oawordeulem  6764  uniixp  7052  dfdom2  7100  ssdomg  7120  2dom  7146  xpcomf1o  7164  sbthlem5  7188  pwdom  7226  map2xp  7244  limensuci  7250  fiint  7350  fidomdm  7355  pwfilem  7367  mptfi  7372  fisn  7398  dffi3  7402  ordtypelem6  7456  ordtypelem7  7457  wemaplem2  7480  wdompwdom  7510  harwdom  7522  suc11reg  7538  zfinf  7558  axinf2  7559  noinfep  7578  cantnfvalf  7584  cantnflt  7591  cantnf0  7594  cantnf  7613  tz9.1c  7630  tc2  7645  r111  7665  r1tr2  7667  r1ordg  7668  r1sssuc  7673  r1val1  7676  tz9.13  7681  r1elssi  7695  pwwf  7697  rankopb  7742  rankeq0b  7750  ranksuc  7755  rankxplim  7767  rankxplim3  7769  rankxpsuc  7770  cp  7779  karden  7783  card0  7809  cardlim  7823  cardom  7837  pm54.43lem  7850  infxpenlem  7859  alephsuc2  7925  alephgeom  7927  alephprc  7944  unialeph  7946  dfac4  7967  dfacacn  7985  cda1dif  8020  pm110.643  8021  infcda1  8037  ackbij1lem13  8076  ackbij2  8087  cf0  8095  cfsuc  8101  cfom  8108  cfslb2n  8112  ominf4  8156  fin23lem17  8182  fin23lem28  8184  fin23lem30  8186  fin23lem31  8187  fin23lem40  8195  isfin1-3  8230  dfacfin7  8243  fin1a2lem6  8249  itunitc1  8264  axcc3  8282  dcomex  8291  axdc2lem  8292  axcclem  8301  zfac  8304  ac3  8306  ackm  8309  axac2  8310  axac  8311  axaci  8312  cardeqv  8313  numth2  8315  numth  8316  brdom3  8370  fin71ac  8375  cardf  8389  aleph1  8410  cfpwsdom  8423  smobeth  8425  zfcndrep  8453  zfcndpow  8455  zfcndac  8458  canthp1lem2  8492  gch2  8518  wunex3  8580  tskpr  8609  inar1  8614  rankcf  8616  tskcard  8620  tskuni  8622  grothpw  8665  axgroth4  8671  grothprim  8673  inaprc  8675  dmaddpi  8731  dmmulpi  8732  1lt2pi  8746  addpqf  8785  mulpqf  8787  1lt2nq  8814  supsrlem  8950  renepnf  9096  renemnf  9097  ssxr  9109  ltxrlt  9110  subf  9271  negne0i  9339  negdii  9348  ine0  9433  mulnzcnopr  9632  recgt0ii  9880  lbinfm  9925  infmsup  9950  infmrgelb  9952  infmrlb  9953  inelr  9954  halflt1  10153  nn0ssz  10266  zeo  10319  numlt  10365  numltc  10366  uzf  10455  uzinfmi  10519  xrltnr  10684  pnfnlt  10689  nltmnf  10690  xaddf  10774  xsubge0  10804  xmulf  10815  infmxrcl  10859  infmxrlb  10876  infmxrgelb  10877  xrinfm0  10879  ixxf  10890  ixxssxr  10892  iooval2  10913  ioof  10966  unirnioo  10968  dfioo2  10969  fzval2  11010  fzf  11011  fz10  11039  4fvwrd4  11084  fzof  11100  fzo0  11122  injresinjlem  11162  om2uzoi  11258  faclbnd4lem1  11547  hashkf  11583  hashgval  11584  hashinf  11586  hashclb  11604  hasheq0  11607  hashnn0n0nn  11627  hashbclem  11664  wrdexg  11702  rev0  11759  f1oun2prg  11827  sqr2gt1lt2  12043  limsupgord  12229  limsupval  12231  fclim  12310  fsumrelem  12549  ackbijnn  12570  incexclem  12579  incexc  12580  arisum2  12603  georeclim  12612  geoisumr  12618  0.999...  12621  geoihalfsum  12622  ege2le3  12655  sin0  12713  ef01bndlem  12748  cos2bnd  12752  cos01gt0  12755  sincos2sgn  12758  sin4lt0  12759  egt2lt3  12768  rpnnen2lem3  12779  rpnnen2lem9  12785  rexpen  12790  cnso  12809  nthruc  12813  dvdslelem  12857  divalglem1  12877  divalglem5  12880  divalglem6  12881  divalglem10  12885  bitsfzolem  12909  bitsfzo  12910  0bits  12914  bitsinv1lem  12916  sadcf  12928  sadcadd  12933  bitsshft  12950  smupf  12953  gcdf  12982  eucalgf  13037  isprm3  13051  2prm  13058  dfphi2  13126  odzval  13140  pcgcd1  13213  pc2dvds  13215  pockthi  13238  prmreclem2  13248  prmrec  13253  vdwapf  13303  vdwap0  13307  vdwlem6  13317  ramval  13339  ramcl2lem  13340  ramtcl2  13342  karatsuba  13383  1259lem5  13417  2503lem3  13421  4001lem4  13426  structcnvcnv  13443  structfn  13445  strlemor1  13519  strleun  13522  prdsval  13641  prdsds  13649  imasdsfn  13703  imasdsval  13704  imasvscafn  13725  xpsc0  13748  xpsc1  13749  xpsfrnel2  13753  xpsff1o  13756  sscpwex  13978  wunfunc  14059  wunnat  14116  eldmcoa  14183  coapm  14189  setcepi  14206  catcfuccl  14227  catcxpccl  14267  yonedainv  14341  plusffval  14665  grpinvfvi  14809  mulgfvi  14857  odval  15135  odf  15138  odhash3  15173  gexval  15175  sylow3lem2  15225  oppglsm  15239  efgmf  15308  efgval  15312  efgsf  15324  0frgp  15374  gsumzaddlem  15489  dmdprd  15522  dprdval  15524  invrfval  15741  drngui  15804  scaffval  15931  lssintcl  16003  mplsubrglem  16465  opsrtoslem2  16508  cnfld0  16688  cnfld1  16689  cnfldsub  16692  xrsds  16704  xrsdsreclblem  16707  ipffval  16842  ocv1  16869  eltpsi  16974  fctop  17031  cctop  17033  ppttop  17034  epttop  17036  leordtvallem1  17236  leordtvallem2  17237  iccordt  17240  pnfnei  17246  mnfnei  17247  iscnp2  17265  discmp  17423  concompcld  17458  1stcrestlem  17476  2ndcdisj  17480  topnlly  17515  disllycmp  17522  dis1stc  17523  txuni2  17558  xkotf  17578  dfac14lem  17610  prdstps  17622  txindis  17627  tx1stc  17643  xkohaus  17646  xkoptsub  17647  cnmpt1st  17661  cnmpt2nd  17662  ptcmpfi  17806  filcon  17876  trfil1  17879  fin1aufil  17925  tgpconcompeqg  18102  tgpconcomp  18103  tsmsres  18134  trust  18220  met1stc  18512  dscmet  18581  nmoval  18710  retopon  18758  cnfldtopon  18778  xrsxmet  18801  xrsmopn  18804  metdsval  18838  iimulcn  18924  icopnfhmeo  18929  iccpnfhmeo  18931  xrhmeo  18932  xrhmph  18933  cnheiborlem  18940  lebnumii  18952  ishtpy  18958  htpycc  18966  pco1  19001  pcohtpylem  19005  pcopt  19008  pcopt2  19009  pcoass  19010  pcorevlem  19012  cfilresi  19209  ovolval  19331  ovolf  19339  ovoliunlem3  19361  ovolicc1  19373  ovolicc2  19379  volf  19386  ioorf  19426  dyadf  19444  dyadmbl  19453  vitalilem4  19464  vitalilem5  19465  vitali  19466  mbfimaopnlem  19508  mbflimsup  19519  0plef  19525  i1fima  19531  i1fima2  19532  i1fd  19534  i1f0rn  19535  itg1ge0  19539  itg10  19541  i1f1lem  19542  i1fadd  19548  i1fmul  19549  i1fmulc  19556  mbfi1fseqlem5  19572  itg2addlem  19611  reldv  19718  dvbsss  19750  dvef  19825  dvlt0  19850  lhop1lem  19858  deg1fvi  19969  deg1nn0clb  19974  plypf1  20092  coeeulem  20104  coeeu  20105  vieta1lem2  20189  elqaalem1  20197  elqaalem3  20199  aannenlem3  20208  aalioulem2  20211  aalioulem3  20212  dvradcnv  20298  pserulm  20299  pserdvlem2  20305  abelthlem6  20313  sinhalfpilem  20335  sincos4thpi  20382  tan4thpi  20383  sincos6thpi  20384  pige3  20386  coseq1  20391  resinf1o  20399  tanord1  20400  tanregt0  20402  relogrn  20420  dfrelog  20424  logneg  20443  logltb  20455  logcn  20499  logf1o2  20502  dvlog  20503  efopnlem2  20509  efopn  20510  logccv  20515  dvsqr  20589  cxpcn3  20593  angpined  20632  1cubr  20643  atanre  20686  asinsin  20693  asin1  20695  reasinsin  20697  atan0  20709  atanbnd  20727  atan1  20729  log2cnv  20745  log2ublem3  20749  log2ub  20750  birthday  20754  amgmlem  20789  emcllem5  20799  emgt0  20806  harmonicbnd3  20807  ftalem3  20818  basellem4  20827  sgmf  20889  ppi1  20908  cht1  20909  vma1  20910  ppiltx  20921  sqff1o  20926  ppiublem1  20947  ppiublem2  20948  ppiub  20949  chtub  20957  dchreq  21003  bposlem7  21035  bposlem8  21036  bposlem9  21037  lgsdir2lem2  21069  lgsdir2lem3  21070  chebbnd1  21127  chto1ub  21131  chpo1ubb  21136  pntibndlem1  21244  umgrafi  21318  usgraedgprv  21357  usgraexmpl  21381  usgrafilem1  21386  2trllemA  21511  wlkntrllem1  21520  wlkntrllem3  21522  0pth  21531  spthispth  21534  2pthon  21563  2pthon3v  21565  redwlk  21567  constr3trllem3  21600  constr3pthlem3  21605  4cycl4dv  21615  konigsberg  21670  ex-dif  21692  ex-un  21693  ex-in  21694  ex-fl  21716  avril1  21718  ginvsn  21898  cnid  21900  mulid  21905  rngosn3  21975  vcoprnelem  22018  vcoprne  22019  vcex  22020  cnnvm  22135  ipasslem8  22299  ipasslem10  22301  hvsubf  22479  normlem1  22573  normlem6  22578  normlem7  22579  norm-ii-i  22600  norm3adifii  22611  hilid  22624  hlimf  22701  norm1exi  22713  hhssabloi  22723  hhssnv  22725  hhshsslem1  22728  shincli  22825  shsval2i  22850  shs0i  22912  chj0i  22918  chm1i  22919  chincli  22923  chdmm1i  22940  shjshsi  22955  chsup0  23011  h1de2bi  23017  spansnpji  23041  cmcmlem  23054  cmcmii  23060  cmcm2ii  23061  cmcm3ii  23062  pjidmi  23136  pjssmii  23144  pj0i  23156  pjocini  23161  mayetes3i  23193  df0op2  23216  hoaddcomi  23236  hoaddassi  23240  hocadddiri  23243  hocsubdiri  23244  hoaddid1i  23250  ho0coi  23252  hoid1i  23253  hoid1ri  23254  hodseqi  23258  honegsubi  23260  adj1o  23358  hoddii  23453  lnopunilem1  23474  lnopunilem2  23475  nmcopexi  23491  nmcopex  23493  nmcoplb  23494  nmcfnexi  23515  nmcfnex  23517  nmcfnlb  23518  adjbd1o  23549  adjcoi  23564  nmopcoadji  23565  opsqrlem6  23609  pjsdii  23619  pjddii  23620  pjidmcoi  23641  pjtoi  23643  pjin1i  23656  pjclem1  23659  stji1i  23706  largei  23731  reuxfr3d  23937  iuninc  23972  rinvf1o  24003  suppss2f  24010  xppreima  24020  ofoprabco  24040  funcnvmptOLD  24043  gtiso  24049  df1stres  24052  df2ndres  24053  snct  24064  dmct  24067  hashresfn  24117  ressplusf  24144  xrge0base  24168  xrge00  24169  xrge0neqmnf  24173  xrnarchi  24215  unicls  24262  sqsscirc1  24267  mhmhmeotmd  24274  rmulccn  24275  raddcn  24276  xrge0iifiso  24282  xrge0iifhmeo  24283  lmxrge0  24298  cnzh  24315  rezh  24316  qqh0  24329  qqh1  24330  qqhre  24347  rrhre  24348  rnlogblem  24360  log2le1  24368  ind1a  24379  esumnul  24404  esum0  24405  esumsn  24417  esumpfinvallem  24425  esumpfinvalf  24427  esumpcvgval  24429  sigaclfu2  24465  dmsigagen  24488  imambfm  24573  mbfmvolf  24577  br2base  24580  sibfof  24615  sitmcl  24624  probdif  24639  0rrv  24670  coinfliplem  24697  coinflipprob  24698  coinfliprv  24701  ballotlem2  24707  ballotlem4  24717  ballotlem5  24718  ballotlemi  24719  ballotlemiex  24720  ballotlemi1  24721  ballotlemii  24722  ballotlemsup  24723  ballotlemimin  24724  ballotlem1c  24726  ballotlemfrcn0  24748  ballotlemirc  24750  ballotlem7  24754  ballotth  24756  subfacf  24822  subfacp1lem1  24826  subfacp1lem5  24831  subfacp1lem6  24832  subfacval3  24836  erdszelem2  24839  erdszelem9  24846  erdszelem11  24848  kur14lem4  24856  iooscon  24895  iccllyscon  24898  ghomgrpilem1  25057  ghomgrpilem2  25058  circum  25072  axextprim  25111  axrepprim  25112  axunprim  25113  axinfprim  25116  axacprim  25117  inffz  25161  fz0n  25163  risefall0lem  25302  binomfallfaclem2  25315  setinds  25356  dfon2lem2  25362  dfon2lem4  25364  dfrdg2  25374  axextdfeq  25376  poseq  25475  wfrlem4  25481  frrlem4  25506  sltval2  25532  nosgnn0  25534  sltintdifex  25539  sltres  25540  sltsolem1  25544  bdayfo  25551  symdifV  25591  fobigcup  25662  snelsingles  25683  fullfunfnv  25707  fullfunfv  25708  dfrdg4  25711  rankaltopb  25736  axlowdimlem4  25796  axlowdimlem13  25805  axlowdimlem16  25808  axlowdim1  25810  axlowdim  25812  linedegen  25989  rank0  26023  rankeq1o  26024  hfuni  26037  nabi1i  26053  nabi2i  26054  limsucncmpi  26107  mblfinlem  26151  ovoliunnfl  26155  voliunnfl  26157  itg2addnclem  26163  itg2addnclem2  26164  dvreasin  26187  areacirclem2  26189  areacirclem3  26190  gtinf  26220  fneer  26266  neibastop1  26286  opelopab3  26316  fdc  26347  cntotbnd  26403  heiborlem6  26423  rrnval  26434  reheibor  26446  prter2  26628  diophrw  26715  0dioph  26735  rabren3dioph  26774  rencldnfilem  26779  pellexlem6  26795  pellex  26796  pellfundval  26841  frmx  26874  frmy  26875  jm2.23  26965  jm2.27dlem3  26980  axac10  27002  pw2f1ocnv  27006  wepwsolem  27014  kelac2lem  27038  lmhmlnmsplit  27061  dsmmbas2  27079  pwfi2f1o  27136  frlmpwfi  27138  dgraaval  27225  dgraaf  27228  symgsssg  27284  symgfisg  27285  psgnunilem5  27293  psgnghm  27313  seff  27414  expgrowthi  27426  expgrowth  27428  refsum2cnlem1  27583  infrglb  27597  dvcosre  27616  stoweidlem1  27625  stoweidlem7  27631  stoweidlem26  27650  stoweidlem34  27658  stoweidlem44  27668  stoweid  27687  stirlinglem5  27702  stirlinglem6  27703  axorbtnotaiffb  27746  axorbciffatcxorb  27748  abnotbtaxb  27759  resisresindm  27965  fzo0ss1  27993  frgrawopreg2  28162  ee233  28321  a9e2nd  28364  in1  28380  dfvd2ani  28393  dfvd2i  28395  dfvd3i  28402  dfvd3ani  28405  e0bi  28606  uun2221  28643  uun2221p1  28644  uun2221p2  28645  en3lpVD  28675  relopabVD  28731  a9e2ndVD  28738  a9e2ndALT  28761  bnj521  28822  bnj1098  28872  bnj1109  28875  bnj1131  28876  bnj1533  28941  bnj151  28966  bnj580  29002  bnj852  29010  bnj864  29011  bnj865  29012  bnj978  29038  bnj1021  29053  bnj907  29054  bnj1093  29067  bnj1145  29080  bnj1172  29088  bnj1174  29090  bnj1176  29092  bnj1186  29094  sbcoNEW7  29297  sbidmNEW7  29299  sbcomOLD7  29451  sb9iOLD7  29454  mapdunirnN  32145
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