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

Theorem mpbi 211
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 197 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  pm5.74i  248  notbii  297  pm5.19  361  ori  376  imori  414  pm4.71i  636  pm4.71ri  637  pm5.32i  641  pm3.24  890  pm5.16  898  biluk  941  4exmid  947  dn1  974  3ori  1324  trubifalOLD  1478  cadan  1507  nic-dfim  1548  nic-dfneg  1549  nic-mp  1550  nic-mpALT  1551  tbw-negdf  1578  rb-imdf  1629  mpgbi  1668  19.35i  1733  19.36iv  1810  19.37iv  1816  19.36i  2019  ax6  2056  sbie  2200  axi12  2396  bm1.1  2403  eqcomi  2433  eqtri  2449  eleqtri  2506  neii  2620  necomi  2692  nesymiOLD  2696  neeqtri  2720  neli  2758  nrex  2878  rexlimi  2905  rexlimiv  2909  isseti  3084  vtocl2  3131  vtocl3  3132  eueq1  3241  euxfr2  3253  cdeqri  3282  sseqtri  3493  3sstr3i  3499  pssn2lp  3563  equncomi  3609  unssi  3638  ssini  3682  unabs  3700  inabs  3701  dfin4  3710  npss0  3828  difid  3860  disjdif  3864  difin0  3865  snid  4021  iinrab2  4356  symdifv  4371  rintn0  4387  breqtri  4440  axsep  4538  bm1.3ii  4542  ax6vsep  4543  zfnuleu  4544  notzfaus  4591  zfpow  4595  dtru  4607  reusv2lem4  4620  reuxfr2d  4636  dtruALT  4645  dtruALT2  4657  op1stb  4683  copsexg  4698  uniop  4715  pwundif  4752  relop  4996  rn0  5097  dmresi  5171  issref  5224  somincom  5245  cnvcnv  5299  rescnvcnv  5309  cnvcnvres  5310  cnvsn  5330  cocnvcnv2  5358  cores2  5359  co01  5361  relcoi1OLD  5376  cnviin  5384  onunisuci  5546  iota4an  5575  fnopab  5711  mpt0  5714  fnmpti  5715  f1cnvcnv  5795  f1ovi  5858  eliman0  5901  fvco4i  5950  fmpti  6051  fvsnun2  6106  funiunfv  6159  oprabss  6387  relmptopab  6522  zfun  6589  tfinds2  6695  omon  6708  2nd0  6805  f1stres  6820  f2ndres  6821  relmpt2opab  6880  df1st2  6884  df2nd2  6885  fsplit  6903  reldmtpos  6980  dftpos4  6991  tpostpos  6992  tpos0  7002  wfrlem4  7038  smo0  7076  tfrlem14  7108  tfrlem16  7110  rdgsucg  7140  rdglimg  7142  frfnom  7151  oawordeulem  7254  uniixp  7544  dfdom2  7593  ssdomg  7613  xpcomf1o  7658  sbthlem5  7683  pwdom  7721  limensuci  7745  fiint  7845  fidomdm  7850  pwfilem  7865  mptfi  7870  fisn  7938  dffi3  7942  ordtypelem6  8029  ordtypelem7  8030  wemaplem2  8053  wdompwdom  8084  harwdom  8096  suc11reg  8115  zfinf  8135  axinf2  8136  noinfep  8155  cantnfvalf  8160  cantnflt  8167  cantnf0  8170  cantnf  8188  tz9.1c  8204  tc2  8216  r111  8236  r1tr2  8238  r1ordg  8239  r1sssuc  8244  r1val1  8247  tz9.13  8252  r1elssi  8266  pwwf  8268  rankopb  8313  rankeq0b  8321  ranksuc  8326  rankmapu  8339  rankxplim  8340  rankxplim3  8342  rankxpsuc  8343  cp  8352  karden  8356  card0  8382  cardlim  8396  cardom  8410  infxpenlem  8434  alephsuc2  8500  alephgeom  8502  unialeph  8521  dfac4  8542  dfacacn  8560  cda1dif  8595  pm110.643  8596  infcda1  8612  ackbij1lem13  8651  ackbij2  8662  cf0  8670  cfsuc  8676  cfom  8683  cfslb2n  8687  ominf4  8731  fin23lem17  8757  fin23lem28  8759  fin23lem30  8761  fin23lem31  8762  fin23lem40  8770  isfin1-3  8805  dfacfin7  8818  fin1a2lem6  8824  itunitc1  8839  axcc3  8857  dcomex  8866  axdc2lem  8867  axcclem  8876  zfac  8879  ac3  8881  ackm  8884  axac2  8885  axac  8886  axaci  8887  cardeqv  8888  numth2  8890  numth  8891  brdom3  8945  fin71ac  8950  cardf  8964  aleph1  8985  cfpwsdom  8998  smobeth  9000  zfcndrep  9028  zfcndpow  9030  zfcndac  9033  gch2  9089  wunex3  9155  tskpr  9184  inar1  9189  rankcf  9191  tskcard  9195  tskuni  9197  grothpw  9240  axgroth4  9246  grothprim  9248  inaprc  9250  dmaddpi  9304  dmmulpi  9305  1lt2pi  9319  addpqf  9358  mulpqf  9360  1lt2nq  9387  supsrlem  9524  ssxr  9692  gtso  9704  subf  9866  negne0i  9938  negdiiOLD  9948  mulnzcnopr  10247  infrenegsup  10580  infmsupOLD  10581  halflt1  10820  nn0ssz  10947  zeo  11010  numlt  11059  numltc  11060  uzf  11151  uzinfmiOLD  11228  zgt1rpn0n1  11329  xaddf  11506  xsubge0  11536  xmulf  11547  infmxrclOLD  11591  infmxrlbOLD  11613  infmxrgelbOLD  11614  xrinfm0OLD  11616  ixxf  11634  ixxssxr  11636  iooval2  11658  ioof  11721  unirnioo  11723  dfioo2  11724  fzval2  11774  fzf  11775  0nelfz1  11805  fz10  11807  fzpreddisj  11832  4fvwrd4  11896  fzof  11904  fzo0  11929  om2uzoi  12155  faclbnd4lem1  12464  hashkf  12503  hashgval  12504  hashinf  12506  hashresfn  12509  hashnn0n0nn  12556  hashbclem  12599  hashge3el3dif  12622  wrdexg  12658  rev0  12843  f1oun2prg  12970  trclublem  13027  sqrt2gt1lt2  13306  limsupgord  13495  limsupvalOLD  13499  fclim  13584  fsumrelem  13834  ackbijnn  13853  incexclem  13861  incexc  13862  arisum2  13886  georeclim  13895  geoisumr  13901  0.999...  13904  geoihalfsum  13905  risefall0lem  14046  ege2le3  14111  sin0  14170  ef01bndlem  14205  cos2bnd  14209  cos01gt0  14212  sincos2sgn  14215  sin4lt0  14216  rpnnen2lem3  14236  rpnnen2lem9  14242  rexpen  14247  cnso  14266  dvdslelem  14316  n2dvds1  14321  divalglem1  14339  divalglem5  14342  divalglem6  14343  divalglem10  14347  0bits  14376  sadcf  14390  sadcadd  14395  bitsshft  14412  smupf  14415  gcdf  14446  eucalgf  14502  2prm  14600  dfphi2  14680  pockthi  14803  prmreclem2  14813  prmrec  14818  vdwapf  14874  vdwap0  14878  vdwlem6  14888  ramvalOLD  14913  ramcl2lemOLD  14915  karatsuba  15008  1259lem5  15058  2503lem3  15062  4001lem4  15067  structcnvcnv  15084  structfn  15086  strlemor1  15169  strleun  15172  prdsval  15305  prdsds  15314  imasdsfn  15364  imasdsval  15365  imasvscafn  15387  xpsc0  15410  xpsc1  15411  xpsff1o  15418  sscpwex  15664  wunfunc  15748  wunnat  15805  eldmcoa  15904  coapm  15910  catcfuccl  15948  catcxpccl  16036  yonedainv  16110  plusffval  16437  grpinvfvi  16651  mulgfvi  16706  symgsssg  17052  symgfisg  17053  psgnunilem5  17079  sylow3lem2  17208  oppglsm  17222  efgmf  17291  efgval  17295  efgsf  17307  0frgp  17357  gsumzaddlem  17482  dmdprd  17558  dprdval  17563  invrfval  17829  drngui  17909  scaffval  18037  lssintcl  18115  mplsubrglem  18591  opsrtoslem2  18636  cnfld0  18920  cnfld1  18921  cnfldsub  18924  xrsds  18939  psgnghm  19072  zrhpsgnmhm  19076  recrng  19113  ipffval  19139  ocv1  19166  dsmmbas2  19224  mdetralt  19557  maducoeval2  19589  eltpsi  19885  unitg  19906  fctop  19943  cctop  19945  ppttop  19946  epttop  19948  leordtvallem1  20150  leordtvallem2  20151  iccordt  20154  iscnp2  20179  discmp  20337  concompcld  20373  1stcrestlem  20391  2ndcdisj  20395  topnlly  20430  disllycmp  20437  dis1stc  20438  txuni2  20504  xkotf  20524  dfac14lem  20556  prdstps  20568  txindis  20573  tx1stc  20589  xkohaus  20592  xkoptsub  20593  cnmpt1st  20607  cnmpt2nd  20608  ptcmpfi  20752  filcon  20822  trfil1  20825  fin1aufil  20871  tgpconcompeqg  21050  tgpconcomp  21051  tsmsres  21082  trust  21168  met1stc  21460  dscmet  21511  nmoval  21640  retopon  21688  cnfldtopon  21707  xrsxmet  21731  xrsmopn  21734  metdsval  21768  iimulcn  21855  icopnfhmeo  21860  iccpnfhmeo  21862  xrhmeo  21863  cnheiborlem  21871  lebnumii  21883  ishtpy  21889  htpycc  21897  pco1  21932  pcohtpylem  21936  pcopt  21939  pcopt2  21940  pcoass  21941  pcorevlem  21943  cfilresi  22151  rrxcph  22237  ovolvalOLD  22301  ovoliunlem3  22331  ovolicc1  22343  ovolicc2  22350  volf  22357  ioorf  22399  ioorfOLD  22404  dyadf  22423  dyadmbl  22432  vitalilem5  22444  vitali  22445  mbfimaopnlem  22485  mbflimsup  22497  mbflimsupOLD  22498  0plef  22504  i1fima  22510  i1fima2  22511  i1fd  22513  itg1ge0  22518  itg10  22520  i1f1lem  22521  i1fadd  22527  i1fmul  22528  i1fmulc  22535  mbfi1fseqlem5  22551  itg2addlem  22590  reldv  22699  dvbsss  22731  dvef  22806  lhop1lem  22839  deg1fvi  22908  plypf1  23031  coeeulem  23043  coeeu  23044  vieta1lem2  23129  aannenlem3  23148  aalioulem3  23152  dvradcnv  23238  pserulm  23239  pserdvlem2  23245  abelthlem6  23253  sinhalfpilem  23280  sincos4thpi  23330  tan4thpi  23331  sincos6thpi  23332  pige3  23334  resinf1o  23347  tanord1  23348  tanregt0  23350  efabl  23361  relogrn  23373  dfrelog  23377  logneg  23399  logltb  23411  logcn  23454  logf1o2  23457  dvlog  23458  efopnlem2  23464  efopn  23465  logccv  23470  dvsqrt  23544  dvcnsqrt  23546  cxpcn3  23550  logblog  23591  angpined  23618  1cubr  23630  asinsin  23680  asin1  23682  reasinsin  23684  atan0  23696  atanbnd  23714  atan1  23716  log2cnv  23732  log2ublem3  23736  log2ub  23737  log2le1  23738  birthday  23742  amgmlem  23777  emcllem5  23787  emgt0  23794  harmonicbnd3  23795  ftalem3  23861  basellem4  23870  sgmf  23932  ppi1  23951  cht1  23952  vma1  23953  ppiltx  23964  sqff1o  23969  ppiublem1  23990  ppiublem2  23991  ppiub  23992  chtub  24000  dchreq  24046  bposlem7  24078  bposlem8  24079  bposlem9  24080  lgsdir2lem2  24112  lgsdir2lem3  24113  chebbnd1  24170  chto1ub  24174  chpo1ubb  24179  pntibndlem1  24287  tgldimor  24406  tglnfn  24449  axlowdimlem4  24818  axlowdimlem16  24830  axlowdim  24834  umgrafi  24892  usgraexmpl  24971  usgraexmplc  24974  usgrafilem1  24981  2trllemA  25122  wlkntrllem1  25131  wlkntrllem3  25133  0pth  25142  spthispth  25145  2pthon  25174  2pthon3v  25176  constr3trllem3  25222  constr3pthlem3  25227  konigsberg  25557  frgrawopreg2  25621  ex-dif  25715  ex-un  25716  ex-in  25717  ex-fl  25739  avril1  25742  ginvsn  25919  cnid  25921  mulid  25926  rngosn3  25996  vcoprnelem  26039  vcex  26041  cnnvm  26156  ipasslem8  26320  ipasslem10  26322  hvsubf  26500  normlem1  26595  normlem6  26600  normlem7  26601  norm-ii-i  26622  norm3adifii  26633  hilid  26646  hlimf  26722  hhssabloi  26745  hhssnv  26747  hhshsslem1  26750  shincli  26847  shsval2i  26872  shs0i  26934  chj0i  26940  chm1i  26941  chincli  26945  chdmm1i  26962  shjshsi  26977  chsup0  27033  h1de2bi  27039  spansnpji  27063  cmcmlem  27076  cmcmii  27082  cmcm2ii  27083  cmcm3ii  27084  pjidmi  27158  pjssmii  27166  pj0i  27178  pjocini  27183  mayetes3i  27214  df0op2  27237  hoaddcomi  27257  hoaddassi  27261  hocadddiri  27264  hocsubdiri  27265  hoaddid1i  27271  ho0coi  27273  hoid1i  27274  hoid1ri  27275  hodseqi  27279  honegsubi  27281  adj1o  27379  hoddii  27474  lnopunilem1  27495  lnopunilem2  27496  nmcopexi  27512  nmcopex  27514  nmcoplb  27515  nmcfnexi  27536  nmcfnex  27538  nmcfnlb  27539  adjbd1o  27570  adjcoi  27585  nmopcoadji  27586  opsqrlem6  27630  pjsdii  27640  pjddii  27641  pjidmcoi  27662  pjtoi  27664  pjin1i  27677  pjclem1  27680  stji1i  27727  reuxfr3d  27957  inindif  27983  iuninc  28012  fnresin  28065  rinvf1o  28067  suppss2fOLD  28074  suppss2f  28075  xppreima  28085  ofoprabco  28104  funcnvmptOLD  28107  gtiso  28118  df1stres  28121  df2ndres  28122  snct  28135  dmct  28138  padct  28147  ffsrn  28154  fpwrelmapffs  28159  xrge0infssd  28179  infxrge0lb  28182  infxrge0glb  28183  infxrge0gelb  28184  nnindf  28217  nn0min  28219  ressplusf  28246  xrsclat  28276  xrge0base  28281  xrge00  28282  xrge0neqmnf  28287  xrnarchi  28336  xrge0slmod  28443  locfinreflem  28503  locfinref  28504  unicls  28545  sqsscirc1  28550  mhmhmeotmd  28569  rmulccn  28570  raddcn  28571  xrge0iifiso  28577  xrge0iifhmeo  28578  lmxrge0  28594  cnzh  28610  rezh  28611  qqh0  28624  qqh1  28625  qqhre  28660  rrhre  28661  esumnul  28705  esum0  28706  esumsnf  28721  esumpfinvallem  28731  esumpfinvalf  28733  esumpcvgval  28735  esumcvgsum  28745  esumsup  28746  esumcvgre  28748  sigaclfu2  28779  dmsigagen  28802  ldgenpisyslem1  28821  ddemeas  28895  imambfm  28920  mbfmvolf  28924  br2base  28927  omsfval  28952  omsf  28954  oms0  28955  omssubaddlem  28957  omssubadd  28958  carsgclctunlem3  28978  sibfof  28998  sitg0  29004  eulerpartlemt  29027  eulerpartgbij  29028  0rrv  29107  coinfliplem  29134  coinflipprob  29135  coinfliprv  29138  ballotlem2  29144  ballotlem4  29154  ballotlem5  29155  ballotlemi1  29158  ballotlem7  29191  ballotth  29193  signsplypnf  29224  signsply0  29225  signsw0g  29230  signswch  29235  signsvf0  29254  bnj521  29330  bnj1098  29380  bnj1109  29383  bnj1131  29384  bnj1533  29448  bnj151  29473  bnj580  29509  bnj852  29517  bnj864  29518  bnj865  29519  bnj978  29545  bnj1021  29560  bnj907  29561  bnj1093  29574  bnj1145  29587  bnj1172  29595  bnj1174  29597  bnj1176  29599  bnj1186  29601  subfacf  29683  subfacp1lem1  29687  subfacp1lem5  29692  subfacp1lem6  29693  subfacval3  29697  erdszelem2  29700  kur14lem4  29717  iooscon  29755  iccllyscon  29758  msrfo  29969  mthmpps  30005  problem5  30086  quad3  30087  ghomgrpilem1  30088  ghomgrpilem2  30089  circum  30103  axextprim  30113  axrepprim  30114  axunprim  30115  axinfprim  30118  axacprim  30119  inffz  30147  logi  30154  bcneg1  30156  setinds  30208  dfon2lem2  30214  dfon2lem4  30216  axextdfeq  30228  poseq  30275  frrlem4  30301  nosgnn0  30329  sltsolem1  30339  bdayfo  30346  fobigcup  30449  snelsingles  30471  fullfunfnv  30495  fullfunfv  30496  rankaltopb  30528  rank0  30719  rankeq1o  30720  hfuni  30733  fneer  30791  neibastop1  30797  nabi1i  30834  nabi2i  30835  limsucncmpi  30887  bj-consensusALT  30939  bj-nfxfr  30994  bj-axsep  31156  bj-zfpow  31158  bj-dtru  31160  bj-sbieOLD  31193  bj-sbidmOLD  31194  bj-n0i  31286  bj-snsetex  31303  bj-tagss  31320  bj-2upln0  31363  bj-2upln1upl  31364  bj-nuliota  31368  bj-elid  31381  bj-pinftyccb  31405  bj-minftyccb  31409  bj-pinftynminfty  31411  f1omptsnlem  31469  mptsnunlem  31471  topdifinffinlem  31481  relowlpssretop  31498  imadifss  31632  tan2h  31641  poimirlem3  31647  poimirlem9  31653  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem22  31666  poimirlem30  31674  mblfinlem1  31681  mblfinlem2  31682  ovoliunnfl  31686  voliunnfl  31688  dvtanlemOLD  31695  itg2addnclem  31697  itg2addnclem2  31698  asindmre  31731  areacirclem1  31736  fdc  31778  cntotbnd  31832  heiborlem6  31852  rrnval  31863  reheibor  31875  prter2  32161  renegclALT  32244  mapdunirnN  34927  rntrclfvOAI  35242  diophrw  35310  rabren3dioph  35367  pellexlem6  35388  pellex  35389  frmx  35471  frmy  35472  jm2.23  35561  jm2.27dlem3  35576  axac10  35598  pw2f1ocnv  35602  kelac2lem  35632  lmhmlnmsplit  35655  pwfi2f1o  35664  frlmpwfi  35666  ifpbiidcor  35821  iunrelexp0  35937  dmtrclfvRP  35965  rntrclfv  35967  corcltrcl  35974  cotrclrcl  35977  0heALT  36020  frege54cor1a  36101  int-rightdistd  36268  int-sqdefd  36269  int-sqgeq0d  36274  seff  36298  expgrowthi  36323  expgrowth  36325  binomcxplemnotnn0  36346  ee233  36517  ax6e2nd  36566  in1  36583  dfvd2ani  36595  dfvd2i  36597  dfvd3i  36604  dfvd3ani  36607  e0bi  36807  uun2221  36844  uun2221p1  36845  uun2221p2  36846  en3lpVD  36885  relopabVD  36942  ax6e2ndVD  36949  ax6e2ndALT  36971  negpilt0  37103  ioontr  37200  iccdifioo  37205  iccdifprioo  37206  fsummulc1f  37226  fsumiunss  37233  icccncfext  37341  dvcosre  37357  dvsinax  37359  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvmptmulf  37385  dvnmul  37391  dvmptfprodlem  37392  dvnprodlem2  37395  stoweidlem1  37434  stoweidlem26  37459  stoweidlem34  37468  stoweidlem44  37478  stoweid  37498  stirlinglem5  37513  dirkercncflem1  37538  fourierdlem44  37586  fourierdlem56  37598  fourierdlem62  37604  fourierdlem89  37631  fourierdlem91  37633  fourierdlem100  37642  fourierdlem102  37644  fourierdlem103  37645  fourierdlem104  37646  fourierdlem108  37650  fourierdlem112  37654  fourierdlem114  37656  fouriersw  37667  gsumge0cl  37751  sge0tsms  37760  axorbtnotaiffb  37894  axorbciffatcxorb  37896  abnotbtaxb  37907  1nevenALTV  38223  nnsum3primes4  38286  evengpoap3  38297  tgblthelfgott  38311  tgoldbachlt  38312  resisresindm  38395  residfi  38401  ldepslinc  39075  3halfnz  39091  alimp-no-surprise  39294  aacllem  39314
  Copyright terms: Public domain W3C validator