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 582  pm4.71i 635  pm4.71ri 636  pm5.32i 643  pm5.16 665  pm5.19 667  pm5.55 673  biluk 743  3ori 882  nicodraw 949  19.35i 1072  19.36i 1075  exan 1102  sbco 1247  19.37aiv 1299  equsb3lem 1324  elsb3 1326  eqcomi 1471  eqtr 1487  eleqtr 1538  nemtbir 1633  nrex 1721  isseti 1806  vtocl2 1834  vtocl3 1835  eueq1 1908  euxfr2 1916  csbief 2022  ssid 2070  sseqtr 2083  3sstr3 2089  unssi 2195  ssini 2223  unabs 2228  inabs 2229  dfin4 2238  noel 2274  rab0 2283  difid 2324  difdisj 2327  ifor 2371  snid 2425  snsssn 2469  intab 2550  breqtr 2628  axrep1 2684  axsep 2692  bm1.3ii 2696  zfnuleu 2697  0nep0 2727  notzfaus 2731  axpow 2733  dtruALT 2738  dtru 2762  opprc1b 2786  uniop 2797  axun 2858  rabxfr 2892  reuxfr2 2893  op1stb 2903  fr0 2917  onunisuc 3096  omon 3133  relop 3265  dmsnsn0 3314  rn0 3341  dmresi 3383  cnvcnv 3472  cnvcnvres 3480  cocnvcnv2 3492  cores2 3493  co01 3495  isarep2 3564  fnopab 3603  f1cnv 3651  f1ovi 3703  fvprc 3706  fvopabn 3771  fvsnun2 3781  fopab 3812  xpsn 3820  fvi 3827  tfrlem13 3908  tz7.44-2 3914  tz7.44-3 3915  frfnom 3936  oprabss 3991  2nd0 4068  f1stres 4077  f2ndres 4078  foprab 4104  fnoprab2 4106  2on 4123  xp01disj 4127  oawordeulem 4172  oarec 4180  ersym 4256  ertr 4258  0nelqs 4282  dfdom2 4365  dmen 4388  ssdomg 4389  2dom 4408  sbthlem5 4431  mapdom2lem 4473  limensuci 4486  fiint 4534  abfii4 4538  pwfilem 4544  suc11reg 4577  axinf 4595  axinf2 4596  tz9.13 4635  rankval 4640  ssrankr1 4648  rankpw 4656  rankop 4665  rankeq0 4668  ranksuc 4672  rankelun 4679  rankxplim 4684  rankxplim3 4686  rankxpsuc 4687  cp 4694  bnd 4695  karden 4698  axac 4717  ac3 4719  ac5 4724  ac6lem 4726  brdom3 4773  card0 4795  cardom 4797  cardval 4798  card1 4805  cardlim 4823  alephsuc 4838  aleph1 4843  alephgeom 4854  unialeph 4867  cffnon 4879  cf0 4882  cfsuc 4887  pm110.643 4895  cdaassen 4902  zfcndrep 4938  zfcndpow 4940  zfcndac 4943  dmaddpi 4990  dmmulpi 4991  1lt2pi 5004  dmrecpq 5046  1lt2pq 5050  renegcl 5388  ine0 5406  ltxrltt 5472  renepnft 5510  renemnft 5511  renfdisj 5512  xrltnrt 5514  pnfnltt 5519  nltmnft 5520  mulnzcnopr 5671  divcan2 5685  eqneg 5760  negn0 5764  recgt0i 5770  posex 5856  nnsub 5903  halflt1 5977  lbinfm 5995  infmsup 6015  infmxrcl 6033  nn0mulcl 6069  nn0ltp1let 6074  nn0ssz 6099  elnnz1 6102  zltp1let 6128  nneo 6144  zeot 6146  uzrdgfnuz 6243  ser1cl2 6270  iccf 6334  dfioo2 6336  uzinfm 6394  limsupvalt 6461  sumsqne0 6565  nnlesq 6591  nnesq 6592  sqrlem1 6603  sqrlem2 6604  sqrlem10 6612  sqrlem11 6613  sqrlem15 6617  sqrlem16 6618  sqrlem19 6621  sqrlem20 6622  sqrmuli 6634  sqr2gt1lt2 6649  sqr2irrlem1 6654  inelr 6665  nthruc 6676  ipcn 6725  cjmulval 6727  reret 6734  re0 6755  im0 6756  re1 6757  im1 6758  cj0 6761  absgt0 6778  absid 6796  absi 6815  abstri 6829  abslem2i 6845  faclbnd4lem1 6885  bcpasc2 6905  bcpasc 6907  ser0mulc 6997  ser1mulc 6998  climunii 7035  climabslem 7084  climsup 7091  caucvg 7099  cvgcmpub 7121  isumcmpi 7150  isumsplit 7151  isum0split 7152  infcvglem1 7156  fnsmntlem 7160  fnsmnt 7161  expcnvlem1 7162  expcnvlem2 7163  expcnvlem4 7165  geolimilem 7170  geolim1i 7173  0.999... 7181  negfcncf 7204  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  dsupivthlem 7226  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivthOLD 7233  ivth2OLD 7234  efcltlem1 7246  dfef2 7249  reefcl 7259  ele3lem 7268  ege2lem2 7270  ege2le3lem2 7271  efaddlem7 7286  efaddlem8 7287  efaddlem10 7289  efaddlem12 7291  efaddlem20 7299  efaddlem22 7301  efne0t 7311  eftlexOLD 7319  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  absef01tllem 7328  eirrlem1 7330  eirrlem3 7332  eirrlem4 7333  efsep 7337  effsumle 7338  efgt0 7345  efm1lim 7351  eflegeolem2 7354  efm1legeo 7357  efcnlem1 7359  efcnlem2 7360  reeff1o 7368  reeff1o2 7369  sin0ALT 7387  sin01bndlem1 7409  cos01bndlem2 7412  cos2bnd 7417  sin01gt0 7418  cos01gt0 7419  sincos2sgn 7422  sin4lt0 7423  acdc2lem2 7431  acdc5lem2 7434  ruclem6 7458  ruclem8 7460  ruclem17 7469  ruclem25 7477  ruclem26 7478  ruclem27 7479  infdif 7511  remetba 7848  dscmet 7856  xplm 7909  bcthlem33 7965  bcth 7966  isgrp2i 8011  cnid 8064  mulid 8069  ghgrpilem1 8070  ghgrpilem2 8071  ghgrpilem3 8072  ghgrpilem4 8073  ghsubgi 8075  vcoprnelem 8135  vcoprne 8136  vcex 8137  cnnvm 8251  ip1cnilem2 8308  ip1cnilem6 8312  ipasslem6 8426  ipasslem8 8428  ipasslem10 8430  minveclem14 8489  sincolem 8584  pilem1 8590  pilem2 8591  pilem3 8592  pigt2lt4 8594  sinhalfpilem 8598  sincos4thpi 8627  sincos6thpi 8628  cosh111lem1 8629  cosh111t 8632  efghgrpilem 8634  efifolem1 8637  efifolem2 8638  efifolem3 8639  efifolem4 8640  efifolem6 8642  efif1lem5 8649  efif1lem6 8650  efif1lem7 8651  logrn 8673  resslogrn 8675  dfrelog 8678  pilog 8690  logltbt 8698  dflog2OLD 8701  logltbtOLD 8715  axgroth4 8719  grothprim 8722  avril1 8723  normlem1 8897  normlem6 8902  normlem7 8903  norm-ii 8925  hilid 8949  hilnorm 8951  hlimunii 9029  norm1ex 9043  hhssabl 9053  hhssnv 9054  hhshsslem1 9057  projlem3 9104  projlem5 9106  projlem12 9113  projlem14 9115  projlem15 9116  projlem18 9119  shincl 9246  shsumval2 9275  shs0 9287  chj0 9293  chincl 9298  chdmm1 9315  shjshs 9330  chsup0 9386  spansnpj 9418  cmcmlem 9451  cmcmi 9457  cmcm2i 9458  cmcm3i 9459  pjidm 9534  pjssm 9543  pj0 9555  pjocin 9560  pjrn 9564  df0op2 9595  hoaddcom 9615  hoaddass 9619  hocadddir 9622  hocsubdir 9623  hoaddid1 9629  ho0co 9631  hoid1 9632  hoid1r 9633  hodseq 9637  honegsub 9639  adj1o 9735  hoddi 9829  lnopunilem1 9850  lnopunilem2 9851  nmcopexlem2 9867  nmcopext 9874  nmcoplbt 9875  nmcfnexlem2 9896  nmcfnext 9903  nmcfnlbt 9904  adjbd1o 9933  adjco 9947  nmopcoadj 9948  pjsdi 9994  pjddi 9995  pjidmco 10016  pjtot 10017  pjin1 10030  pjclem1 10033  stji1 10079  large 10104  ghomgrpilem1 10290  ghomgrpilem2 10291  cayleylem2 10317  cayleylem3 10318  ump 10355  cmpfun 10363  fgsb 10444  fgsb2 10449  cnfilca 10451  clicls 10466  stoi 10483  relrded 10519  relrcat 10540

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