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  880  pm5.16  888  biluk  931  4exmid  937  dn1  964  3ori  1287  trubifal  1420  cadan  1445  nic-dfim  1487  nic-dfneg  1488  nic-mp  1489  nic-mpALT  1490  tbw-negdf  1517  rb-imdf  1568  mpgbi  1606  19.35i  1674  19.36aiv  1748  19.37aiv  1754  19.36i  1949  ax6  1987  sbie  2133  sbieOLD  2134  sbidmOLD  2141  axi12  2417  bm1.1  2424  eqcomi  2454  eqtri  2470  eleqtri  2527  neii  2640  necomi  2711  nesymiOLD  2715  neeqtri  2739  neli  2776  nrex  2896  rexlimi  2923  rexlimiv  2927  isseti  3099  vtocl2  3146  vtocl3  3147  eueq1  3256  euxfr2  3268  cdeqri  3297  sseqtri  3519  3sstr3i  3525  pssn2lp  3588  equncomi  3633  unssi  3662  ssini  3704  unabs  3711  inabs  3712  dfin4  3721  npss0  3848  difid  3879  disjdif  3883  difin0  3884  snid  4039  iinrab2  4375  rintn0  4403  breqtri  4457  axsep  4554  bm1.3ii  4558  ax6vsep  4559  zfnuleu  4560  notzfaus  4609  zfpow  4613  dtru  4625  reusv2lem4  4638  reuxfr2d  4657  dtruALT  4666  dtruALT2  4678  op1stb  4704  copsexg  4719  copsexgOLD  4720  uniop  4737  pwundif  4774  onunisuci  4978  relop  5140  rn0  5241  dmresi  5316  issref  5367  somincom  5391  cnvcnv  5446  rescnvcnv  5457  cnvcnvres  5458  cnvsn  5478  cocnvcnv2  5506  cores2  5507  co01  5509  relcoi1  5523  cnviin  5531  iota4an  5557  fnopab  5692  mpt0  5695  fnmpti  5696  f1cnvcnv  5776  f1ovi  5839  eliman0  5882  fvco4i  5933  fmpti  6036  fvsnun2  6089  funiunfv  6142  oprabss  6370  relmptopab  6505  zfun  6575  tfinds2  6680  omon  6693  2nd0  6789  f1stres  6804  f2ndres  6805  relmpt2opab  6864  df1st2  6868  df2nd2  6869  fsplit  6887  reldmtpos  6962  dftpos4  6973  tpostpos  6974  tpos0  6984  smo0  7028  tfrlem14  7059  tfrlem16  7061  rdgsucg  7088  rdglimg  7090  frfnom  7099  oawordeulem  7202  uniixp  7491  dfdom2  7540  ssdomg  7560  xpcomf1o  7605  sbthlem5  7630  pwdom  7668  limensuci  7692  fiint  7796  fidomdm  7801  pwfilem  7813  mptfi  7818  fisn  7886  dffi3  7890  ordtypelem6  7948  ordtypelem7  7949  wemaplem2  7972  wdompwdom  8004  harwdom  8016  suc11reg  8036  zfinf  8056  axinf2  8057  noinfep  8076  cantnfvalf  8084  cantnflt  8091  cantnf0  8094  cantnf  8112  cantnfltOLD  8121  cantnfOLD  8134  tz9.1c  8161  tc2  8173  r111  8193  r1tr2  8195  r1ordg  8196  r1sssuc  8201  r1val1  8204  tz9.13  8209  r1elssi  8223  pwwf  8225  rankopb  8270  rankeq0b  8278  ranksuc  8283  rankmapu  8296  rankxplim  8297  rankxplim3  8299  rankxpsuc  8300  cp  8309  karden  8313  card0  8339  cardlim  8353  cardom  8367  infxpenlem  8391  alephsuc2  8461  alephgeom  8463  unialeph  8482  dfac4  8503  dfacacn  8521  cda1dif  8556  pm110.643  8557  infcda1  8573  ackbij1lem13  8612  ackbij2  8623  cf0  8631  cfsuc  8637  cfom  8644  cfslb2n  8648  ominf4  8692  fin23lem17  8718  fin23lem28  8720  fin23lem30  8722  fin23lem31  8723  fin23lem40  8731  isfin1-3  8766  dfacfin7  8779  fin1a2lem6  8785  itunitc1  8800  axcc3  8818  dcomex  8827  axdc2lem  8828  axcclem  8837  zfac  8840  ac3  8842  ackm  8845  axac2  8846  axac  8847  axaci  8848  cardeqv  8849  numth2  8851  numth  8852  brdom3  8906  fin71ac  8911  cardf  8925  aleph1  8946  cfpwsdom  8959  smobeth  8961  zfcndrep  8992  zfcndpow  8994  zfcndac  8997  gch2  9053  wunex3  9119  tskpr  9148  inar1  9153  rankcf  9155  tskcard  9159  tskuni  9161  grothpw  9204  axgroth4  9210  grothprim  9212  inaprc  9214  dmaddpi  9268  dmmulpi  9269  1lt2pi  9283  addpqf  9322  mulpqf  9324  1lt2nq  9351  supsrlem  9488  ssxr  9654  gtso  9666  subf  9824  negne0i  9896  negdiiOLD  9906  mulnzcnopr  10198  infmsup  10524  halflt1  10760  nn0ssz  10888  zeo  10951  numlt  11000  numltc  11001  uzf  11090  uzinfmi  11167  xaddf  11429  xsubge0  11459  xmulf  11470  infmxrcl  11514  infmxrlb  11531  infmxrgelb  11532  xrinfm0  11534  ixxf  11545  ixxssxr  11547  iooval2  11568  ioof  11628  unirnioo  11630  dfioo2  11631  fzval2  11681  fzf  11682  fz10  11712  fzpreddisj  11735  4fvwrd4  11798  fzof  11802  fzo0  11825  om2uzoi  12042  faclbnd4lem1  12347  hashkf  12383  hashgval  12384  hashinf  12386  hashresfn  12389  hashnn0n0nn  12434  hashbclem  12477  hashge3el3dif  12500  wrdexg  12533  rev0  12714  f1oun2prg  12841  sqrt2gt1lt2  13084  limsupgord  13271  limsupval  13273  fclim  13352  fsumrelem  13597  ackbijnn  13616  incexclem  13624  incexc  13625  arisum2  13648  georeclim  13657  geoisumr  13663  0.999...  13666  geoihalfsum  13667  ege2le3  13700  sin0  13758  ef01bndlem  13793  cos2bnd  13797  cos01gt0  13800  sincos2sgn  13803  sin4lt0  13804  rpnnen2lem3  13824  rpnnen2lem9  13830  rexpen  13835  cnso  13854  dvdslelem  13904  n2dvds1  13909  divalglem1  13926  divalglem5  13929  divalglem6  13930  divalglem10  13934  0bits  13963  sadcf  13977  sadcadd  13982  bitsshft  13999  smupf  14002  gcdf  14031  eucalgf  14086  2prm  14107  dfphi2  14178  pockthi  14299  prmreclem2  14309  prmrec  14314  vdwapf  14364  vdwap0  14368  vdwlem6  14378  ramval  14400  ramcl2lem  14401  karatsuba  14444  1259lem5  14491  2503lem3  14495  4001lem4  14500  structcnvcnv  14517  structfn  14519  strlemor1  14598  strleun  14601  prdsval  14726  prdsds  14735  imasdsfn  14785  imasdsval  14786  imasvscafn  14808  xpsc0  14831  xpsc1  14832  xpsff1o  14839  sscpwex  15058  wunfunc  15139  wunnat  15196  eldmcoa  15263  coapm  15269  catcfuccl  15307  catcxpccl  15347  yonedainv  15421  plusffval  15748  grpinvfvi  15962  mulgfvi  16017  symgsssg  16363  symgfisg  16364  psgnunilem5  16390  sylow3lem2  16519  oppglsm  16533  efgmf  16602  efgval  16606  efgsf  16618  0frgp  16668  gsumzaddlem  16805  gsumzaddlemOLD  16807  dmdprd  16900  dprdval  16905  dprdvalOLD  16907  invrfval  17193  drngui  17273  scaffval  17401  lssintcl  17481  mplsubrglem  17971  mplsubrglemOLD  17972  opsrtoslem2  18020  cnfld0  18313  cnfld1  18314  cnfldsub  18317  xrsds  18332  psgnghm  18486  zrhpsgnmhm  18490  recrng  18527  ipffval  18553  ocv1  18580  dsmmbas2  18638  mdetralt  18980  maducoeval2  19012  eltpsi  19317  unitg  19338  fctop  19375  cctop  19377  ppttop  19378  epttop  19380  leordtvallem1  19581  leordtvallem2  19582  iccordt  19585  iscnp2  19610  discmp  19768  concompcld  19805  1stcrestlem  19823  2ndcdisj  19827  topnlly  19862  disllycmp  19869  dis1stc  19870  txuni2  19936  xkotf  19956  dfac14lem  19988  prdstps  20000  txindis  20005  tx1stc  20021  xkohaus  20024  xkoptsub  20025  cnmpt1st  20039  cnmpt2nd  20040  ptcmpfi  20184  filcon  20254  trfil1  20257  fin1aufil  20303  tgpconcompeqg  20480  tgpconcomp  20481  tsmsresOLD  20515  tsmsres  20516  trust  20602  met1stc  20894  dscmet  20963  nmoval  21092  retopon  21140  cnfldtopon  21160  xrsxmet  21184  xrsmopn  21187  metdsval  21221  iimulcn  21308  icopnfhmeo  21313  iccpnfhmeo  21315  xrhmeo  21316  cnheiborlem  21324  lebnumii  21336  ishtpy  21342  htpycc  21350  pco1  21385  pcohtpylem  21389  pcopt  21392  pcopt2  21393  pcoass  21394  pcorevlem  21396  cfilresi  21604  rrxcph  21694  ovolval  21755  ovolf  21763  ovoliunlem3  21785  ovolicc1  21797  ovolicc2  21803  volf  21810  ioorf  21852  dyadf  21870  dyadmbl  21879  vitalilem5  21891  vitali  21892  mbfimaopnlem  21932  mbflimsup  21943  0plef  21949  i1fima  21955  i1fima2  21956  i1fd  21958  itg1ge0  21963  itg10  21965  i1f1lem  21966  i1fadd  21972  i1fmul  21973  i1fmulc  21980  mbfi1fseqlem5  21996  itg2addlem  22035  reldv  22144  dvbsss  22176  dvef  22251  lhop1lem  22284  deg1fvi  22355  plypf1  22479  coeeulem  22491  coeeu  22492  vieta1lem2  22576  aannenlem3  22595  aalioulem3  22599  dvradcnv  22685  pserulm  22686  pserdvlem2  22692  abelthlem6  22700  sinhalfpilem  22725  sincos4thpi  22775  tan4thpi  22776  sincos6thpi  22777  pige3  22779  resinf1o  22792  tanord1  22793  tanregt0  22795  efabl  22806  relogrn  22818  dfrelog  22822  logneg  22841  logltb  22853  logcn  22897  logf1o2  22900  dvlog  22901  efopnlem2  22907  efopn  22908  logccv  22913  dvsqrt  22987  cxpcn3  22991  angpined  23030  1cubr  23042  asinsin  23092  asin1  23094  reasinsin  23096  atan0  23108  atanbnd  23126  atan1  23128  log2cnv  23144  log2ublem3  23148  log2ub  23149  birthday  23153  amgmlem  23188  emcllem5  23198  emgt0  23205  harmonicbnd3  23206  ftalem3  23217  basellem4  23226  sgmf  23288  ppi1  23307  cht1  23308  vma1  23309  ppiltx  23320  sqff1o  23325  ppiublem1  23346  ppiublem2  23347  ppiub  23348  chtub  23356  dchreq  23402  bposlem7  23434  bposlem8  23435  bposlem9  23436  lgsdir2lem2  23468  lgsdir2lem3  23469  chebbnd1  23526  chto1ub  23530  chpo1ubb  23535  pntibndlem1  23643  tgldimor  23762  tglnfn  23803  axlowdimlem4  24117  axlowdimlem16  24129  axlowdim  24133  umgrafi  24191  usgraexmpl  24270  usgraexmplc  24273  usgrafilem1  24280  2trllemA  24421  wlkntrllem1  24430  wlkntrllem3  24432  0pth  24441  spthispth  24444  2pthon  24473  2pthon3v  24475  constr3trllem3  24521  constr3pthlem3  24526  konigsberg  24856  frgrawopreg2  24920  ex-dif  25013  ex-un  25014  ex-in  25015  ex-fl  25037  avril1  25040  ginvsn  25220  cnid  25222  mulid  25227  rngosn3  25297  vcoprnelem  25340  vcex  25342  cnnvm  25457  ipasslem8  25621  ipasslem10  25623  hvsubf  25801  normlem1  25896  normlem6  25901  normlem7  25902  norm-ii-i  25923  norm3adifii  25934  hilid  25947  hlimf  26024  hhssabloi  26047  hhssnv  26049  hhshsslem1  26052  shincli  26149  shsval2i  26174  shs0i  26236  chj0i  26242  chm1i  26243  chincli  26247  chdmm1i  26264  shjshsi  26279  chsup0  26335  h1de2bi  26341  spansnpji  26365  cmcmlem  26378  cmcmii  26384  cmcm2ii  26385  cmcm3ii  26386  pjidmi  26460  pjssmii  26468  pj0i  26480  pjocini  26485  mayetes3i  26517  df0op2  26540  hoaddcomi  26560  hoaddassi  26564  hocadddiri  26567  hocsubdiri  26568  hoaddid1i  26574  ho0coi  26576  hoid1i  26577  hoid1ri  26578  hodseqi  26582  honegsubi  26584  adj1o  26682  hoddii  26777  lnopunilem1  26798  lnopunilem2  26799  nmcopexi  26815  nmcopex  26817  nmcoplb  26818  nmcfnexi  26839  nmcfnex  26841  nmcfnlb  26842  adjbd1o  26873  adjcoi  26888  nmopcoadji  26889  opsqrlem6  26933  pjsdii  26943  pjddii  26944  pjidmcoi  26965  pjtoi  26967  pjin1i  26980  pjclem1  26983  stji1i  27030  reuxfr3d  27257  inindif  27283  iuninc  27297  fnresin  27339  rinvf1o  27341  suppss2f  27346  xppreima  27356  ofoprabco  27374  funcnvmptOLD  27378  gtiso  27388  df1stres  27391  df2ndres  27392  snct  27403  dmct  27406  ffsrn  27421  fpwrelmapffs  27426  xrge0infssd  27450  nnindf  27480  nn0min  27481  ressplusf  27508  xrsclat  27538  xrge0base  27543  xrge00  27544  xrge0neqmnf  27549  xrnarchi  27598  xrge0slmod  27704  locfinreflem  27713  locfinref  27714  unicls  27755  sqsscirc1  27760  mhmhmeotmd  27779  rmulccn  27780  raddcn  27781  xrge0iifiso  27787  xrge0iifhmeo  27788  lmxrge0  27804  cnzh  27821  rezh  27822  qqh0  27835  qqh1  27836  qqhre  27868  rnlogblem  27885  log2le1  27893  esumnul  27929  esum0  27930  esumsn  27942  esumpfinvallem  27950  esumpfinvalf  27952  esumpcvgval  27954  sigaclfu2  27991  dmsigagen  28014  ddemeas  28078  imambfm  28103  mbfmvolf  28107  br2base  28110  omsfval  28135  oms0  28136  sibfof  28152  sitg0  28158  eulerpartlemt  28180  eulerpartgbij  28181  0rrv  28260  coinfliplem  28287  coinflipprob  28288  coinfliprv  28291  ballotlem2  28297  ballotlem4  28307  ballotlem5  28308  ballotlemi1  28311  ballotlem7  28344  ballotth  28346  signsplypnf  28377  signsply0  28378  signsw0g  28383  signswch  28388  signsvf0  28407  subfacf  28489  subfacp1lem1  28493  subfacp1lem5  28498  subfacp1lem6  28499  subfacval3  28503  erdszelem2  28506  kur14lem4  28523  iooscon  28562  iccllyscon  28565  msrfo  28776  mthmpps  28812  problem5  28893  quad3  28894  ghomgrpilem1  28895  ghomgrpilem2  28896  circum  28910  axextprim  28943  axrepprim  28944  axunprim  28945  axinfprim  28948  axacprim  28949  inffz  28978  risefall0lem  29120  setinds  29182  dfon2lem2  29188  dfon2lem4  29190  axextdfeq  29202  poseq  29305  wfrlem4  29318  frrlem4  29362  nosgnn0  29390  sltsolem1  29400  bdayfo  29407  symdifV  29447  fobigcup  29522  snelsingles  29544  fullfunfnv  29568  fullfunfv  29569  rankaltopb  29601  rank0  29799  rankeq1o  29800  hfuni  29813  nabi1i  29829  nabi2i  29830  limsucncmpi  29882  tan2h  30019  mblfinlem1  30023  mblfinlem2  30024  ovoliunnfl  30028  voliunnfl  30030  dvtanlem  30036  itg2addnclem  30038  itg2addnclem2  30039  dvcnsqrt  30073  asindmre  30074  areacirclem1  30079  fneer  30143  neibastop1  30149  fdc  30210  cntotbnd  30264  heiborlem6  30284  rrnval  30295  reheibor  30307  prter2  30594  diophrw  30664  rabren3dioph  30721  pellexlem6  30742  pellex  30743  frmx  30821  frmy  30822  jm2.23  30910  jm2.27dlem3  30925  axac10  30947  pw2f1ocnv  30951  kelac2lem  30982  lmhmlnmsplit  31005  pwfi2f1o  31016  frlmpwfi  31018  seff  31162  expgrowthi  31211  expgrowth  31213  negpilt0  31411  ioontr  31485  iccdifioo  31491  iccdifprioo  31492  icccncfext  31597  dvcosre  31610  dvsinax  31612  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  stoweidlem1  31672  stoweidlem26  31697  stoweidlem34  31705  stoweidlem44  31715  stoweid  31734  stirlinglem5  31749  dirkercncflem1  31774  fourierdlem44  31822  fourierdlem56  31834  fourierdlem62  31840  fourierdlem89  31867  fourierdlem91  31869  fourierdlem100  31878  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem108  31886  fourierdlem112  31890  fourierdlem114  31892  fouriersw  31903  axorbtnotaiffb  31936  axorbciffatcxorb  31938  abnotbtaxb  31949  resisresindm  32143  residfi  32152  ldepslinc  32840  alimp-no-surprise  32926  ee233  33017  ax6e2nd  33059  in1  33076  dfvd2ani  33088  dfvd2i  33090  dfvd3i  33097  dfvd3ani  33100  e0bi  33301  uun2221  33338  uun2221p1  33339  uun2221p2  33340  en3lpVD  33373  relopabVD  33429  ax6e2ndVD  33436  ax6e2ndALT  33458  bnj521  33520  bnj1098  33570  bnj1109  33573  bnj1131  33574  bnj1533  33638  bnj151  33663  bnj580  33699  bnj852  33707  bnj864  33708  bnj865  33709  bnj978  33735  bnj1021  33750  bnj907  33751  bnj1093  33764  bnj1145  33777  bnj1172  33785  bnj1174  33787  bnj1176  33789  bnj1186  33791  bj-nfxfr  33953  bj-axsep  34112  bj-zfpow  34114  bj-dtru  34116  bj-n0i  34236  bj-snsetex  34254  bj-tagss  34271  bj-2upln0  34314  bj-2upln1upl  34315  bj-nuliota  34319  bj-elid  34324  bj-pinftyccb  34347  bj-minftyccb  34351  bj-pinftynminfty  34353  renegclALT  34417  mapdunirnN  37100  trclubg  37461  0heALT  37476  bj-frege54cor1a  37559
  Copyright terms: Public domain W3C validator