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

Theorem mpbi 208
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 194 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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 185
This theorem is referenced by:  pm5.74i  245  notbii  296  pm5.19  360  ori  375  imori  413  pm4.71i  632  pm4.71ri  633  pm5.32i  637  pm3.24  877  pm5.16  885  biluk  924  4exmid  930  dn1  957  3ori  1279  trubifal  1409  cadan  1434  nic-dfim  1477  nic-dfneg  1478  nic-mp  1479  nic-mpALT  1480  tbw-negdf  1507  rb-imdf  1558  mpgbi  1595  19.35i  1657  19.36i  1902  19.37aiv  1928  ax6  1956  sbie  2107  sbieOLD  2108  sbcoOLD  2114  sbidmOLD  2117  axi12  2428  bm1.1  2434  eqcomi  2464  eqtri  2480  eleqtri  2537  neii  2648  necomi  2718  nesymiOLD  2722  neeqtri  2746  neli  2783  nrex  2914  rexlimi  2930  isseti  3074  vtocl2  3121  vtocl3  3122  eueq1  3229  euxfr2  3241  cdeqri  3270  sseqtri  3486  3sstr3i  3492  pssn2lp  3555  equncomi  3600  unssi  3629  ssini  3671  unabs  3678  inabs  3679  dfin4  3688  npss0  3815  difid  3845  disjdif  3849  difin0  3850  snid  4003  iinrab2  4331  rintn0  4359  breqtri  4413  axsep  4510  bm1.3ii  4514  ax6vsep  4515  zfnuleu  4516  notzfaus  4565  zfpow  4569  dtru  4581  reusv2lem4  4594  reuxfr2d  4613  dtruALT  4622  dtruALT2  4634  op1stb  4660  copsexg  4674  copsexgOLD  4675  uniop  4692  pwundif  4726  onunisuci  4930  relop  5088  rn0  5189  dmresi  5259  issref  5309  somincom  5333  cnvcnv  5388  rescnvcnv  5399  cnvcnvres  5400  cnvsn  5420  cocnvcnv2  5447  cores2  5448  co01  5450  relcoi1  5464  cnviin  5472  iota4an  5498  fnopab  5633  mpt0  5636  fnmpti  5637  f1cnvcnv  5712  f1ovi  5775  eliman0  5818  fvco4i  5868  fmpti  5965  fvsnun2  6013  funiunfv  6064  oprabss  6276  relmptopab  6408  zfun  6473  tfinds2  6574  omon  6587  2nd0  6684  f1stres  6698  f2ndres  6699  relmpt2opab  6755  df1st2  6759  df2nd2  6760  fsplit  6777  reldmtpos  6853  dftpos4  6864  tpostpos  6865  tpos0  6875  smo0  6919  tfrlem14  6950  tfrlem16  6952  rdgsucg  6979  rdglimg  6981  frfnom  6990  oawordeulem  7093  uniixp  7386  dfdom2  7435  ssdomg  7455  xpcomf1o  7500  sbthlem5  7525  pwdom  7563  limensuci  7587  fiint  7689  fidomdm  7694  pwfilem  7706  mptfi  7711  fisn  7778  dffi3  7782  ordtypelem6  7838  ordtypelem7  7839  wemaplem2  7862  wdompwdom  7894  harwdom  7906  suc11reg  7926  zfinf  7946  axinf2  7947  noinfep  7966  cantnfvalf  7974  cantnflt  7981  cantnf0  7984  cantnf  8002  cantnfltOLD  8011  cantnfOLD  8024  tz9.1c  8051  tc2  8063  r111  8083  r1tr2  8085  r1ordg  8086  r1sssuc  8091  r1val1  8094  tz9.13  8099  r1elssi  8113  pwwf  8115  rankopb  8160  rankeq0b  8168  ranksuc  8173  rankmapu  8186  rankxplim  8187  rankxplim3  8189  rankxpsuc  8190  cp  8199  karden  8203  card0  8229  cardlim  8243  cardom  8257  infxpenlem  8281  alephsuc2  8351  alephgeom  8353  unialeph  8372  dfac4  8393  dfacacn  8411  cda1dif  8446  pm110.643  8447  infcda1  8463  ackbij1lem13  8502  ackbij2  8513  cf0  8521  cfsuc  8527  cfom  8534  cfslb2n  8538  ominf4  8582  fin23lem17  8608  fin23lem28  8610  fin23lem30  8612  fin23lem31  8613  fin23lem40  8621  isfin1-3  8656  dfacfin7  8669  fin1a2lem6  8675  itunitc1  8690  axcc3  8708  dcomex  8717  axdc2lem  8718  axcclem  8727  zfac  8730  ac3  8732  ackm  8735  axac2  8736  axac  8737  axaci  8738  cardeqv  8739  numth2  8741  numth  8742  brdom3  8796  fin71ac  8801  cardf  8815  aleph1  8836  cfpwsdom  8849  smobeth  8851  zfcndrep  8882  zfcndpow  8884  zfcndac  8887  gch2  8943  wunex3  9009  tskpr  9038  inar1  9043  rankcf  9045  tskcard  9049  tskuni  9051  grothpw  9094  axgroth4  9100  grothprim  9102  inaprc  9104  dmaddpi  9160  dmmulpi  9161  1lt2pi  9175  addpqf  9214  mulpqf  9216  1lt2nq  9243  supsrlem  9379  ssxr  9545  gtso  9557  subf  9713  negne0i  9784  negdii  9793  mulnzcnopr  10083  infmsup  10409  halflt1  10644  nn0ssz  10768  zeo  10828  numlt  10875  numltc  10876  uzf  10965  uzinfmi  11035  xaddf  11295  xsubge0  11325  xmulf  11336  infmxrcl  11380  infmxrlb  11397  infmxrgelb  11398  xrinfm0  11400  ixxf  11411  ixxssxr  11413  iooval2  11434  ioof  11488  unirnioo  11490  dfioo2  11491  fzval2  11541  fzf  11542  fz10  11571  fzpreddisj  11605  4fvwrd4  11634  fzof  11651  fzo0  11674  fzo0ss1  11680  injresinjlem  11739  om2uzoi  11879  faclbnd4lem1  12170  hashkf  12206  hashgval  12207  hashinf  12209  hashresfn  12212  hashnn0n0nn  12255  hashge3el3dif  12289  hashbclem  12307  wrdexg  12346  rev0  12506  f1oun2prg  12629  sqr2gt1lt2  12866  limsupgord  13052  limsupval  13054  fclim  13133  fsumrelem  13372  ackbijnn  13393  incexclem  13401  incexc  13402  arisum2  13425  georeclim  13434  geoisumr  13440  0.999...  13443  geoihalfsum  13444  ege2le3  13477  sin0  13535  ef01bndlem  13570  cos2bnd  13574  cos01gt0  13577  sincos2sgn  13580  sin4lt0  13581  rpnnen2lem3  13601  rpnnen2lem9  13607  rexpen  13612  cnso  13631  dvdslelem  13679  n2dvds1  13684  divalglem1  13700  divalglem5  13703  divalglem6  13704  divalglem10  13708  0bits  13737  sadcf  13751  sadcadd  13756  bitsshft  13773  smupf  13776  gcdf  13805  eucalgf  13860  isprm3  13874  2prm  13881  dfphi2  13951  reumodprminv  13974  pockthi  14070  prmreclem2  14080  prmrec  14085  vdwapf  14135  vdwap0  14139  vdwlem6  14149  ramval  14171  ramcl2lem  14172  karatsuba  14215  1259lem5  14261  2503lem3  14265  4001lem4  14270  structcnvcnv  14287  structfn  14289  strlemor1  14367  strleun  14370  prdsval  14495  prdsds  14504  imasdsfn  14554  imasdsval  14555  imasvscafn  14577  xpsc0  14600  xpsc1  14601  xpsff1o  14608  sscpwex  14830  wunfunc  14911  wunnat  14968  eldmcoa  15035  coapm  15041  catcfuccl  15079  catcxpccl  15119  yonedainv  15193  plusffval  15529  grpinvfvi  15681  mulgfvi  15733  symgsssg  16075  symgfisg  16076  psgnunilem5  16102  sylow3lem2  16231  oppglsm  16245  efgmf  16314  efgval  16318  efgsf  16330  0frgp  16380  gsumzaddlem  16512  gsumzaddlemOLD  16514  dmdprd  16585  dprdval  16590  dprdvalOLD  16592  invrfval  16871  drngui  16944  scaffval  17072  lssintcl  17151  mplsubrglem  17624  mplsubrglemOLD  17625  opsrtoslem2  17673  cnfld0  17949  cnfld1  17950  cnfldsub  17953  xrsds  17965  psgnghm  18119  zrhpsgnmhm  18123  psgnodpmr  18129  recrng  18160  ipffval  18186  ocv1  18213  dsmmbas2  18271  frlmip  18312  mdetralt  18530  maducoeval2  18562  eltpsi  18667  fctop  18724  cctop  18726  ppttop  18727  epttop  18729  leordtvallem1  18930  leordtvallem2  18931  iccordt  18934  iscnp2  18959  discmp  19117  concompcld  19154  1stcrestlem  19172  2ndcdisj  19176  topnlly  19211  disllycmp  19218  dis1stc  19219  txuni2  19254  xkotf  19274  dfac14lem  19306  prdstps  19318  txindis  19323  tx1stc  19339  xkohaus  19342  xkoptsub  19343  cnmpt1st  19357  cnmpt2nd  19358  ptcmpfi  19502  filcon  19572  trfil1  19575  fin1aufil  19621  tgpconcompeqg  19798  tgpconcomp  19799  tsmsresOLD  19833  tsmsres  19834  trust  19920  met1stc  20212  dscmet  20281  nmoval  20410  retopon  20458  cnfldtopon  20478  xrsxmet  20502  xrsmopn  20505  metdsval  20539  iimulcn  20626  icopnfhmeo  20631  iccpnfhmeo  20633  xrhmeo  20634  cnheiborlem  20642  lebnumii  20654  ishtpy  20660  htpycc  20668  pco1  20703  pcohtpylem  20707  pcopt  20710  pcopt2  20711  pcoass  20712  pcorevlem  20714  cfilresi  20922  rrxip  21010  rrxcph  21012  ovolval  21073  ovolf  21081  ovoliunlem3  21103  ovolicc1  21115  ovolicc2  21121  volf  21128  ioorf  21169  dyadf  21187  dyadmbl  21196  vitalilem5  21208  vitali  21209  mbfimaopnlem  21249  mbflimsup  21260  0plef  21266  i1fima  21272  i1fima2  21273  i1fd  21275  itg1ge0  21280  itg10  21282  i1f1lem  21283  i1fadd  21289  i1fmul  21290  i1fmulc  21297  mbfi1fseqlem5  21313  itg2addlem  21352  reldv  21461  dvbsss  21493  dvef  21568  lhop1lem  21601  deg1fvi  21672  plypf1  21796  coeeulem  21808  coeeu  21809  vieta1lem2  21893  aannenlem3  21912  aalioulem3  21916  dvradcnv  22002  pserulm  22003  pserdvlem2  22009  abelthlem6  22017  sinhalfpilem  22041  sincos4thpi  22091  tan4thpi  22092  sincos6thpi  22093  pige3  22095  resinf1o  22108  tanord1  22109  tanregt0  22111  relogrn  22129  dfrelog  22133  logneg  22152  logltb  22164  logcn  22208  logf1o2  22211  dvlog  22212  efopnlem2  22218  efopn  22219  logccv  22224  dvsqr  22298  cxpcn3  22302  angpined  22341  1cubr  22353  asinsin  22403  asin1  22405  reasinsin  22407  atan0  22419  atanbnd  22437  atan1  22439  log2cnv  22455  log2ublem3  22459  log2ub  22460  birthday  22464  amgmlem  22499  emcllem5  22509  emgt0  22516  harmonicbnd3  22517  ftalem3  22528  basellem4  22537  sgmf  22599  ppi1  22618  cht1  22619  vma1  22620  ppiltx  22631  sqff1o  22636  ppiublem1  22657  ppiublem2  22658  ppiub  22659  chtub  22667  dchreq  22713  bposlem7  22745  bposlem8  22746  bposlem9  22747  lgsdir2lem2  22779  lgsdir2lem3  22780  chebbnd1  22837  chto1ub  22841  chpo1ubb  22846  pntibndlem1  22954  tgldimor  23073  tglnfn  23100  legov  23137  legtrid  23143  axlowdimlem4  23326  axlowdimlem13  23335  axlowdimlem16  23338  axlowdim1  23340  axlowdim  23342  ecgrtg  23364  umgrafi  23391  usgraexmpl  23454  usgrafilem1  23459  2trllemA  23584  wlkntrllem1  23593  wlkntrllem3  23595  0pth  23604  spthispth  23607  2pthon  23636  2pthon3v  23638  redwlk  23640  constr3trllem3  23673  constr3pthlem3  23678  konigsberg  23743  ex-dif  23765  ex-un  23766  ex-in  23767  ex-fl  23789  avril1  23791  ginvsn  23971  cnid  23973  mulid  23978  rngosn3  24048  vcoprnelem  24091  vcoprne  24092  vcex  24093  cnnvm  24208  ipasslem8  24372  ipasslem10  24374  hvsubf  24552  normlem1  24647  normlem6  24652  normlem7  24653  norm-ii-i  24674  norm3adifii  24685  hilid  24698  hlimf  24775  norm1exi  24788  hhssabloi  24798  hhssnv  24800  hhshsslem1  24803  shincli  24900  shsval2i  24925  shs0i  24987  chj0i  24993  chm1i  24994  chincli  24998  chdmm1i  25015  shjshsi  25030  chsup0  25086  h1de2bi  25092  spansnpji  25116  cmcmlem  25129  cmcmii  25135  cmcm2ii  25136  cmcm3ii  25137  pjidmi  25211  pjssmii  25219  pj0i  25231  pjocini  25236  mayetes3i  25268  df0op2  25291  hoaddcomi  25311  hoaddassi  25315  hocadddiri  25318  hocsubdiri  25319  hoaddid1i  25325  ho0coi  25327  hoid1i  25328  hoid1ri  25329  hodseqi  25333  honegsubi  25335  adj1o  25433  hoddii  25528  lnopunilem1  25549  lnopunilem2  25550  nmcopexi  25566  nmcopex  25568  nmcoplb  25569  nmcfnexi  25590  nmcfnex  25592  nmcfnlb  25593  adjbd1o  25624  adjcoi  25639  nmopcoadji  25640  opsqrlem6  25684  pjsdii  25694  pjddii  25695  pjidmcoi  25716  pjtoi  25718  pjin1i  25731  pjclem1  25734  stji1i  25781  largei  25806  spc2ed  25992  reuxfr3d  26008  inindif  26032  iuninc  26045  fnresin  26081  rinvf1o  26083  suppss2f  26088  xppreima  26098  ofoprabco  26116  funcnvmptOLD  26120  gtiso  26130  df1stres  26133  df2ndres  26134  snct  26145  dmct  26148  ffsrn  26163  resf1o  26164  fpwrelmapffs  26168  xrge0infssd  26188  nnindf  26223  nn0min  26224  ressplusf  26245  xrsclat  26275  xrge0base  26280  xrge00  26281  xrge0neqmnf  26286  xrnarchi  26335  orngsqr  26406  xrge0slmod  26446  unicls  26467  sqsscirc1  26472  ordtconlem1  26488  mhmhmeotmd  26491  rmulccn  26492  raddcn  26493  xrge0iifiso  26499  xrge0iifhmeo  26500  lmxrge0  26516  cnzh  26533  rezh  26534  qqh0  26547  qqh1  26548  qqhre  26580  rrhre  26581  rnlogblem  26592  log2le1  26600  ind1a  26611  esumnul  26636  esum0  26637  esumsn  26649  esumpfinvallem  26657  esumpfinvalf  26659  esumpcvgval  26661  sigaclfu2  26698  dmsigagen  26721  ddemeas  26786  imambfm  26811  mbfmvolf  26815  br2base  26818  omsfval  26843  oms0  26844  sibfof  26860  sitg0  26866  eulerpartlemt  26888  eulerpartgbij  26889  fib5  26922  probdif  26937  0rrv  26968  coinfliplem  26995  coinflipprob  26996  coinfliprv  26999  ballotlem2  27005  ballotlem4  27015  ballotlem5  27016  ballotlemi  27017  ballotlemiex  27018  ballotlemi1  27019  ballotlemii  27020  ballotlemsup  27021  ballotlemimin  27022  ballotlemfrcn0  27046  ballotlemirc  27048  ballotlem7  27052  ballotth  27054  signsplypnf  27085  signsply0  27086  signsw0g  27091  signswch  27096  signsvvf  27114  signsvf0  27115  subfacf  27197  subfacp1lem1  27201  subfacp1lem5  27206  subfacp1lem6  27207  subfacval3  27211  erdszelem2  27214  erdszelem9  27221  erdszelem11  27223  kur14lem4  27231  iooscon  27270  iccllyscon  27273  problem5  27436  quad3  27437  ghomgrpilem1  27438  ghomgrpilem2  27439  circum  27453  axextprim  27486  axrepprim  27487  axunprim  27488  axinfprim  27491  axacprim  27492  inffz  27521  risefall0lem  27663  setinds  27725  dfon2lem2  27731  dfon2lem4  27733  dfrdg2  27743  axextdfeq  27745  poseq  27848  wfrlem4  27861  frrlem4  27905  sltval2  27931  nosgnn0  27933  sltintdifex  27938  sltres  27939  sltsolem1  27943  bdayfo  27950  symdifV  27990  fobigcup  28065  snelsingles  28087  fullfunfnv  28111  fullfunfv  28112  dfrdg4  28115  rankaltopb  28144  linedegen  28308  rank0  28342  rankeq1o  28343  hfuni  28356  nabi1i  28372  nabi2i  28373  limsucncmpi  28425  tan2h  28562  heicant  28564  mblfinlem1  28566  mblfinlem2  28567  ovoliunnfl  28571  voliunnfl  28573  dvtanlem  28579  itg2addnclem  28581  itg2addnclem2  28582  dvcnsqr  28616  asindmre  28617  areacirclem1  28622  gtinf  28652  fneer  28698  neibastop1  28718  opelopab3  28748  fdc  28779  cntotbnd  28833  heiborlem6  28853  rrnval  28864  reheibor  28876  impor  29019  prter2  29164  diophrw  29235  0dioph  29255  rabren3dioph  29292  rencldnfilem  29297  pellexlem6  29313  pellex  29314  pellfundval  29359  frmx  29392  frmy  29393  jm2.23  29483  jm2.27dlem3  29498  axac10  29520  pw2f1ocnv  29524  wepwsolem  29532  kelac2lem  29555  lmhmlnmsplit  29578  pwfi2f1o  29589  frlmpwfi  29591  dgraaval  29639  dgraaf  29642  seff  29733  expgrowthi  29745  expgrowth  29747  refsum2cnlem1  29897  infrglb  29909  dvcosre  29926  stoweidlem1  29934  stoweidlem26  29959  stoweidlem34  29967  stoweidlem44  29977  stoweid  29996  stirlinglem5  30011  axorbtnotaiffb  30055  axorbciffatcxorb  30057  abnotbtaxb  30068  resisresindm  30277  wwlktovf  30389  frgrawopreg2  30782  ldepslinc  31158  fvmptnn04if  31303  comraddi  31414  alimp-no-surprise  31433  ee233  31524  ax6e2nd  31567  in1  31584  dfvd2ani  31596  dfvd2i  31598  dfvd3i  31605  dfvd3ani  31608  e0bi  31809  uun2221  31846  uun2221p1  31847  uun2221p2  31848  en3lpVD  31881  relopabVD  31937  ax6e2ndVD  31944  ax6e2ndALT  31966  bnj521  32028  bnj1098  32077  bnj1109  32080  bnj1131  32081  bnj1533  32145  bnj151  32170  bnj580  32206  bnj852  32214  bnj864  32215  bnj865  32216  bnj978  32242  bnj1021  32257  bnj907  32258  bnj1093  32271  bnj1145  32284  bnj1172  32292  bnj1174  32294  bnj1176  32296  bnj1186  32298  bj-nfxfr  32460  bj-axsep  32614  bj-zfpow  32616  bj-dtru  32618  bj-n0i  32738  bj-snsetex  32756  bj-tagss  32773  bj-2upln0  32816  bj-2upln1upl  32817  bj-nuliota  32821  bj-elid  32826  bj-pinftyccb  32850  bj-minftyccb  32854  bj-pinftynminfty  32856  renegclALT  32920  mapdunirnN  35601
  Copyright terms: Public domain W3C validator