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 583  pm4.71i 636  pm4.71ri 637  pm5.32i 644  pm5.16 666  pm5.19 668  pm5.55 674  biluk 744  3ori 884  nicodraw 951  19.35i 1075  19.36i 1078  exan 1105  sbco 1251  19.37aiv 1303  equsb3lem 1328  elsb3 1330  eqcomi 1477  eqtr 1493  eleqtr 1544  nemtbir 1639  nrex 1727  isseti 1812  vtocl2 1840  vtocl3 1841  eueq1 1914  euxfr2 1923  csbief 2029  ssid 2077  sseqtr 2090  3sstr3 2096  unssi 2202  ssini 2230  unabs 2235  inabs 2236  dfin4 2245  noel 2281  rab0 2290  difid 2331  difdisj 2334  ifor 2378  snid 2432  snsssn 2475  intab 2556  breqtr 2634  axrep1 2690  axsep 2698  bm1.3ii 2702  zfnuleu 2703  0nep0 2733  notzfaus 2737  axpow 2739  dtruALT 2744  dtru 2768  opprc1b 2792  uniop 2804  axun 2863  rabxfr 2898  reuxfr2 2899  op1stb 2909  fr0 2923  onunisuc 3102  omon 3139  relop 3271  dmsnsn0 3321  rn0 3351  dmresi 3395  cnvcnv 3482  cnvcnvres 3490  cocnvcnv2 3502  cores2 3503  co01 3505  isarep2 3574  fnopab 3613  f1cnv 3661  f1ovi 3713  fvprc 3716  fvopabn 3781  fvsnun2 3791  fopab 3822  xpsn 3830  fvi 3837  tfrlem13 3918  tz7.44-2 3924  tz7.44-3 3925  frfnom 3946  oprabss 4001  2nd0 4077  f1stres 4086  f2ndres 4087  foprab 4113  fnoprab2 4115  2on 4132  xp01disj 4136  oawordeulem 4181  oarec 4189  ersym 4265  ertr 4267  0nelqs 4291  dfdom2 4374  dmen 4397  ssdomg 4398  2dom 4417  sbthlem5 4440  mapdom2lem 4482  limensuci 4495  fiint 4543  abfii4 4547  pwfilem 4553  suc11reg 4588  axinf 4606  axinf2 4607  tz9.13 4646  rankval 4651  ssrankr1 4659  rankpw 4667  rankop 4676  rankeq0 4679  ranksuc 4683  rankelun 4690  rankxplim 4695  rankxplim3 4697  rankxpsuc 4698  cp 4705  bnd 4706  karden 4709  axac 4728  ac3 4730  ac5 4735  ac6lem 4737  brdom3 4784  card0 4806  cardom 4808  cardval 4809  card1 4816  cardlim 4834  alephsuc 4849  aleph1 4854  alephgeom 4865  unialeph 4878  cffnon 4890  cf0 4893  cfsuc 4898  pm110.643 4906  cdaassen 4913  zfcndrep 4949  zfcndpow 4951  zfcndac 4954  dmaddpi 5001  dmmulpi 5002  1lt2pi 5015  dmrecpq 5057  1lt2pq 5061  renegcl 5399  ine0 5417  ltxrltt 5483  renepnft 5520  renemnft 5521  renfdisj 5522  xrltnrt 5524  pnfnltt 5529  nltmnft 5530  mulnzcnopr 5681  divcan2 5695  eqneg 5770  negn0 5774  recgt0i 5780  posex 5866  nnsub 5913  halflt1 5987  lbinfm 6005  infmsup 6025  infmxrcl 6043  nn0mulcl 6079  nn0ltp1let 6084  nn0ssz 6109  elnnz1 6112  zltp1let 6138  nneo 6154  zeot 6156  uzrdgfnuz 6256  ser1cl2 6283  iccf 6347  dfioo2 6349  uzinfm 6407  limsupvalt 6474  sumsqne0 6579  nnlesq 6606  nnesq 6607  sqrlem1 6618  sqrlem2 6619  sqrlem10 6627  sqrlem11 6628  sqrlem15 6632  sqrlem16 6633  sqrlem19 6636  sqrlem20 6637  sqrmuli 6649  sqr2gt1lt2 6664  sqr2irrlem1 6669  inelr 6680  nthruc 6691  ipcn 6740  cjmulval 6742  reret 6749  re0 6770  im0 6771  re1 6772  im1 6773  cj0 6776  absgt0 6793  absid 6811  absi 6830  abstri 6844  abslem2i 6860  faclbnd4lem1 6900  bcpasc2 6920  bcpasc 6922  ser0mulc 7012  ser1mulc 7013  climunii 7051  climabslem 7101  climsup 7108  caucvg 7116  cvgcmpub 7138  isumcmpi 7167  isumsplit 7168  isum0split 7169  infcvglem1 7173  fnsmntlem 7177  fnsmnt 7178  expcnvlem1 7179  expcnvlem2 7180  expcnvlem4 7182  geolimilem 7187  geolim1i 7190  0.999... 7198  negfcncf 7221  ivthlem6 7238  ivthlem7 7239  ivthlem8 7240  dsupivthlem 7243  ivthlem6OLD 7247  ivthlem7OLD 7248  ivthlem8OLD 7249  ivthOLD 7250  ivth2OLD 7251  efcltlem1 7263  dfef2 7266  reefcl 7276  ele3lem 7285  ege2lem2 7287  ege2le3lem2 7288  efaddlem7 7303  efaddlem8 7304  efaddlem10 7306  efaddlem12 7308  efaddlem20 7316  efaddlem22 7318  efne0t 7328  eftlexOLD 7336  ef1tllem 7340  ef01tllem1 7342  ef01tllem2 7343  absef01tllem 7345  eirrlem1 7347  eirrlem3 7349  eirrlem4 7350  efsep 7354  effsumle 7355  efgt0 7362  efm1lim 7368  eflegeolem2 7371  efm1legeo 7374  efcnlem1 7376  efcnlem2 7377  reeff1o 7385  reeff1o2 7386  sin0ALT 7404  sin01bndlem1 7426  cos01bndlem2 7429  cos2bnd 7434  sin01gt0 7435  cos01gt0 7436  sincos2sgn 7439  sin4lt0 7440  acdc2lem2 7448  acdc5lem2 7451  ruclem6 7475  ruclem8 7477  ruclem17 7486  ruclem25 7494  ruclem26 7495  ruclem27 7496  infdif 7528  remetba 7871  dscmet 7880  xplm 7937  bcthlem33 7993  bcth 7994  isgrp2i 8038  cnid 8091  mulid 8096  ghgrpilem1 8097  ghgrpilem2 8098  ghgrpilem3 8099  ghgrpilem4 8100  ghsubgi 8102  vcoprnelem 8161  vcoprne 8162  vcex 8163  cnnvm 8277  ip1cnilem2 8336  ip1cnilem6 8340  ipasslem6 8454  ipasslem8 8456  ipasslem10 8458  minveclem14 8517  sincolem 8619  pilem1 8625  pilem2 8626  pilem3 8627  pigt2lt4 8629  sinhalfpilem 8633  sincos4thpi 8662  sincos6thpi 8663  cosh111lem1 8664  cosh111t 8667  efghgrpilem 8669  efifolem1 8672  efifolem2 8673  efifolem3 8674  efifolem4 8675  efifolem6 8677  efif1lem5 8684  efif1lem6 8685  efif1lem7 8686  logrn 8706  resslogrn 8708  dfrelog 8711  pilog 8723  logltbt 8731  axgroth4 8735  grothprim 8738  avril1 8739  normlem1 8931  normlem6 8936  normlem7 8937  norm-ii 8959  hilid 8983  hilnorm 8985  hlimunii 9063  norm1ex 9077  hhssabl 9087  hhssnv 9089  hhshsslem1 9092  projlem3 9143  projlem5 9145  projlem12 9152  projlem14 9154  projlem15 9155  projlem18 9158  projlemHIL 9173  shincl 9286  shsumval2 9315  shs0 9327  chj0 9333  chincl 9338  chdmm1 9355  shjshs 9370  chsup0 9426  spansnpj 9458  cmcmlem 9491  cmcmi 9497  cmcm2i 9498  cmcm3i 9499  pjidm 9574  pjssm 9583  pj0 9595  pjocin 9600  pjrn 9604  df0op2 9635  hoaddcom 9655  hoaddass 9659  hocadddir 9662  hocsubdir 9663  hoaddid1 9669  ho0co 9671  hoid1 9672  hoid1r 9673  hodseq 9677  honegsub 9679  adj1o 9775  hoddi 9870  lnopunilem1 9891  lnopunilem2 9892  nmcopexlem2 9908  nmcopext 9915  nmcoplbt 9916  nmcfnexlem2 9937  nmcfnext 9944  nmcfnlbt 9945  adjbd1o 9974  adjco 9989  nmopcoadj 9990  pjsdi 10039  pjddi 10040  pjidmco 10061  pjtot 10063  pjin1 10076  pjclem1 10079  stji1 10125  large 10150  ghomgrpilem1 10341  ghomgrpilem2 10342  cayleylem2 10366  cayleylem3 10367  ump 10413  cmpfun 10421  fgsb 10503  fgsb2 10508  cnfilca 10510  rcfpfillem5 10515  clicls 10538  stoi 10555  relrded 10591  relrcat 10612

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