Theorem mpbi 205

Description: An inference from a biconditional, related to modus ponens.

Hypotheses

Ref	Expression
mpbi.min	|- ph
mpbi.maj	|- (ph <-> ps)

Assertion

Ref	Expression
mpbi	|- ps

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 |- ph
2		mpbi.maj	. . 3 |- (ph <-> ps)
3	2	biimpi 167	. 2 |- (ph -> ps)
4	1, 3	ax-mp 7	1 |- ps

Syntax hints:   <-> wb 162

This theorem is referenced by:  mtbi 207  ori 246  ex 400  pm5.74i 641  pm4.71i 696  pm4.71ri 697  pm5.32i 704  pm5.16 727  pm5.19 729  pm5.55 736  biluk 814  3ori 1004  nic-dfim 1082  nic-dfneg 1083  nic-mp 1084  nic-mpALT 1085  notfal 1112  3impexpbicomi 1130  mpgbi 1171  19.35i 1265  19.36i 1268  exanOLD 1302  sbco 1463  sbidm 1465  19.37aiv 1522  equsb3lemOLD 1554  elsb3 1556  elsb3OLD 1557  elsb4 1558  elsb4OLD 1559  eqcomi 1725  eqtri 1745  eleqtri 1806  eqsb3lemOLD 1825  clelsb3 1827  clelsb3OLD 1828  nemtbir 1934  nrex 2026  r19.23ai 2043  isseti 2130  vtocl2 2173  vtocl2OLD 2174  vtocl3 2175  vtocl3OLD 2176  eueq1 2261  euxfr2 2270  csbiefOLD 2410  ssidOLD 2468  sseqtri 2482  3sstr3i 2488  pssn2lp 2541  unssi 2611  ssini 2643  unabs 2649  inabs 2650  dfin4 2662  noel 2705  rab0OLD 2717  npss0 2735  difid 2766  difdisj 2769  difin0 2770  inundifOLD 2776  iforOLD 2833  snid 2893  snsssn 2970  unissintOLD 3064  intab 3069  iinrab2 3140  breqtri 3180  axrep1 3244  axsep 3252  bm1.3ii 3256  zfnuleu 3257  0nep0 3289  notzfaus 3293  zfpow 3297  dtru 3313  dtruALT 3332  copsexg 3352  opprc1b 3357  uniop 3370  fr0 3451  onunisuci 3594  zfun 3602  reuxfr2d 3655  reuxfr2 3656  op1stb 3668  omon 3774  relop 3924  rn0 4014  dmresi 4068  cnvcnv 4170  rescnvcnv 4196  cnvcnvres 4198  cocnvcnv2 4220  cores2 4221  co01 4223  isarep2 4310  fnopab 4359  f1cnv 4422  f1ovi 4484  fvprc 4489  fvopabn 4560  fvsnun2 4576  fopab 4611  xpsn 4619  fvi 4629  oprabss 4746  2nd0 4836  f1stres 4845  f2ndres 4846  foprab 4873  fnoprab2 4875  df1st2 4879  df2nd2 4880  fparlem3 4894  fparlem4 4895  iota4an 4912  tfrlem13 4942  tz7.44-2 4948  tz7.44-3 4949  frfnom 4970  2onOLD 4995  xp01disj 4999  oawordeulem 5047  oarec 5055  ersym 5141  ertr 5143  dfdom2 5254  dmen 5277  ssdomg 5278  2dom 5297  sbthlem5 5325  mapdom2lem 5397  limensuci 5410  fiint 5460  abfii4 5464  pwfilem 5470  suc11reg 5520  zfinf 5538  axinf2 5539  tz9.13 5583  rankval 5588  ssrankr1 5596  rankpw 5604  rankop 5613  rankeq0 5616  ranksuc 5620  rankelun 5627  rankxplim 5632  rankxplim3 5634  rankxpsuc 5635  cp 5648  bnd 5649  karden 5652  card0 5665  cardom 5668  omsubsuc 5673  omsubsuc2 5674  elomsubsd 5681  zfac 5703  ac3 5705  ac5 5710  ac6lem 5712  brdom3 5759  cardval 5771  card1 5779  cardlim 5799  alephsuc 5810  aleph1 5815  alephgeom 5826  unialeph 5839  cffnon 5851  cf0 5854  cfsuc 5859  pm110.643 5868  cdaassen 5876  zfcndrep 5914  zfcndpow 5916  zfcndac 5919  dmaddpi 5966  dmmulpi 5967  1lt2pi 5980  dmrecpq 6022  1lt2pq 6026  subcli 6319  negnegi 6345  renegcliOLD 6373  ine0 6393  negdii 6407  ltxrlt 6465  renepnf 6504  renepnfOLD 6505  renemnf 6506  renemnfOLD 6507  renfdisjOLD 6509  ssxr 6510  xrltnr 6512  pnfnlt 6517  nltmnf 6518  mulnzcnopr 6687  divcli 6695  divcan2i 6701  eqnegi 6777  negne0i 6781  recgt0ii 6787  posexi 6886  nnsubi 6935  halflt1 7011  lbinfm 7052  infmsup 7072  infmxrcl 7090  nn0mulcli 7126  nn0ltp1le 7131  nn0ssz 7156  elnnz1 7159  zltp1le 7185  nneoi 7204  zeo 7206  iccf 7365  dfioo2 7367  uzinfmi 7426  uzrdgfnuzi 7513  cardfz 7514  ser1cl2i 7541  limsupval 7567  sumsqne0i 7674  nnlesqi 7706  nnesqi 7707  sqrlem1 7718  sqrlem2 7719  sqrlem10 7727  sqrlem11 7728  sqrlem15 7732  sqrlem16 7733  sqrlem19 7736  sqrlem20 7737  sqrmulii 7749  sqr2gt1lt2 7764  sqr2irrlem1 7769  inelr 7780  nthruc 7790  ipcni 7835  cjmulvali 7837  re0 7865  im0 7866  re1 7867  im1 7868  cj0 7871  absidi 7907  absi 7925  abstrii 7938  abslem2i 7955  faclbnd4lem1 7995  bcpasc2i 8014  bcpasci 8016  hashgval 8025  ser0mulci 8114  ser1mulci 8115  climunii 8153  climabslem 8203  climsupi 8210  caucvgi 8218  cvgcmpubi 8241  isumcmpii 8271  isumspliti 8272  isum0spliti 8273  infcvglem1 8277  arisumilem 8281  arisumi 8282  expcnvlem1 8283  expcnvlem2 8284  expcnvlem4 8286  geolimilem 8292  geolim1i 8295  0.999... 8303  negfcncfi 8326  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  dsupivthlem 8348  efcltlem1 8361  dfef2i 8364  reefcli 8374  ele3lem 8383  ege2lem2 8385  ege2le3lem2 8386  efaddlem7 8401  efaddlem8 8402  efaddlem10 8404  efaddlem12 8406  efaddlem20 8414  efaddlem22 8416  efne0 8426  eftlexiOLD 8434  ef1tllem 8438  ef01tllem1 8440  ef01tllem2 8441  ef01tllem2OLD 8442  absef01tllem 8444  eirrlem1 8446  eirrlem3 8448  eirrlem4 8449  egt2OLD 8452  elt3OLD 8453  egt2lt3 8454  efsepi 8456  effsumlei 8457  efgt0i 8464  efm1limi 8471  eflegeolem2 8474  efm1legeoi 8477  efcnlem1 8479  efcnlem2 8480  reeff1o 8486  reeff1o2 8487  sin0ALT 8505  sin01bndlem1 8528  cos01bndlem2 8531  cos2bnd 8536  sin01gt0 8537  cos01gt0 8538  sincos2sgn 8541  sin4lt0 8542  acdc2lem2 8553  acdc5lem2 8556  ruclem6 8579  ruclem8 8581  ruclem17 8590  ruclem25 8598  ruclem26 8599  ruclem27 8600  infdif 8632  remetba 8982  dscmet 8991  xplm 9048  bcthlem33 9104  bcth 9105  isgrp2i 9155  cnid 9230  mulid 9235  ghgrpilem1 9236  ghgrpilem2 9237  ghgrpilem3 9238  ghgrpilem4 9239  ghsubgi 9241  gapm 9257  vcoprnelem 9324  vcoprne 9325  vcex 9326  cnnvm 9440  ip1cnilem2 9508  ip1cnilem6 9512  ipasslem6 9631  ipasslem8 9633  ipasslem10 9635  minveclem14 9698  sincolem 9809  pilem1 9815  pilem2 9816  pilem3 9817  pigt2lt4 9819  sinhalfpilem 9823  sincos4thpi 9855  sincos6thpi 9856  cosh111lem1 9863  cosh111 9866  efghgrpilem 9868  efifolem1 9871  efifolem2 9872  efifolem3 9873  efifolem4 9874  efifolem6 9876  efif1lem5 9883  efif1lem6 9884  efif1lem7 9885  logrn 9900  resslogrn 9902  dfrelog 9905  pilog 9917  logltb 9925  grothpw 9929  axgroth4 9934  grothprim 9936  avril1 9937  clicls 9976  stoiglem 10042  fsubbas 10073  normlem1 10401  normlem6 10406  normlem7 10407  norm-ii.i 10429  norm3adifii 10440  hilid 10453  hilnormi 10455  hlimuniii 10533  norm1exi 10547  hhssabli 10557  hhssnv 10559  hhshsslem1 10562  projlem3 10613  projlem5 10615  projlem12 10622  projlem14 10624  projlem15 10625  projlem18 10628  projlemHIL 10643  shincli 10756  shsumval2i 10785  shs0i 10797  chj0i 10803  chincli 10808  chdmm1i 10825  shjshsi 10840  chsup0 10896  spansnpji 10926  cmcmlem 10959  cmcmii 10965  cmcm2ii 10966  cmcm3ii 10967  pjidmi 11044  pjssmii 11053  pj0i 11065  pjocini 11070  pjrni 11074  mayetes3i 11102  df0op2 11107  hoaddcomi 11127  hoaddassi 11131  hocadddiri 11134  hocsubdiri 11135  hoaddid1i 11141  ho0coi 11143  hoid1i 11144  hoid1ri 11145  hodseqi 11149  honegsubi 11151  adj1o 11247  hoddii 11343  lnopunilem1 11364  lnopunilem2 11365  nmcopexlem2 11381  nmcopex 11388  nmcoplb 11389  nmcfnexlem2 11410  nmcfnex 11417  nmcfnlb 11418  adjbd1o 11447  adjcoi 11462  nmopcoadji 11463  opsqrlem6 11508  pjsdii 11519  pjddii 11520  pjidmcoi 11541  pjtoi 11543  pjin1i 11557  pjclem1 11560  stji1i 11606  largei 11631  bnj90OLD 12238  bnj100 12241  bnj99 12242  bnj521 12314  bnj584 12342  bnj586 12344  bnj598 12351  bnj614 12359  bnj853 12579  bnj856 12581  bnj857 12582  bnj861 12586  bnj895 12605  bnj901 12610  bnj979 12655  bnj997 12665  bnj1025 12672  bnj1050 12681  bnj1060 12689  bnj1079 12698  bnj1092 12705  bnj1130 12725  bnj1131 12726  bnj1166 12750  bnj1181 12755  bnj1225 12789  bnj1306 12841  bnj1310 12842  bnj1492 12953  bnj151 13035  bnj515 13048  bnj609 13098  bnj894 13119  bnj1008 13165  bnj1021 13172  bnj1172 13232  bnj1174 13234  bnj1497 13352  fz1eqblem 13400  ghomgrpilem1 13420  ghomgrpilem2 13421  cayleylem2 13434  cayleylem3 13435  dvdslelem 13484  divalglem1 13489  divalglem5 13492  divalglem6 13493  divalglem10 13497  eucalgf 13543  isprm2 13567  2prm 13571  4nprm 13573  axextprim 13577  axrepprim 13578  axunprim 13579  axinfprim 13582  axacprim 13583  setinds 13635  dfon2lem2 13641  dfon2lem4 13643  axextdfeq 13654  frxp 13743  poseq 13746  wfrlem4 13752  noxpsgn 13782  sltval2 13789  nosgnn0 13791  axsltsolem1 13796  axbday 13802  TFBid 13851  nabi1i 13871  nabi2i 13872  tbw-negdf 13896  rb-imdf 13947  rb-ax1 13949  meran1 13965  meran2 13966  meran3 13967  ump 14077  vxveqv 14085  ref3w 14094  prj1 14125  r1subsuc 14169  uncum 14170  cmprelid2 14177  cmpfun 14207  cmpdom2 14209  cbicplem 14234  nZdef 14253  domrancur1b 14274  domncnt 14348  ranncnt 14349  toplat 14364  rrisgrp 14421  top2usne 14618  fgsb 14635  fgsb2 14639  cnfilca 14641  rcfpfillem5 14646  trhom 14697  stoi 14708  cntrsetlem 14709  relrded 14771  relrcat 14792  tarval2 14931  omsubsucOLD 15068  omsubsuc2OLD 15069  elomsubsdOLD 15076  cnsubsp2 15109  compsublem 15112  compfipin0 15118  fneerdm 15180  neibastop2lem1 15201  fbasfip 15238  ufileu 15255  filufint 15256  prfunOLD 15359  opelopab3 15370  fimax 15428  infmrlb 15447  infmrgelb 15448  divexp 15461  fz10 15470  fdc 15494  fsumltisumii 15504  fsumltisumi 15505  fsumleisumii 15507  fsumleisumi 15508  csbrni 15514  trirni 15515  trirn 15516  piececn 15576  cnoprab1 15603  cnoprab2 15604  heiborlem9 15645  heiborlem11 15647  heiborlem16 15652  heiborlem17 15653  heiborlem18 15654  heiborlem33 15669  heiborlem40 15676  heiborlem41 15677  rrncms 15701  rrntotbnd 15704  reparphtlem2 15746  pcocn 15758  pcopt 15766  pcoass 15767  pcorev 15769  prter2 15967  ltfrn 16120  smo0 16131  smoge 16136  in1 16139  dfvd2i 16149  dfvd3i 16154  e0bi 16297  en3lpVD 16328  stb2xpl 16501  stb3xpl 16502  divrngmclNEW 16893  invrcl 16900

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 163

Copyright terms: Public domain