Theorem mpbi 189

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	biimp 151	. 2 |- (ph -> ps)
4	1, 3	ax-mp 7	1 |- ps

Syntax hints:   <-> wb 146

This theorem is referenced by:  mtbi 191  ori 230  ex 373  pm5.74i 584  pm4.71i 637  pm4.71ri 638  pm5.32i 645  pm5.16 667  pm5.19 669  pm5.55 675  biluk 745  3ori 885  nicodraw 952  19.35i 1076  19.36i 1079  exan 1106  sbco 1252  19.37aiv 1304  equsb3lem 1329  elsb3 1331  eqcomi 1479  eqtr 1495  eleqtr 1546  nemtbir 1641  nrex 1729  isseti 1815  vtocl2 1843  vtocl3 1844  eueq1 1917  euxfr2 1926  csbief 2032  ssid 2080  sseqtr 2093  3sstr3 2099  unssi 2205  ssini 2233  unabs 2238  inabs 2239  dfin4 2248  noel 2284  rab0 2293  difid 2334  difdisj 2337  ifor 2381  snid 2435  snsssn 2478  intab 2560  breqtr 2638  axrep1 2694  axsep 2702  bm1.3ii 2706  zfnuleu 2707  0nep0 2737  notzfaus 2741  axpow 2743  dtruALT 2748  dtru 2772  opprc1b 2796  uniop 2808  axun 2867  rabxfr 2902  reuxfr2 2903  op1stb 2913  fr0 2927  onunisuc 3106  omon 3143  relop 3275  dmsnsn0 3325  rn0 3355  dmresi 3399  cnvcnv 3486  cnvcnvres 3494  cocnvcnv2 3506  cores2 3507  co01 3509  isarep2 3578  fnopab 3617  f1cnv 3666  f1ovi 3718  fvprc 3721  fvopabn 3786  fvsnun2 3796  fopab 3827  xpsn 3835  fvi 3842  tfrlem13 3923  tz7.44-2 3929  tz7.44-3 3930  frfnom 3951  oprabss 4006  2nd0 4084  f1stres 4093  f2ndres 4094  foprab 4120  fnoprab2 4122  2on 4139  xp01disj 4143  oawordeulem 4188  oarec 4196  ersym 4272  ertr 4274  0nelqs 4298  dfdom2 4384  dmen 4407  ssdomg 4408  2dom 4427  sbthlem5 4451  mapdom2lem 4493  limensuci 4506  fiint 4559  fiintOLD 4560  abfii4OLD 4564  pwfilemOLD 4570  suc11reg 4605  axinf 4623  axinf2 4624  tz9.13 4663  rankval 4668  ssrankr1 4676  rankpw 4684  rankop 4693  rankeq0 4696  ranksuc 4700  rankelun 4707  rankxplim 4712  rankxplim3 4714  rankxpsuc 4715  cp 4722  bnd 4723  karden 4726  axac 4745  ac3 4747  ac5 4752  ac6lem 4754  brdom3 4801  card0 4823  cardom 4825  cardval 4826  card1 4833  cardlim 4851  alephsuc 4866  aleph1 4871  alephgeom 4882  unialeph 4895  cffnon 4907  cf0 4910  cfsuc 4915  pm110.643 4923  cdaassen 4930  zfcndrep 4966  zfcndpow 4968  zfcndac 4971  dmaddpi 5018  dmmulpi 5019  1lt2pi 5032  dmrecpq 5074  1lt2pq 5078  renegcl 5416  ine0 5434  ltxrltt 5500  renepnft 5537  renemnft 5538  renfdisj 5539  xrltnrt 5541  pnfnltt 5546  nltmnft 5547  mulnzcnopr 5702  divcan2 5716  divcan2OLD 5720  eqneg 5804  negn0 5808  recgt0i 5814  posex 5908  nnsub 5956  halflt1 6030  lbinfm 6048  infmsup 6068  infmxrcl 6086  nn0mulcl 6122  nn0ltp1let 6127  nn0ssz 6152  elnnz1 6155  zltp1let 6181  nneo 6197  zeot 6199  uzrdgfnuz 6306  ser1cl2 6333  iccf 6401  dfioo2 6403  uzinfm 6462  limsupvalt 6529  sumsqne0 6634  nnlesq 6661  nnesq 6662  sqrlem1 6673  sqrlem2 6674  sqrlem10 6682  sqrlem11 6683  sqrlem15 6687  sqrlem16 6688  sqrlem19 6691  sqrlem20 6692  sqrmuli 6704  sqr2gt1lt2 6719  sqr2irrlem1 6724  inelr 6735  nthruc 6745  ipcn 6790  cjmulval 6792  re0 6820  im0 6821  re1 6822  im1 6823  cj0 6826  absid 6861  absi 6878  abstri 6891  abslem2i 6908  faclbnd4lem1 6948  bcpasc2 6967  bcpasc 6969  ser0mulc 7059  ser1mulc 7060  climunii 7098  climabslem 7148  climsup 7155  caucvg 7163  cvgcmpub 7185  isumcmpi 7215  isumsplit 7216  isum0split 7217  infcvglem1 7221  fnsmntlem 7225  fnsmnt 7226  expcnvlem1 7227  expcnvlem2 7228  expcnvlem4 7230  geolimilem 7235  geolim1i 7238  0.999... 7246  negfcncf 7269  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  dsupivthlem 7291  efcltlem1 7304  dfef2 7307  reefcl 7317  ele3lem 7326  ege2lem2 7328  ege2le3lem2 7329  efaddlem7 7344  efaddlem8 7345  efaddlem10 7347  efaddlem12 7349  efaddlem20 7357  efaddlem22 7359  efne0t 7369  eftlexOLD 7377  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tllem 7387  eirrlem1 7389  eirrlem3 7391  eirrlem4 7392  efsep 7396  effsumle 7397  efgt0 7404  efm1lim 7411  eflegeolem2 7414  efm1legeo 7417  efcnlem1 7419  efcnlem2 7420  reeff1o 7426  reeff1o2 7427  sin0ALT 7445  sin01bndlem1 7467  cos01bndlem2 7470  cos2bnd 7475  sin01gt0 7476  cos01gt0 7477  sincos2sgn 7480  sin4lt0 7481  acdc2lem2 7489  acdc5lem2 7492  ruclem6 7515  ruclem8 7517  ruclem17 7526  ruclem25 7534  ruclem26 7535  ruclem27 7536  infdif 7568  remetba 7909  dscmet 7918  xplm 7975  bcthlem33 8031  bcth 8032  isgrp2i 8076  cnid 8127  mulid 8132  ghgrpilem1 8133  ghgrpilem2 8134  ghgrpilem3 8135  ghgrpilem4 8136  ghsubgi 8138  vcoprnelem 8197  vcoprne 8198  vcex 8199  cnnvm 8313  ip1cnilem2 8374  ip1cnilem6 8378  ipasslem6 8495  ipasslem8 8497  ipasslem10 8499  minveclem14 8558  sincolem 8665  pilem1 8671  pilem2 8672  pilem3 8673  pigt2lt4 8675  sinhalfpilem 8679  sincos4thpi 8710  sincos6thpi 8711  cosh111lem1 8714  cosh111t 8717  efghgrpilem 8719  efifolem1 8722  efifolem2 8723  efifolem3 8724  efifolem4 8725  efifolem6 8727  efif1lem5 8734  efif1lem6 8735  efif1lem7 8736  logrn 8751  resslogrn 8753  dfrelog 8756  pilog 8768  logltbt 8776  axgroth4 8780  grothprim 8783  avril1 8784  normlem1 8976  normlem6 8981  normlem7 8982  norm-ii 9004  norm3adif 9015  hilid 9028  hilnorm 9030  hlimunii 9108  norm1ex 9122  hhssabl 9132  hhssnv 9134  hhshsslem1 9137  projlem3 9188  projlem5 9190  projlem12 9197  projlem14 9199  projlem15 9200  projlem18 9203  projlemHIL 9218  shincl 9331  shsumval2 9360  shs0 9372  chj0 9378  chincl 9383  chdmm1 9400  shjshs 9415  chsup0 9471  spansnpj 9501  cmcmlem 9534  cmcmi 9540  cmcm2i 9541  cmcm3i 9542  pjidm 9617  pjssm 9626  pj0 9638  pjocin 9643  pjrn 9647  df0op2 9678  hoaddcom 9698  hoaddass 9702  hocadddir 9705  hocsubdir 9706  hoaddid1 9712  ho0co 9714  hoid1 9715  hoid1r 9716  hodseq 9720  honegsub 9722  adj1o 9818  hoddi 9914  lnopunilem1 9935  lnopunilem2 9936  nmcopexlem2 9952  nmcopext 9959  nmcoplbt 9960  nmcfnexlem2 9981  nmcfnext 9988  nmcfnlbt 9989  adjbd1o 10018  adjco 10033  nmopcoadj 10034  pjsdi 10083  pjddi 10084  pjidmco 10105  pjtot 10107  pjin1 10120  pjclem1 10123  stji1 10169  large 10194  ghomgrpilem1 10385  ghomgrpilem2 10386  cayleylem2 10410  cayleylem3 10411  ump 10459  cmpfun 10467  top2usne 10549  fgsb 10570  fgsbOLD 10571  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem5 10593  rcfpfillem5OLD 10594  clicls 10622  stoi 10639  relrded 10675  relrcat 10696

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 147

Copyright terms: Public domain