Theorem mpbir 190

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

Hypotheses

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

Assertion

Ref	Expression
mpbir	|- ph

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 |- ps
2		mpbir.maj	. . 3 |- (ph <-> ps)
3	2	biimpr 152	. 2 |- (ps -> ph)
4	1, 3	ax-mp 7	1 |- ph

Syntax hints:   <-> wb 146

This theorem is referenced by:  mtbir 192  orri 231  imp 350  con4bii 525  pm3.2ni 582  pm5.74ri 589  pm3.24 660  pm5.16 669  mpbir2an 732  nicodmpraw 955  19.35ri 1079  ax9o 1124  a9e 1127  cbval2 1318  cbvex2 1319  moaneu 1432  moanmo 1433  axext 1463  eqeltr 1547  mprgbir 1704  visset 1816  issetri 1819  eueq3 1922  moeq 1923  ru 1941  eqsstr 2095  3sstr4 2104  ssnpss 2153  pwid 2413  pri1 2455  pwv 2507  uni0 2530  intab 2565  eqbrtr 2640  tr0 2697  trv 2698  zfrep4 2707  zfnuleu 2713  0ex 2717  inex1 2722  0elpw 2742  notzfaus 2747  pwex 2752  snex 2757  exss 2776  dvdemo1 2782  zfpair2 2787  moop2 2808  itlso 2870  uniex2 2876  rabxfr 2909  0elon 3029  nsuceq0 3060  limon 3101  onuninsuc 3115  finds 3163  finds2 3165  tfinds2 3172  onxpdisj 3248  relsn 3261  relxp 3262  relopab 3273  rel0 3279  reli 3280  rele 3281  ididg 3285  dmi 3333  relres 3394  relcnv 3442  relco 3491  cnvcnv 3493  isarep2 3585  opabex 3616  f0 3663  fconst 3665  f10 3720  f1o00 3721  f1oi 3724  f1osn 3726  fvopab3ig 3785  canth 3914  ncanth 3915  tfrlem8 3925  tz7.44lem1 3934  abianfp 3969  reloprab 3999  reldmoprab 4012  oprabex 4026  oprabex3 4029  oprabvalig 4031  oprabval3 4037  ndmoprcl 4051  fo1st 4098  fo2nd 4099  f1stres 4100  f2ndres 4101  df1st2 4133  df2nd2 4134  1ne0 4149  0lt1o 4154  th3qcor 4323  mapsspw 4348  map0 4351  relen 4379  reldom 4380  ssdomg 4415  ensn1 4431  snfi 4439  limensuci 4513  omsdomnn 4540  unblem4 4556  prfiOLD 4571  pm54.43 4588  inf2 4624  inf3lem6 4634  infeq5 4637  zfinf 4642  inf5 4644  trcl 4662  r1fnon 4667  r1tr 4671  tz9.12lem2 4677  tz9.12lem3 4678  jech9.3 4683  rankval 4685  rankr1 4691  rankpw 4701  karden 4743  aceq3lem 4749  ac2 4763  kmlem2 4783  numthlem 4800  numth2 4802  zorn 4814  cardon 4844  cardid 4845  sucxpdom 4864  ondomon 4874  cardprc 4879  alephfnon 4880  alephsucpw 4888  alephsucdom 4898  alephfplem4 4917  alephfp 4918  alephval3 4921  axpowndlem3 4970  zfcndun 4986  zfcndpow 4987  zfcndinf 4989  zfcndac 4990  dmaddpi 5037  dmmulpi 5038  1lt2pi 5051  1q 5076  1lt2pq 5097  1pr 5136  0r 5208  1r 5209  m1r 5210  m1p1sr 5220  m1m1sr 5221  0lt1sr 5223  axaddopr 5284  axmulopr 5285  ax1cn 5288  ax1ne0 5299  subaddri 5391  ine0 5453  pnfxr 5512  mnfxr 5513  pnfnre 5515  mnfnre 5516  pnfnemnf 5555  renfdisj 5558  mnfltpnf 5563  divrec 5751  div1 5780  recgt0i 5823  nn1suc 5948  4d2e2 6036  nnunb 6079  arch 6080  0z 6155  nneo 6206  om2uzran 6308  om2uzf1o 6309  uzrdgfnuz 6314  ndmioo 6378  ioof 6408  indstr 6469  elfzlem 6481  seq0fn 6554  dfseq0 6571  sq0 6643  sqrlem6 6686  sqrlem8 6688  sqrlem11 6691  sqr4 6725  sqr9 6726  sqr2irr 6737  irec 6739  nthruz 6754  cjmulrcl 6798  abs0 6884  abstri 6898  abslem2i 6915  bcpasc2 6974  climrel 6983  climuz0 7115  iserzshft 7151  climabslem 7155  climubi 7160  climsup 7162  caucvg 7170  isumshft2 7212  isumcmpi 7222  infcvgaux1 7226  fnsmnt 7233  negfcncf 7276  ivthlem5 7292  ivthlem6 7293  ivthlem7 7294  ivthlem8 7295  isupivth 7297  efaddlem8 7352  efaddlem12 7356  ef1tllem 7388  ef01tllem1 7390  ef01tllem2 7391  eirrlem1 7396  eirrlem3 7398  eirr 7401  reeff1o 7433  sinadd 7458  cos2tOLD 7472  cos1bnd 7482  cos2bnd 7483  acdc2lem2 7497  acdc5lem2 7500  nnenom 7506  unbenlem 7512  ruclem13 7530  ruclem35 7552  aleph1re 7559  eltopsp 7612  tpsex 7613  sn0top 7651  indistps 7657  distps 7658  retopbas 7659  msrel 7801  0met 7829  cnmet 7908  bcthlem12 8014  isgrpi 8046  0ngrp 8059  isgrp2i 8079  issubgi 8125  grpsn 8127  ghgrpilem4 8139  ghsubgi 8141  isring 8144  vcrel 8169  isvci 8204  nvrel 8224  0vfval 8228  isnvi 8235  vsfval 8257  ipcl 8368  ajmoi 8522  ajfuni 8523  minvecdist 8588  pilem2 8674  sincosq1lem 8705  sincos4thpi 8712  sincos6thpi 8713  cosh111lem1 8716  efifolem2 8725  logrn 8753  eff1o2 8756  logf1o 8757  relogf1o 8759  log1 8768  loge 8769  pilog 8770  relogiso 8777  axgroth2 8780  axgroth3 8781  avril1 8786  2bornot2b 8787  normlem2 8979  norm3adif 9017  hhssnv 9136  projlem13 9200  projlem14 9201  pjpj0 9257  shscl 9283  shsumval2 9362  h1de2 9478  fh3 9568  fh4 9569  qlaxr3 9579  ho0f 9679  hoif 9682  hodid 9715  ho0sub 9723  hosd1 9750  adjmo 9760  nmopsetn0 9794  nmfnsetn0 9807  funadj 9815  funcnvadj 9819  adj1o 9820  nlelsh 9995  cnlnadjlem8 10009  nmoptri2 10034  bra11 10043  pjoc 10110  pjinvar 10122  cvnsymt 10220  ghomgrpilem2 10389  symggrpi 10409  symgidi 10410  cmpfun 10465  vxveqv 10475  inposet 10485  hmeogrp 10532  efilcp 10564  efilcp2 10569  dtopcl 10594  1ded 10650  relded 10652  reldded 10653  relrded 10654  relcat 10673  reldcat 10674  relrcat 10675  hgrarel 10747

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