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

Theorem mpbi 213
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-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 199 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190
This theorem is referenced by:  pm5.74i  253  notbii  302  pm5.19  366  ori  381  imori  419  pm4.71i  642  pm4.71ri  643  pm5.32i  647  pm3.24  898  pm5.16  906  biluk  949  4exmid  956  dn1  983  3ori  1337  trubifalOLD  1494  cadan  1523  nic-dfim  1563  nic-dfneg  1564  nic-mp  1565  nic-mpALT  1566  tbw-negdf  1593  rb-imdf  1644  mpgbi  1683  19.35i  1752  19.36iv  1832  19.37iv  1838  19.36i  2056  ax6  2106  sbie  2248  axi12  2440  bm1.1  2447  eqcomi  2471  eqtri  2484  eleqtri  2538  neii  2637  necomi  2690  neeqtri  2708  neli  2738  nrex  2854  rexlimi  2881  rexlimiv  2885  isseti  3063  vtocl2  3114  vtocl3  3115  eueq1  3223  euxfr2  3235  cdeqri  3265  sseqtri  3476  3sstr3i  3482  pssn2lp  3546  equncomi  3592  unssi  3621  ssini  3667  unabs  3685  inabs  3686  dfin4  3695  npss0  3815  difid  3847  disjdif  3851  difin0  3852  snid  4008  iinrab2  4355  symdifv  4370  rintn0  4388  breqtri  4442  axsep  4540  bm1.3ii  4544  ax6vsep  4545  zfnuleu  4546  notzfaus  4595  zfpow  4599  dtru  4611  reusv2lem4  4624  reuxfr2d  4640  dtruALT  4649  dtruALT2  4661  op1stb  4689  copsexg  4704  uniop  4721  pwundif  4763  rn0  5108  dmresi  5182  issref  5235  somincom  5256  cnvcnv  5311  rescnvcnv  5321  cnvcnvres  5322  cnvsn  5342  cocnvcnv2  5370  cores2  5371  co01  5373  relcoi1OLD  5388  cnviin  5396  onunisuci  5559  iota4an  5588  fnopab  5728  mpt0  5731  fnmpti  5732  f1cnvcnv  5814  f1ovi  5878  eliman0  5921  fvco4i  5971  fmpti  6073  fvsnun2  6129  funiunfv  6183  oprabss  6414  relmptopab  6549  zfun  6616  tfinds2  6722  omon  6735  2nd0  6832  f1stres  6847  f2ndres  6848  relmpt2opab  6910  df1st2  6914  df2nd2  6915  fsplit  6933  reldmtpos  7012  dftpos4  7023  tpostpos  7024  tpos0  7034  wfrlem4  7070  smo0  7108  tfrlem14  7140  tfrlem16  7142  rdgsucg  7172  rdglimg  7174  frfnom  7183  oawordeulem  7286  uniixp  7576  dfdom2  7626  ssdomg  7646  xpcomf1o  7692  sbthlem5  7717  pwdom  7755  limensuci  7779  fiint  7879  fidomdm  7884  pwfilem  7899  mptfi  7904  fisn  7972  dffi3  7976  ordtypelem6  8069  ordtypelem7  8070  wemaplem2  8093  wdompwdom  8124  harwdom  8136  suc11reg  8155  zfinf  8175  axinf2  8176  noinfep  8196  cantnfvalf  8201  cantnflt  8208  cantnf0  8211  cantnf  8229  tz9.1c  8245  tc2  8257  r111  8277  r1tr2  8279  r1ordg  8280  r1sssuc  8285  r1val1  8288  tz9.13  8293  r1elssi  8307  pwwf  8309  rankopb  8354  rankeq0b  8362  ranksuc  8367  rankmapu  8380  rankxplim  8381  rankxplim3  8383  rankxpsuc  8384  cp  8393  karden  8397  card0  8423  cardlim  8437  cardom  8451  infxpenlem  8475  alephsuc2  8542  alephgeom  8544  unialeph  8563  dfac4  8584  dfacacn  8602  cda1dif  8637  pm110.643  8638  infcda1  8654  ackbij1lem13  8693  ackbij2  8704  cf0  8712  cfsuc  8718  cfom  8725  cfslb2n  8729  ominf4  8773  fin23lem17  8799  fin23lem28  8801  fin23lem30  8803  fin23lem31  8804  fin23lem40  8812  isfin1-3  8847  dfacfin7  8860  fin1a2lem6  8866  itunitc1  8881  axcc3  8899  dcomex  8908  axdc2lem  8909  axcclem  8918  zfac  8921  ac3  8923  ackm  8926  axac2  8927  axac  8928  axaci  8929  cardeqv  8930  numth2  8932  numth  8933  brdom3  8987  fin71ac  8992  cardf  9006  aleph1  9027  cfpwsdom  9040  smobeth  9042  zfcndrep  9070  zfcndpow  9072  zfcndac  9075  gch2  9131  wunex3  9197  tskpr  9226  inar1  9231  rankcf  9233  tskcard  9237  tskuni  9239  grothpw  9282  axgroth4  9288  grothprim  9290  inaprc  9292  dmaddpi  9346  dmmulpi  9347  1lt2pi  9361  addpqf  9400  mulpqf  9402  1lt2nq  9429  supsrlem  9566  ssxr  9734  gtso  9746  subf  9908  negne0i  9980  negdiiOLD  9990  mulnzcnopr  10291  infrenegsup  10624  infmsupOLD  10625  halflt1  10865  nn0ssz  10992  zeo  11055  numlt  11104  numltc  11105  uzf  11196  uzinfmiOLD  11273  zgt1rpn0n1  11374  xaddf  11551  xsubge0  11581  xmulf  11592  infmxrclOLD  11636  infmxrlbOLD  11658  infmxrgelbOLD  11659  xrinfm0OLD  11661  ixxf  11679  ixxssxr  11681  iooval2  11703  ioof  11766  unirnioo  11768  dfioo2  11769  xrge0neqmnf  11771  fzval2  11822  fzf  11823  0nelfz1  11853  fz10  11855  fzpreddisj  11880  4fvwrd4  11946  fzof  11954  fzo0  11979  om2uzoi  12207  faclbnd4lem1  12516  hashkf  12555  hashgval  12556  hashinf  12558  hashresfn  12561  hashnn0n0nn  12608  hashbclem  12654  hashge3el3dif  12681  wrdexg  12721  rev0  12912  f1oun2prg  13054  trclublem  13114  sqrt2gt1lt2  13393  limsupgord  13583  limsupvalOLD  13587  fclim  13672  fsumrelem  13922  ackbijnn  13941  incexclem  13949  incexc  13950  arisum2  13974  georeclim  13983  geoisumr  13989  0.999...  13992  geoihalfsum  13993  risefall0lem  14134  ege2le3  14199  sin0  14258  ef01bndlem  14293  cos2bnd  14297  cos01gt0  14300  sincos2sgn  14303  sin4lt0  14304  rpnnen2lem3  14324  rpnnen2lem9  14330  rexpen  14335  cnso  14354  dvdslelem  14404  n2dvds1  14409  divalglem1  14427  divalglem5OLD  14431  divalglem5  14432  divalglem6  14433  divalglem10  14438  0bits  14468  sadcf  14482  sadcadd  14487  bitsshft  14504  smupf  14507  gcdf  14538  eucalgf  14597  2prm  14695  dfphi2  14777  pockthi  14906  prmreclem2  14916  prmrec  14921  vdwapf  14977  vdwap0  14981  vdwlem6  14991  ramvalOLD  15016  ramcl2lemOLD  15018  karatsuba  15111  1259lem5  15161  2503lem3  15165  4001lem4  15170  structcnvcnv  15187  structfn  15189  strlemor1  15272  strleun  15275  prdsval  15408  prdsds  15417  imasdsfnOLD  15482  imasdsvalOLD  15483  imasvscafn  15498  xpsc0  15521  xpsc1  15522  xpsff1o  15529  sscpwex  15775  wunfunc  15859  wunnat  15916  eldmcoa  16015  coapm  16021  catcfuccl  16059  catcxpccl  16147  yonedainv  16221  plusffval  16548  grpinvfvi  16762  mulgfvi  16817  symgsssg  17163  symgfisg  17164  psgnunilem5  17190  sylow3lem2  17335  oppglsm  17349  efgmf  17418  efgval  17422  efgsf  17434  0frgp  17484  gsumzaddlem  17609  dmdprd  17685  dprdval  17690  invrfval  17956  drngui  18036  scaffval  18164  lssintcl  18242  mplsubrglem  18718  opsrtoslem2  18763  cnfld0  19047  cnfld1  19048  cnfldsub  19051  xrsds  19066  psgnghm  19203  zrhpsgnmhm  19207  recrng  19244  ipffval  19270  ocv1  19297  dsmmbas2  19355  mdetralt  19688  maducoeval2  19720  eltpsi  20016  unitg  20037  fctop  20074  cctop  20076  ppttop  20077  epttop  20079  leordtvallem1  20281  leordtvallem2  20282  iccordt  20285  iscnp2  20310  discmp  20468  concompcld  20504  1stcrestlem  20522  2ndcdisj  20526  topnlly  20561  disllycmp  20568  dis1stc  20569  txuni2  20635  xkotf  20655  dfac14lem  20687  prdstps  20699  txindis  20704  tx1stc  20720  xkohaus  20723  xkoptsub  20724  cnmpt1st  20738  cnmpt2nd  20739  ptcmpfi  20883  filcon  20953  trfil1  20956  fin1aufil  21002  tgpconcompeqg  21181  tgpconcomp  21182  tsmsres  21213  trust  21299  met1stc  21591  dscmet  21642  nmovalOLD  21794  retopon  21839  cnfldtopon  21858  xrsxmet  21882  xrsmopn  21885  metdsvalOLD  21934  iimulcn  22021  icopnfhmeo  22026  iccpnfhmeo  22028  xrhmeo  22029  cnheiborlem  22037  lebnumii  22052  ishtpy  22058  htpycc  22066  pco1  22101  pcohtpylem  22105  pcopt  22108  pcopt2  22109  pcoass  22110  pcorevlem  22112  cfilresi  22320  rrxcph  22406  ovolvalOLD  22482  ovoliunlem3  22512  ovolicc1  22524  ovolicc2  22531  volf  22538  ioorf  22581  ioorfOLD  22586  dyadf  22605  dyadmbl  22614  vitalilem5  22626  vitali  22627  mbfimaopnlem  22667  mbflimsup  22679  mbflimsupOLD  22680  0plef  22686  i1fima  22692  i1fima2  22693  i1fd  22695  itg1ge0  22700  itg10  22702  i1f1lem  22703  i1fadd  22709  i1fmul  22710  i1fmulc  22717  mbfi1fseqlem5  22733  itg2addlem  22772  reldv  22881  dvbsss  22913  dvef  22988  lhop1lem  23021  deg1fvi  23090  plypf1  23222  coeeulem  23234  coeeu  23235  vieta1lem2  23320  aannenlem3  23342  aalioulem3  23346  dvradcnv  23432  pserulm  23433  pserdvlem2  23439  abelthlem6  23447  sinhalfpilem  23474  sincos4thpi  23524  tan4thpi  23525  sincos6thpi  23526  pige3  23528  resinf1o  23541  tanord1  23542  tanregt0  23544  efabl  23555  relogrn  23567  dfrelog  23571  logneg  23593  logltb  23605  logcn  23648  logf1o2  23651  dvlog  23652  efopnlem2  23658  efopn  23659  logccv  23664  dvsqrt  23738  dvcnsqrt  23740  cxpcn3  23744  logblog  23785  angpined  23812  1cubr  23824  asinsin  23874  asin1  23876  reasinsin  23878  atan0  23890  atanbnd  23908  atan1  23910  log2cnv  23926  log2ublem3  23930  log2ub  23931  log2le1  23932  birthday  23936  amgmlem  23971  emcllem5  23981  emgt0  23988  harmonicbnd3  23989  ftalem3  24055  basellem4  24066  sgmf  24128  ppi1  24147  cht1  24148  vma1  24149  ppiltx  24160  sqff1o  24165  ppiublem1  24186  ppiublem2  24187  ppiub  24188  chtub  24196  dchreq  24242  bposlem7  24274  bposlem8  24275  bposlem9  24276  lgsdir2lem2  24308  lgsdir2lem3  24309  chebbnd1  24366  chto1ub  24370  chpo1ubb  24375  pntibndlem1  24483  tgldimor  24602  tglnfn  24648  axlowdimlem4  25031  axlowdimlem16  25043  axlowdim  25047  umgrafi  25105  usgraexmplef  25184  usgraexmplc  25188  usgrafilem1  25195  2trllemA  25336  wlkntrllem1  25345  wlkntrllem3  25347  0pth  25356  spthispth  25359  2pthon  25388  2pthon3v  25390  constr3trllem3  25436  constr3pthlem3  25441  konigsberg  25771  frgrawopreg2  25835  ex-dif  25929  ex-un  25930  ex-in  25931  ex-fl  25953  avril1  25956  ginvsn  26133  cnid  26135  mulid  26140  rngosn3  26210  vcoprnelem  26253  vcex  26255  cnnvm  26370  ipasslem8  26534  ipasslem10  26536  hvsubf  26724  normlem1  26819  normlem6  26824  normlem7  26825  norm-ii-i  26846  norm3adifii  26857  hilid  26870  hlimf  26946  hhssabloi  26969  hhssnv  26971  hhshsslem1  26974  shincli  27071  shsval2i  27096  shs0i  27158  chj0i  27164  chm1i  27165  chincli  27169  chdmm1i  27186  shjshsi  27201  chsup0  27257  h1de2bi  27263  spansnpji  27287  cmcmlem  27300  cmcmii  27306  cmcm2ii  27307  cmcm3ii  27308  pjidmi  27382  pjssmii  27390  pj0i  27402  pjocini  27407  mayetes3i  27438  df0op2  27461  hoaddcomi  27481  hoaddassi  27485  hocadddiri  27488  hocsubdiri  27489  hoaddid1i  27495  ho0coi  27497  hoid1i  27498  hoid1ri  27499  hodseqi  27503  honegsubi  27505  adj1o  27603  hoddii  27698  lnopunilem1  27719  lnopunilem2  27720  nmcopexi  27736  nmcopex  27738  nmcoplb  27739  nmcfnexi  27760  nmcfnex  27762  nmcfnlb  27763  adjbd1o  27794  adjcoi  27809  nmopcoadji  27810  opsqrlem6  27854  pjsdii  27864  pjddii  27865  pjidmcoi  27886  pjtoi  27888  pjin1i  27901  pjclem1  27904  stji1i  27951  reuxfr3d  28181  inindif  28206  iuninc  28230  fnresin  28281  rinvf1o  28283  suppss2fOLD  28290  suppss2f  28291  xppreima  28301  ofoprabco  28319  funcnvmptOLD  28322  gtiso  28333  df1stres  28336  df2ndres  28337  snct  28347  dmct  28350  padct  28359  ffsrn  28366  fpwrelmapffs  28371  xrge0infssdOLD  28395  infxrge0lbOLD  28399  infxrge0glbOLD  28401  infxrge0gelbOLD  28403  nnindf  28434  nn0min  28436  ressplusf  28463  xrsclat  28494  xrge0base  28499  xrge00  28500  xrnarchi  28552  xrge0slmod  28658  locfinreflem  28718  locfinref  28719  unicls  28760  sqsscirc1  28765  mhmhmeotmd  28784  rmulccn  28785  raddcn  28786  xrge0iifiso  28792  xrge0iifhmeo  28793  lmxrge0  28809  cnzh  28825  rezh  28826  qqh0  28839  qqh1  28840  qqhre  28875  rrhre  28876  esumnul  28920  esum0  28921  esumsnf  28936  esumpfinvallem  28946  esumpfinvalf  28948  esumpcvgval  28950  esumcvgsum  28960  esumsup  28961  esumcvgre  28963  sigaclfu2  28994  dmsigagen  29017  ldgenpisyslem1  29036  ddemeas  29109  imambfm  29134  mbfmvolf  29138  br2base  29141  omsfvalOLD  29172  omsfOLD  29174  omssubadd  29178  oms0OLD  29179  omssubaddlemOLD  29181  omssubaddOLD  29182  carsgclctunlem3  29202  sibfof  29223  sitg0  29229  eulerpartlemt  29254  eulerpartgbij  29255  0rrv  29334  coinfliplem  29361  coinflipprob  29362  coinfliprv  29365  ballotlem2  29371  ballotlem4  29381  ballotlem5  29382  ballotlemi1  29385  ballotlem7  29418  ballotth  29420  ballotlemi1OLD  29423  ballotlem7OLD  29456  ballotthOLD  29458  signsplypnf  29489  signsply0  29490  signsw0g  29495  signswch  29500  signsvf0  29519  bnj521  29595  bnj1098  29645  bnj1109  29648  bnj1131  29649  bnj1533  29713  bnj151  29738  bnj580  29774  bnj852  29782  bnj864  29783  bnj865  29784  bnj978  29810  bnj1021  29825  bnj907  29826  bnj1093  29839  bnj1145  29852  bnj1172  29860  bnj1174  29862  bnj1176  29864  bnj1186  29866  subfacf  29948  subfacp1lem1  29952  subfacp1lem5  29957  subfacp1lem6  29958  subfacval3  29962  erdszelem2  29965  kur14lem4  29982  iooscon  30020  iccllyscon  30023  msrfo  30234  mthmpps  30270  problem5  30351  quad3  30352  ghomgrpilem1  30353  ghomgrpilem2  30354  circum  30368  axextprim  30378  axrepprim  30379  axunprim  30380  axinfprim  30383  axacprim  30384  inffz  30413  logi  30420  bcneg1  30422  setinds  30474  dfon2lem2  30480  dfon2lem4  30482  axextdfeq  30494  poseq  30541  frrlem4  30567  nosgnn0  30595  sltsolem1  30607  bdayfo  30614  fobigcup  30717  snelsingles  30739  fullfunfnv  30763  fullfunfv  30764  rankaltopb  30796  rank0  30987  rankeq1o  30988  hfuni  31001  fneer  31059  neibastop1  31065  nabi1i  31102  nabi2i  31103  limsucncmpi  31155  bj-consensusALT  31203  bj-nfxfr  31264  bj-axsep  31454  bj-zfpow  31456  bj-dtru  31458  bj-sbieOLD  31491  bj-sbidmOLD  31492  bj-n0i  31586  bj-snsetex  31603  bj-tagss  31620  bj-2upln0  31663  bj-2upln1upl  31664  bj-nuliota  31669  bj-elid  31686  bj-pinftyccb  31709  bj-minftyccb  31713  bj-pinftynminfty  31715  f1omptsnlem  31784  mptsnunlem  31786  topdifinffinlem  31796  relowlpssretop  31813  1oequni2o  31817  imadifss  31974  tan2h  31983  poimirlem3  31989  poimirlem9  31995  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem22  32008  poimirlem30  32016  mblfinlem1  32023  mblfinlem2  32024  ovoliunnfl  32028  voliunnfl  32030  dvtanlemOLD  32037  itg2addnclem  32039  itg2addnclem2  32040  asindmre  32073  areacirclem1  32078  fdc  32120  cntotbnd  32174  heiborlem6  32194  rrnval  32205  reheibor  32217  prter2  32499  renegclALT  32581  mapdunirnN  35264  rntrclfvOAI  35579  diophrw  35647  rabren3dioph  35704  pellexlem6  35724  pellex  35725  frmx  35807  frmy  35808  jm2.23  35897  jm2.27dlem3  35912  axac10  35934  pw2f1ocnv  35938  kelac2lem  35968  lmhmlnmsplit  35991  pwfi2f1o  36000  frlmpwfi  36002  ifpbiidcor  36164  cnvnonrel  36240  rnnonrel  36243  resnonrel  36244  cononrel1  36246  cononrel2  36247  fvnonrel  36249  cnvcnvintabd  36252  cnvintabd  36255  rclexi  36268  rtrclex  36270  clcnvlem  36276  cnvrcl0  36278  dmtrcl  36280  rntrcl  36281  dfrtrcl5  36282  iunrelexp0  36340  dmtrclfvRP  36368  rntrclfv  36370  corcltrcl  36377  cotrclrcl  36380  0heALT  36425  frege54cor1a  36506  int-rightdistd  36672  int-sqdefd  36673  int-sqgeq0d  36678  seff  36702  expgrowthi  36727  expgrowth  36729  binomcxplemnotnn0  36750  ee233  36921  ax6e2nd  36970  in1  36985  dfvd2ani  36997  dfvd2i  36999  dfvd3i  37006  dfvd3ani  37009  e0bi  37204  uun2221  37241  uun2221p1  37242  uun2221p2  37243  en3lpVD  37282  relopabVD  37339  ax6e2ndVD  37346  ax6e2ndALT  37368  nnf1oxpnn  37526  icof  37557  negpilt0  37565  xrgtso  37643  ioontr  37696  iccdifioo  37701  iccdifprioo  37702  fsummulc1f  37732  fsumiunss  37739  icccncfext  37851  dvcosre  37867  dvsinax  37869  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvmptmulf  37898  dvnmul  37904  dvmptfprodlem  37905  dvnprodlem2  37908  stoweidlem1  37962  stoweidlem26  37987  stoweidlem34  37996  stoweidlem44  38006  stoweid  38026  stirlinglem5  38041  dirkercncflem1  38066  fourierdlem44  38116  fourierdlem56  38127  fourierdlem62  38133  fourierdlem89  38160  fourierdlem91  38162  fourierdlem100  38171  fourierdlem102  38173  fourierdlem103  38174  fourierdlem104  38175  fourierdlem108  38179  fourierdlem112  38183  fourierdlem114  38185  fouriersw  38196  rrndistlt  38260  gsumge0cl  38316  sge0tsms  38325  sge0ltfirpmpt2  38371  ovn0  38495  hoidmv1le  38523  hoidmvle  38529  ovnsubadd2lem  38574  ovolval4lem1  38578  axorbtnotaiffb  38625  axorbciffatcxorb  38627  abnotbtaxb  38638  1nevenALTV  38955  nnsum3primes4  39018  evengpoap3  39029  tgblthelfgott  39043  tgoldbachlt  39044  resisresindm  39147  residfi  39177  hashfxnn0  39231  upgrfi  39326  pthdlem2  39890  0ewlk  39924  0pth-av  39937  ldepslinc  40671  3halfnz  40686  alimp-no-surprise  40889  aacllem  40909
  Copyright terms: Public domain W3C validator