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  1882  19.37aiv  1912  ax9  1942  spime  1950  sbco  2118  sbidm  2120  axi12  2369  eqcomi  2393  eqtri  2409  eleqtri  2461  neeqtri  2573  necomi  2634  nemtbir  2640  nrex  2753  rexlimi  2768  isseti  2907  vtocl2  2952  vtocl3  2953  eueq1  3052  euxfr2  3064  cdeqri  3092  sseqtri  3325  3sstr3i  3331  pssn2lp  3393  equncomi  3438  unssi  3467  ssini  3509  unabs  3516  inabs  3517  dfin4  3526  npss0  3611  difid  3641  disjdif  3645  difin0  3646  snid  3786  snsssn  3911  iinrab2  4097  rintn0  4124  breqtri  4178  axsep  4272  bm1.3ii  4276  ax9vsep  4277  zfnuleu  4278  notzfaus  4317  zfpow  4321  dtru  4333  dtruALT  4339  dtruALT2  4351  copsexg  4385  uniop  4402  pwundif  4433  onunisuci  4637  zfun  4644  reusv2lem4  4669  reuxfr2d  4688  op1stb  4700  tfinds2  4785  omon  4798  relop  4965  rn0  5069  dmresi  5138  issref  5189  somincom  5213  cnvcnv  5265  rescnvcnv  5274  cnvcnvres  5275  cnvsn  5294  cocnvcnv2  5323  cores2  5324  co01  5326  relcoi1  5340  cnviin  5351  iota4an  5379  fnopab  5511  mpt0  5514  fnmpti  5515  f1cnvcnv  5589  f1ovi  5656  fvco4i  5742  fmpti  5833  fvsnun2  5870  funiunfv  5936  oprabss  6100  relmptopab  6233  2nd0  6295  f1stres  6309  f2ndres  6310  relmpt2opab  6370  df1st2  6374  df2nd2  6375  fsplit  6392  reldmtpos  6425  dftpos4  6436  tpostpos  6437  tpos0  6447  smo0  6558  tfrlem14  6590  tfrlem16  6592  rdgsucg  6619  rdglimg  6621  frfnom  6630  oawordeulem  6735  uniixp  7023  dfdom2  7071  ssdomg  7091  2dom  7117  xpcomf1o  7135  sbthlem5  7159  pwdom  7197  map2xp  7215  limensuci  7221  fiint  7321  fidomdm  7326  pwfilem  7338  mptfi  7343  fisn  7369  dffi3  7373  ordtypelem6  7427  ordtypelem7  7428  wemaplem2  7451  wdompwdom  7481  harwdom  7493  suc11reg  7509  zfinf  7529  axinf2  7530  noinfep  7549  cantnfvalf  7555  cantnflt  7562  cantnf0  7565  cantnf  7584  tz9.1c  7601  tc2  7616  r111  7636  r1tr2  7638  r1ordg  7639  r1sssuc  7644  r1val1  7647  tz9.13  7652  r1elssi  7666  pwwf  7668  rankopb  7713  rankeq0b  7721  ranksuc  7726  rankxplim  7738  rankxplim3  7740  rankxpsuc  7741  cp  7750  karden  7754  card0  7780  cardlim  7794  cardom  7808  pm54.43lem  7821  infxpenlem  7830  alephsuc2  7896  alephgeom  7898  alephprc  7915  unialeph  7917  dfac4  7938  dfacacn  7956  cda1dif  7991  pm110.643  7992  infcda1  8008  ackbij1lem13  8047  ackbij2  8058  cf0  8066  cfsuc  8072  cfom  8079  cfslb2n  8083  ominf4  8127  fin23lem17  8153  fin23lem28  8155  fin23lem30  8157  fin23lem31  8158  fin23lem40  8166  isfin1-3  8201  dfacfin7  8214  fin1a2lem6  8220  itunitc1  8235  axcc3  8253  dcomex  8262  axdc2lem  8263  axcclem  8272  zfac  8275  ac3  8277  ackm  8280  axac2  8281  axac  8282  axaci  8283  cardeqv  8284  numth2  8286  numth  8287  brdom3  8341  fin71ac  8346  cardf  8360  aleph1  8381  cfpwsdom  8394  smobeth  8396  zfcndrep  8424  zfcndpow  8426  zfcndac  8429  canthp1lem2  8463  gch2  8489  wunex3  8551  tskpr  8580  inar1  8585  rankcf  8587  tskcard  8591  tskuni  8593  grothpw  8636  axgroth4  8642  grothprim  8644  inaprc  8646  dmaddpi  8702  dmmulpi  8703  1lt2pi  8717  addpqf  8756  mulpqf  8758  1lt2nq  8785  supsrlem  8921  renepnf  9067  renemnf  9068  ssxr  9080  ltxrlt  9081  subf  9241  negne0i  9309  negdii  9318  ine0  9403  mulnzcnopr  9602  recgt0ii  9850  lbinfm  9895  infmsup  9920  infmrgelb  9922  infmrlb  9923  inelr  9924  halflt1  10123  nn0ssz  10236  zeo  10289  numlt  10335  numltc  10336  uzf  10425  uzinfmi  10489  xrltnr  10654  pnfnlt  10659  nltmnf  10660  xaddf  10744  xsubge0  10774  xmulf  10785  infmxrcl  10829  infmxrlb  10846  infmxrgelb  10847  xrinfm0  10849  ixxf  10860  ixxssxr  10862  iooval2  10883  ioof  10936  unirnioo  10938  dfioo2  10939  fzval2  10980  fzf  10981  fz10  11009  4fvwrd4  11053  fzof  11069  fzo0  11091  injresinjlem  11128  om2uzoi  11224  faclbnd4lem1  11513  hashkf  11549  hashgval  11550  hashinf  11552  hashclb  11570  hasheq0  11573  hashnn0n0nn  11593  hashbclem  11630  wrdexg  11668  rev0  11725  f1oun2prg  11793  sqr2gt1lt2  12009  limsupgord  12195  limsupval  12197  fclim  12276  fsumrelem  12515  ackbijnn  12536  incexclem  12545  incexc  12546  arisum2  12569  georeclim  12578  geoisumr  12584  0.999...  12587  geoihalfsum  12588  ege2le3  12621  sin0  12679  ef01bndlem  12714  cos2bnd  12718  cos01gt0  12721  sincos2sgn  12724  sin4lt0  12725  egt2lt3  12734  rpnnen2lem3  12745  rpnnen2lem9  12751  rexpen  12756  cnso  12775  nthruc  12779  dvdslelem  12823  divalglem1  12843  divalglem5  12846  divalglem6  12847  divalglem10  12851  bitsfzolem  12875  bitsfzo  12876  0bits  12880  bitsinv1lem  12882  sadcf  12894  sadcadd  12899  bitsshft  12916  smupf  12919  gcdf  12948  eucalgf  13003  isprm3  13017  2prm  13024  dfphi2  13092  odzval  13106  pcgcd1  13179  pc2dvds  13181  pockthi  13204  prmreclem2  13214  prmrec  13219  vdwapf  13269  vdwap0  13273  vdwlem6  13283  ramval  13305  ramcl2lem  13306  ramtcl2  13308  karatsuba  13349  1259lem5  13383  2503lem3  13387  4001lem4  13392  structcnvcnv  13409  structfn  13411  strlemor1  13485  strleun  13488  prdsval  13607  prdsds  13615  imasdsfn  13669  imasdsval  13670  imasvscafn  13691  xpsc0  13714  xpsc1  13715  xpsfrnel2  13719  xpsff1o  13722  sscpwex  13944  wunfunc  14025  wunnat  14082  eldmcoa  14149  coapm  14155  setcepi  14172  catcfuccl  14193  catcxpccl  14233  yonedainv  14307  plusffval  14631  grpinvfvi  14775  mulgfvi  14823  odval  15101  odf  15104  odhash3  15139  gexval  15141  sylow3lem2  15191  oppglsm  15205  efgmf  15274  efgval  15278  efgsf  15290  0frgp  15340  gsumzaddlem  15455  dmdprd  15488  dprdval  15490  invrfval  15707  drngui  15770  scaffval  15897  lssintcl  15969  mplsubrglem  16431  opsrtoslem2  16474  cnfld0  16650  cnfld1  16651  cnfldsub  16654  xrsds  16666  xrsdsreclblem  16669  ipffval  16804  ocv1  16831  eltpsi  16936  fctop  16993  cctop  16995  ppttop  16996  epttop  16998  leordtvallem1  17198  leordtvallem2  17199  iccordt  17202  pnfnei  17208  mnfnei  17209  iscnp2  17227  discmp  17385  concompcld  17420  1stcrestlem  17438  2ndcdisj  17442  topnlly  17477  disllycmp  17484  dis1stc  17485  txuni2  17520  xkotf  17540  dfac14lem  17572  prdstps  17584  txindis  17589  tx1stc  17605  xkohaus  17608  xkoptsub  17609  cnmpt1st  17623  cnmpt2nd  17624  ptcmpfi  17768  filcon  17838  trfil1  17841  fin1aufil  17887  tgpconcompeqg  18064  tgpconcomp  18065  tsmsres  18096  trust  18182  met1stc  18443  dscmet  18493  nmoval  18622  retopon  18670  cnfldtopon  18690  xrsxmet  18713  xrsmopn  18716  metdsval  18750  iimulcn  18836  icopnfhmeo  18841  iccpnfhmeo  18843  xrhmeo  18844  xrhmph  18845  cnheiborlem  18852  lebnumii  18864  ishtpy  18870  htpycc  18878  pco1  18913  pcohtpylem  18917  pcopt  18920  pcopt2  18921  pcoass  18922  pcorevlem  18924  cfilresi  19121  ovolval  19239  ovolf  19247  ovoliunlem3  19269  ovolicc1  19281  ovolicc2  19287  volf  19294  ioorf  19334  dyadf  19352  dyadmbl  19361  vitalilem4  19372  vitalilem5  19373  vitali  19374  mbfimaopnlem  19416  mbflimsup  19427  0plef  19433  i1fima  19439  i1fima2  19440  i1fd  19442  i1f0rn  19443  itg1ge0  19447  itg10  19449  i1f1lem  19450  i1fadd  19456  i1fmul  19457  i1fmulc  19464  mbfi1fseqlem5  19480  itg2addlem  19519  reldv  19626  dvbsss  19658  dvef  19733  dvlt0  19758  lhop1lem  19766  deg1fvi  19877  deg1nn0clb  19882  plypf1  20000  coeeulem  20012  coeeu  20013  vieta1lem2  20097  elqaalem1  20105  elqaalem3  20107  aannenlem3  20116  aalioulem2  20119  aalioulem3  20120  dvradcnv  20206  pserulm  20207  pserdvlem2  20213  abelthlem6  20221  sinhalfpilem  20243  sincos4thpi  20290  tan4thpi  20291  sincos6thpi  20292  pige3  20294  coseq1  20299  resinf1o  20307  tanord1  20308  tanregt0  20310  relogrn  20328  dfrelog  20332  logneg  20351  logltb  20363  logcn  20407  logf1o2  20410  dvlog  20411  efopnlem2  20417  efopn  20418  logccv  20423  dvsqr  20497  cxpcn3  20501  angpined  20540  1cubr  20551  atanre  20594  asinsin  20601  asin1  20603  reasinsin  20605  atan0  20617  atanbnd  20635  atan1  20637  log2cnv  20653  log2ublem3  20657  log2ub  20658  birthday  20662  amgmlem  20697  emcllem5  20707  emgt0  20714  harmonicbnd3  20715  ftalem3  20726  basellem4  20735  sgmf  20797  ppi1  20816  cht1  20817  vma1  20818  ppiltx  20829  sqff1o  20834  ppiublem1  20855  ppiublem2  20856  ppiub  20857  chtub  20865  dchreq  20911  bposlem7  20943  bposlem8  20944  bposlem9  20945  lgsdir2lem2  20977  lgsdir2lem3  20978  chebbnd1  21035  chto1ub  21039  chpo1ubb  21044  pntibndlem1  21152  umgrafi  21226  usgraedgprv  21265  usgraexmpl  21288  usgrafilem1  21293  wlkntrllem1  21415  wlkntrllem2  21416  wlkntrllem5  21419  0pth  21426  spthispth  21429  2trllem1  21444  2pthon  21452  2pthon3v  21454  redwlk  21456  constr3trllem3  21489  constr3pthlem3  21494  4cycl4dv  21504  konigsberg  21559  ex-dif  21581  ex-un  21582  ex-in  21583  ex-fl  21605  avril1  21607  ginvsn  21787  cnid  21789  mulid  21794  rngosn3  21864  vcoprnelem  21907  vcoprne  21908  vcex  21909  cnnvm  22024  ipasslem8  22188  ipasslem10  22190  hvsubf  22368  normlem1  22462  normlem6  22467  normlem7  22468  norm-ii-i  22489  norm3adifii  22500  hilid  22513  hlimf  22590  norm1exi  22602  hhssabloi  22612  hhssnv  22614  hhshsslem1  22617  shincli  22714  shsval2i  22739  shs0i  22801  chj0i  22807  chm1i  22808  chincli  22812  chdmm1i  22829  shjshsi  22844  chsup0  22900  h1de2bi  22906  spansnpji  22930  cmcmlem  22943  cmcmii  22949  cmcm2ii  22950  cmcm3ii  22951  pjidmi  23025  pjssmii  23033  pj0i  23045  pjocini  23050  mayetes3i  23082  df0op2  23105  hoaddcomi  23125  hoaddassi  23129  hocadddiri  23132  hocsubdiri  23133  hoaddid1i  23139  ho0coi  23141  hoid1i  23142  hoid1ri  23143  hodseqi  23147  honegsubi  23149  adj1o  23247  hoddii  23342  lnopunilem1  23363  lnopunilem2  23364  nmcopexi  23380  nmcopex  23382  nmcoplb  23383  nmcfnexi  23404  nmcfnex  23406  nmcfnlb  23407  adjbd1o  23438  adjcoi  23453  nmopcoadji  23454  opsqrlem6  23498  pjsdii  23508  pjddii  23509  pjidmcoi  23530  pjtoi  23532  pjin1i  23545  pjclem1  23548  stji1i  23595  largei  23620  reuxfr3d  23822  iuninc  23857  rinvf1o  23887  suppss2f  23894  xppreima  23903  ofoprabco  23923  funcnvmptOLD  23925  gtiso  23931  df1stres  23934  df2ndres  23935  snct  23946  dmct  23949  hashresfn  23996  ressplusf  24024  xrge0base  24038  xrge00  24039  xrge0neqmnf  24043  unicls  24107  sqsscirc1  24112  mhmhmeotmd  24119  rmulccn  24120  raddcn  24121  xrge0iifiso  24127  xrge0iifhmeo  24128  lmxrge0  24143  qqh0  24169  qqh1  24170  qqhre  24184  rrhre  24185  rnlogblem  24197  log2le1  24205  ind1a  24216  esumnul  24241  esum0  24242  esumsn  24254  esumpfinvallem  24262  esumpfinvalf  24264  esumpcvgval  24266  sigaclfu2  24302  dmsigagen  24325  imambfm  24408  mbfmvolf  24412  br2base  24415  probdif  24459  0rrv  24490  coinfliplem  24517  coinflipprob  24518  coinfliprv  24521  ballotlem2  24527  ballotlem4  24537  ballotlem5  24538  ballotlemi  24539  ballotlemiex  24540  ballotlemi1  24541  ballotlemii  24542  ballotlemsup  24543  ballotlemimin  24544  ballotlem1c  24546  ballotlemfrcn0  24568  ballotlemirc  24570  ballotlem7  24574  ballotth  24576  subfacf  24642  subfacp1lem1  24646  subfacp1lem5  24651  subfacp1lem6  24652  subfacval3  24656  erdszelem2  24659  erdszelem9  24666  erdszelem11  24668  kur14lem4  24676  iooscon  24715  iccllyscon  24718  ghomgrpilem1  24877  ghomgrpilem2  24878  circum  24892  axextprim  24931  axrepprim  24932  axunprim  24933  axinfprim  24936  axacprim  24937  inffz  24981  fz0n  24983  risefall0lem  25112  setinds  25160  dfon2lem2  25166  dfon2lem4  25168  dfrdg2  25178  axextdfeq  25180  poseq  25279  wfrlem4  25285  frrlem4  25310  sltval2  25336  nosgnn0  25338  sltintdifex  25343  sltres  25344  sltsolem1  25348  bdayfo  25355  symdifV  25395  fobigcup  25466  snelsingles  25487  fullfunfnv  25511  fullfunfv  25512  dfrdg4  25515  rankaltopb  25540  axlowdimlem4  25600  axlowdimlem13  25609  axlowdimlem16  25612  axlowdim1  25614  axlowdim  25616  linedegen  25793  rank0  25827  rankeq1o  25828  hfuni  25841  nabi1i  25857  nabi2i  25858  limsucncmpi  25911  ovoliunnfl  25955  voliunnfl  25957  itg2addnclem  25959  itg2addnclem2  25960  dvreasin  25982  areacirclem2  25984  areacirclem3  25985  gtinf  26015  fneer  26061  neibastop1  26081  opelopab3  26111  fdc  26142  cntotbnd  26198  heiborlem6  26218  rrnval  26229  reheibor  26241  prter2  26423  diophrw  26510  0dioph  26530  rabren3dioph  26569  rencldnfilem  26574  pellexlem6  26590  pellex  26591  pellfundval  26636  frmx  26669  frmy  26670  jm2.23  26760  jm2.27dlem3  26775  axac10  26797  pw2f1ocnv  26801  wepwsolem  26809  kelac2lem  26833  lmhmlnmsplit  26856  dsmmbas2  26874  pwfi2f1o  26931  frlmpwfi  26933  dgraaval  27020  dgraaf  27023  symgsssg  27079  symgfisg  27080  psgnunilem5  27088  psgnghm  27108  seff  27209  expgrowthi  27221  expgrowth  27223  refsum2cnlem1  27378  infrglb  27392  dvcosre  27411  stoweidlem1  27420  stoweidlem7  27426  stoweidlem26  27445  stoweidlem34  27453  stoweidlem44  27463  stoweid  27482  stirlinglem5  27497  stirlinglem6  27498  axorbtnotaiffb  27541  axorbciffatcxorb  27543  abnotbtaxb  27554  frgrawopreg2  27805  ee233  27947  a9e2nd  27990  in1  28005  dfvd2ani  28018  dfvd2i  28020  dfvd3i  28027  dfvd3ani  28030  e0bi  28231  uun2221  28268  uun2221p1  28269  uun2221p2  28270  en3lpVD  28300  relopabVD  28356  a9e2ndVD  28363  a9e2ndALT  28386  bnj521  28444  bnj1098  28494  bnj1109  28497  bnj1131  28498  bnj1533  28563  bnj151  28588  bnj580  28624  bnj852  28632  bnj864  28633  bnj865  28634  bnj978  28660  bnj1021  28675  bnj907  28676  bnj1093  28689  bnj1145  28702  bnj1172  28710  bnj1174  28712  bnj1176  28714  bnj1186  28716  sbcoNEW7  28919  sbidmNEW7  28921  sbcomOLD7  29073  sb9iOLD7  29076  mapdunirnN  31767
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