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, 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 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  625  pm4.71ri  626  pm5.32i  630  pm3.24  870  pm5.16  878  biluk  917  4exmid  923  dn1  950  3ori  1271  trubifal  1401  cadan  1436  nic-dfim  1479  nic-dfneg  1480  nic-mp  1481  nic-mpALT  1482  tbw-negdf  1509  rb-imdf  1560  mpgbi  1597  19.35i  1655  19.36i  1891  19.37aiv  1917  ax6  1946  sbie  2098  sbieOLD  2099  sbcoOLD  2108  sbidmOLD  2111  axi12  2412  eqcomi  2437  eqtri  2453  eleqtri  2505  neii  2600  neeqtri  2619  nesymi  2638  necomi  2684  neli  2697  nrex  2808  rexlimi  2824  isseti  2968  vtocl2  3014  vtocl3  3015  eueq1  3121  euxfr2  3133  cdeqri  3161  sseqtri  3376  3sstr3i  3382  pssn2lp  3445  equncomi  3490  unssi  3519  ssini  3561  unabs  3568  inabs  3569  dfin4  3578  npss0  3705  difid  3735  disjdif  3739  difin0  3740  snid  3893  iinrab2  4221  rintn0  4249  breqtri  4303  axsep  4400  bm1.3ii  4404  ax6vsep  4405  zfnuleu  4406  notzfaus  4455  zfpow  4459  dtru  4471  reusv2lem4  4484  reuxfr2d  4503  dtruALT  4512  dtruALT2  4524  op1stb  4550  copsexg  4564  copsexgOLD  4565  uniop  4582  pwundif  4615  onunisuci  4819  relop  4977  rn0  5078  dmresi  5149  issref  5199  somincom  5223  cnvcnv  5278  rescnvcnv  5289  cnvcnvres  5290  cnvsn  5310  cocnvcnv2  5337  cores2  5338  co01  5340  relcoi1  5354  cnviin  5362  iota4an  5388  fnopab  5523  mpt0  5526  fnmpti  5527  f1cnvcnv  5602  f1ovi  5665  eliman0  5707  fvco4i  5757  fmpti  5854  fvsnun2  5901  funiunfv  5952  oprabss  6165  relmptopab  6297  zfun  6362  tfinds2  6463  omon  6476  2nd0  6573  f1stres  6587  f2ndres  6588  relmpt2opab  6644  df1st2  6648  df2nd2  6649  fsplit  6666  reldmtpos  6742  dftpos4  6753  tpostpos  6754  tpos0  6764  smo0  6805  tfrlem14  6836  tfrlem16  6838  rdgsucg  6865  rdglimg  6867  frfnom  6876  oawordeulem  6981  uniixp  7274  dfdom2  7323  ssdomg  7343  xpcomf1o  7388  sbthlem5  7413  pwdom  7451  limensuci  7475  fiint  7576  fidomdm  7581  pwfilem  7593  mptfi  7598  fisn  7665  dffi3  7669  ordtypelem6  7725  ordtypelem7  7726  wemaplem2  7749  wdompwdom  7781  harwdom  7793  suc11reg  7813  zfinf  7833  axinf2  7834  noinfep  7853  cantnfvalf  7861  cantnflt  7868  cantnf0  7871  cantnf  7889  cantnfltOLD  7898  cantnfOLD  7911  tz9.1c  7938  tc2  7950  r111  7970  r1tr2  7972  r1ordg  7973  r1sssuc  7978  r1val1  7981  tz9.13  7986  r1elssi  8000  pwwf  8002  rankopb  8047  rankeq0b  8055  ranksuc  8060  rankmapu  8073  rankxplim  8074  rankxplim3  8076  rankxpsuc  8077  cp  8086  karden  8090  card0  8116  cardlim  8130  cardom  8144  infxpenlem  8168  alephsuc2  8238  alephgeom  8240  unialeph  8259  dfac4  8280  dfacacn  8298  cda1dif  8333  pm110.643  8334  infcda1  8350  ackbij1lem13  8389  ackbij2  8400  cf0  8408  cfsuc  8414  cfom  8421  cfslb2n  8425  ominf4  8469  fin23lem17  8495  fin23lem28  8497  fin23lem30  8499  fin23lem31  8500  fin23lem40  8508  isfin1-3  8543  dfacfin7  8556  fin1a2lem6  8562  itunitc1  8577  axcc3  8595  dcomex  8604  axdc2lem  8605  axcclem  8614  zfac  8617  ac3  8619  ackm  8622  axac2  8623  axac  8624  axaci  8625  cardeqv  8626  numth2  8628  numth  8629  brdom3  8683  fin71ac  8688  cardf  8702  aleph1  8723  cfpwsdom  8736  smobeth  8738  zfcndrep  8768  zfcndpow  8770  zfcndac  8773  gch2  8829  wunex3  8895  tskpr  8924  inar1  8929  rankcf  8931  tskcard  8935  tskuni  8937  grothpw  8980  axgroth4  8986  grothprim  8988  inaprc  8990  dmaddpi  9046  dmmulpi  9047  1lt2pi  9061  addpqf  9100  mulpqf  9102  1lt2nq  9129  supsrlem  9265  ssxr  9431  gtso  9443  subf  9599  negne0i  9670  negdii  9679  mulnzcnopr  9969  infmsup  10295  halflt1  10530  nn0ssz  10654  zeo  10714  numlt  10761  numltc  10762  uzf  10851  uzinfmi  10921  xaddf  11181  xsubge0  11211  xmulf  11222  infmxrcl  11266  infmxrlb  11283  infmxrgelb  11284  xrinfm0  11286  ixxf  11297  ixxssxr  11299  iooval2  11320  ioof  11374  unirnioo  11376  dfioo2  11377  fzval2  11426  fzf  11427  fz10  11456  4fvwrd4  11516  fzof  11533  fzo0  11556  fzo0ss1  11562  injresinjlem  11621  om2uzoi  11761  faclbnd4lem1  12052  hashkf  12088  hashgval  12089  hashinf  12091  hashresfn  12094  hashnn0n0nn  12136  hashge3el3dif  12170  hashbclem  12188  wrdexg  12227  rev0  12387  f1oun2prg  12510  sqr2gt1lt2  12747  limsupgord  12933  limsupval  12935  fclim  13014  fsumrelem  13252  ackbijnn  13273  incexclem  13281  incexc  13282  arisum2  13305  georeclim  13314  geoisumr  13320  0.999...  13323  geoihalfsum  13324  ege2le3  13357  sin0  13415  ef01bndlem  13450  cos2bnd  13454  cos01gt0  13457  sincos2sgn  13460  sin4lt0  13461  rpnnen2lem3  13481  rpnnen2lem9  13487  rexpen  13492  cnso  13511  dvdslelem  13559  n2dvds1  13564  divalglem1  13580  divalglem5  13583  divalglem6  13584  divalglem10  13588  0bits  13617  sadcf  13631  sadcadd  13636  bitsshft  13653  smupf  13656  gcdf  13685  eucalgf  13740  isprm3  13754  2prm  13761  dfphi2  13831  reumodprminv  13854  pockthi  13950  prmreclem2  13960  prmrec  13965  vdwapf  14015  vdwap0  14019  vdwlem6  14029  ramval  14051  ramcl2lem  14052  karatsuba  14095  1259lem5  14141  2503lem3  14145  4001lem4  14150  structcnvcnv  14167  structfn  14169  strlemor1  14247  strleun  14250  prdsval  14375  prdsds  14384  imasdsfn  14434  imasdsval  14435  imasvscafn  14457  xpsc0  14480  xpsc1  14481  xpsff1o  14488  sscpwex  14710  wunfunc  14791  wunnat  14848  eldmcoa  14915  coapm  14921  catcfuccl  14959  catcxpccl  14999  yonedainv  15073  plusffval  15409  grpinvfvi  15558  mulgfvi  15610  symgsssg  15952  symgfisg  15953  psgnunilem5  15979  sylow3lem2  16106  oppglsm  16120  efgmf  16189  efgval  16193  efgsf  16205  0frgp  16255  gsumzaddlem  16387  gsumzaddlemOLD  16389  dmdprd  16453  dprdval  16458  dprdvalOLD  16460  invrfval  16698  drngui  16761  scaffval  16889  lssintcl  16966  mplsubrglem  17450  mplsubrglemOLD  17451  opsrtoslem2  17497  cnfld0  17683  cnfld1  17684  cnfldsub  17687  xrsds  17699  psgnghm  17851  zrhpsgnmhm  17855  psgnodpmr  17861  recrng  17892  ipffval  17918  ocv1  17945  dsmmbas2  18003  frlmip  18044  mdetralt  18255  maducoeval2  18287  eltpsi  18392  fctop  18449  cctop  18451  ppttop  18452  epttop  18454  leordtvallem1  18655  leordtvallem2  18656  iccordt  18659  iscnp2  18684  discmp  18842  concompcld  18879  1stcrestlem  18897  2ndcdisj  18901  topnlly  18936  disllycmp  18943  dis1stc  18944  txuni2  18979  xkotf  18999  dfac14lem  19031  prdstps  19043  txindis  19048  tx1stc  19064  xkohaus  19067  xkoptsub  19068  cnmpt1st  19082  cnmpt2nd  19083  ptcmpfi  19227  filcon  19297  trfil1  19300  fin1aufil  19346  tgpconcompeqg  19523  tgpconcomp  19524  tsmsresOLD  19558  tsmsres  19559  trust  19645  met1stc  19937  dscmet  20006  nmoval  20135  retopon  20183  cnfldtopon  20203  xrsxmet  20227  xrsmopn  20230  metdsval  20264  iimulcn  20351  icopnfhmeo  20356  iccpnfhmeo  20358  xrhmeo  20359  cnheiborlem  20367  lebnumii  20379  ishtpy  20385  htpycc  20393  pco1  20428  pcohtpylem  20432  pcopt  20435  pcopt2  20436  pcoass  20437  pcorevlem  20439  cfilresi  20647  rrxip  20735  rrxcph  20737  ovolval  20798  ovolf  20806  ovoliunlem3  20828  ovolicc1  20840  ovolicc2  20846  volf  20853  ioorf  20894  dyadf  20912  dyadmbl  20921  vitalilem5  20933  vitali  20934  mbfimaopnlem  20974  mbflimsup  20985  0plef  20991  i1fima  20997  i1fima2  20998  i1fd  21000  itg1ge0  21005  itg10  21007  i1f1lem  21008  i1fadd  21014  i1fmul  21015  i1fmulc  21022  mbfi1fseqlem5  21038  itg2addlem  21077  reldv  21186  dvbsss  21218  dvef  21293  lhop1lem  21326  deg1fvi  21440  plypf1  21564  coeeulem  21576  coeeu  21577  vieta1lem2  21661  aannenlem3  21680  aalioulem3  21684  dvradcnv  21770  pserulm  21771  pserdvlem2  21777  abelthlem6  21785  sinhalfpilem  21809  sincos4thpi  21859  tan4thpi  21860  sincos6thpi  21861  pige3  21863  resinf1o  21876  tanord1  21877  tanregt0  21879  relogrn  21897  dfrelog  21901  logneg  21920  logltb  21932  logcn  21976  logf1o2  21979  dvlog  21980  efopnlem2  21986  efopn  21987  logccv  21992  dvsqr  22066  cxpcn3  22070  angpined  22109  1cubr  22121  asinsin  22171  asin1  22173  reasinsin  22175  atan0  22187  atanbnd  22205  atan1  22207  log2cnv  22223  log2ublem3  22227  log2ub  22228  birthday  22232  amgmlem  22267  emcllem5  22277  emgt0  22284  harmonicbnd3  22285  ftalem3  22296  basellem4  22305  sgmf  22367  ppi1  22386  cht1  22387  vma1  22388  ppiltx  22399  sqff1o  22404  ppiublem1  22425  ppiublem2  22426  ppiub  22427  chtub  22435  dchreq  22481  bposlem7  22513  bposlem8  22514  bposlem9  22515  lgsdir2lem2  22547  lgsdir2lem3  22548  chebbnd1  22605  chto1ub  22609  chpo1ubb  22614  pntibndlem1  22722  tgldimor  22836  tglnfn  22861  legov  22891  legtrid  22897  axlowdimlem4  23013  axlowdimlem13  23022  axlowdimlem16  23025  axlowdim1  23027  axlowdim  23029  ecgrtg  23051  umgrafi  23078  usgraexmpl  23141  usgrafilem1  23146  2trllemA  23271  wlkntrllem1  23280  wlkntrllem3  23282  0pth  23291  spthispth  23294  2pthon  23323  2pthon3v  23325  redwlk  23327  constr3trllem3  23360  constr3pthlem3  23365  konigsberg  23430  ex-dif  23452  ex-un  23453  ex-in  23454  ex-fl  23476  avril1  23478  ginvsn  23658  cnid  23660  mulid  23665  rngosn3  23735  vcoprnelem  23778  vcoprne  23779  vcex  23780  cnnvm  23895  ipasslem8  24059  ipasslem10  24061  hvsubf  24239  normlem1  24334  normlem6  24339  normlem7  24340  norm-ii-i  24361  norm3adifii  24372  hilid  24385  hlimf  24462  norm1exi  24475  hhssabloi  24485  hhssnv  24487  hhshsslem1  24490  shincli  24587  shsval2i  24612  shs0i  24674  chj0i  24680  chm1i  24681  chincli  24685  chdmm1i  24702  shjshsi  24717  chsup0  24773  h1de2bi  24779  spansnpji  24803  cmcmlem  24816  cmcmii  24822  cmcm2ii  24823  cmcm3ii  24824  pjidmi  24898  pjssmii  24906  pj0i  24918  pjocini  24923  mayetes3i  24955  df0op2  24978  hoaddcomi  24998  hoaddassi  25002  hocadddiri  25005  hocsubdiri  25006  hoaddid1i  25012  ho0coi  25014  hoid1i  25015  hoid1ri  25016  hodseqi  25020  honegsubi  25022  adj1o  25120  hoddii  25215  lnopunilem1  25236  lnopunilem2  25237  nmcopexi  25253  nmcopex  25255  nmcoplb  25256  nmcfnexi  25277  nmcfnex  25279  nmcfnlb  25280  adjbd1o  25311  adjcoi  25326  nmopcoadji  25327  opsqrlem6  25371  pjsdii  25381  pjddii  25382  pjidmcoi  25403  pjtoi  25405  pjin1i  25418  pjclem1  25421  stji1i  25468  largei  25493  spc2ed  25679  reuxfr3d  25696  inindif  25720  iuninc  25734  fnresin  25770  rinvf1o  25772  suppss2f  25777  xppreima  25787  ofoprabco  25805  funcnvmptOLD  25809  gtiso  25819  df1stres  25822  df2ndres  25823  snct  25834  dmct  25837  ffsrn  25853  resf1o  25854  fpwrelmapffs  25858  nnindf  25911  nn0min  25912  ressplusf  25933  xrsclat  25963  xrge0base  25968  xrge00  25969  xrge0neqmnf  25974  xrnarchi  26024  orngsqr  26124  xrge0slmod  26165  unicls  26186  sqsscirc1  26191  ordtconlem1  26207  mhmhmeotmd  26210  rmulccn  26211  raddcn  26212  xrge0iifiso  26218  xrge0iifhmeo  26219  lmxrge0  26235  cnzh  26252  rezh  26253  qqh0  26266  qqh1  26267  qqhre  26299  rrhre  26300  rnlogblem  26311  log2le1  26319  ind1a  26330  esumnul  26355  esum0  26356  esumsn  26368  esumpfinvallem  26376  esumpfinvalf  26378  esumpcvgval  26380  sigaclfu2  26417  dmsigagen  26440  ddemeas  26505  imambfm  26530  mbfmvolf  26534  br2base  26537  sibfof  26573  sitg0  26579  eulerpartlemt  26601  eulerpartgbij  26602  fib5  26635  probdif  26650  0rrv  26681  coinfliplem  26708  coinflipprob  26709  coinfliprv  26712  ballotlem2  26718  ballotlem4  26728  ballotlem5  26729  ballotlemi  26730  ballotlemiex  26731  ballotlemi1  26732  ballotlemii  26733  ballotlemsup  26734  ballotlemimin  26735  ballotlemfrcn0  26759  ballotlemirc  26761  ballotlem7  26765  ballotth  26767  signsplypnf  26798  signsply0  26799  signsw0g  26804  signswch  26809  signsvvf  26827  signsvf0  26828  subfacf  26910  subfacp1lem1  26914  subfacp1lem5  26919  subfacp1lem6  26920  subfacval3  26924  erdszelem2  26927  erdszelem9  26934  erdszelem11  26936  kur14lem4  26944  iooscon  26983  iccllyscon  26986  problem5  27149  ghomgrpilem1  27150  ghomgrpilem2  27151  circum  27165  axextprim  27198  axrepprim  27199  axunprim  27200  axinfprim  27203  axacprim  27204  inffz  27233  risefall0lem  27375  setinds  27437  dfon2lem2  27443  dfon2lem4  27445  dfrdg2  27455  axextdfeq  27457  poseq  27560  wfrlem4  27573  frrlem4  27617  sltval2  27643  nosgnn0  27645  sltintdifex  27650  sltres  27651  sltsolem1  27655  bdayfo  27662  symdifV  27702  fobigcup  27777  snelsingles  27799  fullfunfnv  27823  fullfunfv  27824  dfrdg4  27827  rankaltopb  27856  linedegen  28020  rank0  28054  rankeq1o  28055  hfuni  28068  nabi1i  28084  nabi2i  28085  limsucncmpi  28138  tan2h  28265  heicant  28267  mblfinlem1  28269  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  dvtanlem  28282  itg2addnclem  28284  itg2addnclem2  28285  dvcnsqr  28319  asindmre  28320  areacirclem1  28325  gtinf  28355  fneer  28401  neibastop1  28421  opelopab3  28451  fdc  28482  cntotbnd  28536  heiborlem6  28556  rrnval  28567  reheibor  28579  impor  28722  prter2  28868  diophrw  28939  0dioph  28959  rabren3dioph  28996  rencldnfilem  29001  pellexlem6  29017  pellex  29018  pellfundval  29063  frmx  29096  frmy  29097  jm2.23  29187  jm2.27dlem3  29202  axac10  29224  pw2f1ocnv  29228  wepwsolem  29236  kelac2lem  29259  lmhmlnmsplit  29282  pwfi2f1o  29293  frlmpwfi  29295  dgraaval  29343  dgraaf  29346  areaquad  29434  seff  29437  expgrowthi  29449  expgrowth  29451  refsum2cnlem1  29601  infrglb  29614  dvcosre  29631  stoweidlem1  29639  stoweidlem26  29664  stoweidlem34  29672  stoweidlem44  29682  stoweid  29701  stirlinglem5  29716  axorbtnotaiffb  29760  axorbciffatcxorb  29762  abnotbtaxb  29773  resisresindm  29982  wwlktovf  30094  frgrawopreg2  30487  ldepslinc  30757  comraddi  30820  alimp-no-surprise  30837  ee233  30922  ax6e2nd  30965  in1  30982  dfvd2ani  30995  dfvd2i  30997  dfvd3i  31004  dfvd3ani  31007  e0bi  31208  uun2221  31245  uun2221p1  31246  uun2221p2  31247  en3lpVD  31280  relopabVD  31336  ax6e2ndVD  31343  ax6e2ndALT  31365  bnj521  31427  bnj1098  31476  bnj1109  31479  bnj1131  31480  bnj1533  31544  bnj151  31569  bnj580  31605  bnj852  31613  bnj864  31614  bnj865  31615  bnj978  31641  bnj1021  31656  bnj907  31657  bnj1093  31670  bnj1145  31683  bnj1172  31691  bnj1174  31693  bnj1176  31695  bnj1186  31697  bj-nfxfr  31818  bj-axsep  31931  bj-zfpow  31933  bj-dtru  31935  bj-n0i  32018  bj-snsetex  32036  bj-tagss  32053  bj-2upln0  32096  bj-2upln1upl  32097  bj-pinftyccb  32121  bj-minftyccb  32125  bj-pinftynminfty  32127  renegclALT  32184  mapdunirnN  34865
  Copyright terms: Public domain W3C validator