Theorem mpbir 146

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74ri  181  imnani  692  stabnot  834  mpbir2an  944  mpbir3an  1181  tru  1376  dcfromnotnotr  1466  dcfromcon  1467  dcfrompeirce  1468  mpgbir  1475  nfxfr  1496  19.8a  1612  sbt  1806  dveeq2  1837  dveeq2or  1838  sbequilem  1860  cbvex2  1945  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  nfeuv  2071  moaneu  2129  moanmo  2130  eqeltri  2277  nfcxfr  2344  neir  2378  neirr  2384  eqnetri  2398  nesymir  2422  nelir  2473  mprgbir  2563  vex  2774  issetri  2780  moeq  2947  cdeqi  2982  ru  2996  eqsstri  3224  3sstr4i  3233  mosn  3668  rabrsndc  3700  tpid1  3743  tpid2  3745  tpid3  3748  pwv  3848  uni0  3876  eqbrtri  4064  tr0  4152  trv  4153  zfnuleu  4167  0ex  4170  inex1  4177  elpwi2  4201  0elpw  4207  axpow2  4219  axpow3  4220  vpwex  4222  zfpair2  4253  exss  4270  opwo0id  4292  moop2  4295  pwundifss  4331  po0  4357  epse  4388  fr0  4397  0elon  4438  onm  4447  uniex2  4482  snnex  4494  ordtriexmidlem  4566  ordtriexmid  4568  ontr2exmid  4572  ordtri2or2exmidlem  4573  onsucsssucexmid  4574  onsucelsucexmidlem  4576  ruALT  4598  zfregfr  4621  dcextest  4628  zfinf2  4636  omex  4640  finds  4647  finds2  4648  ordom  4654  omsinds  4669  relsnop  4780  relxp  4783  rel0  4799  relopabiv  4800  relopabi  4802  eliunxp  4816  opeliunxp2  4817  dmi  4892  xpidtr  5072  cnvcnv  5134  dmsn0  5149  cnvsn0  5150  funmpt  5308  funmpt2  5309  funinsn  5322  isarep2  5360  f0  5465  f10  5555  f1o00  5556  f1oi  5559  f1osn  5561  brprcneu  5568  fvopab3ig  5652  opabex  5807  eufnfv  5814  mpofun  6046  reldmmpo  6056  ovid  6061  ovidig  6062  ovidi  6063  ovig  6066  ovi3  6082  oprabex  6212  oprabex3  6213  f1stres  6244  f2ndres  6245  opeliunxp2f  6323  tpos0  6359  issmo  6373  tfrlem6  6401  tfrlem8  6403  tfri1dALT  6436  tfrcl  6449  rdgfun  6458  frecfun  6480  frecfcllem  6489  0lt1o  6525  eqer  6651  ecopover  6719  ecopoverg  6722  th3qcor  6725  mapsnf1o3  6783  ssdomg  6869  ensn1  6887  xpcomf1o  6919  fiunsnnn  6977  finexdc  6998  exmidpw  7004  dcfi  7082  omct  7218  infnninf  7225  infnninfOLD  7226  pm54.43  7297  exmidonfinlem  7300  pw1on  7337  pw1dom2  7338  pw1ne1  7340  2oneel  7367  dmaddpi  7437  dmmulpi  7438  1lt2pi  7452  indpi  7454  1lt2nq  7518  genpelxp  7623  ltexprlempr  7720  recexprlempr  7744  cauappcvgprlemcl  7765  cauappcvgprlemladd  7770  caucvgprlemcl  7788  caucvgprprlemcl  7816  m1p1sr  7872  m1m1sr  7873  0lt1sr  7877  peano1nnnn  7964  ax1cn  7973  ax1re  7974  axaddf  7980  axmulf  7981  ax0lt1  7988  0lt1  8198  subaddrii  8360  ixi  8655  1ap0  8662  sup3exmid  9029  nn1suc  9054  neg1lt0  9143  4d2e2  9196  iap0  9259  un0mulcl  9328  pnf0xnn0  9364  3halfnz  9469  nummac  9547  uzf  9650  mnfltpnf  9906  ixxf  10019  ioof  10092  fzf  10133  fzp1disj  10201  fzp1nel  10225  fzo0  10290  frecfzennn  10569  frechashgf1o  10571  xnn0nnen  10580  fxnn0nninf  10582  seq3f1olemp  10658  sq0  10773  irec  10782  hash0  10939  prhash2ex  10952  climmo  11580  sum0  11670  fisumcom2  11720  prod0  11867  fprodcom2fi  11908  cos1bnd  12041  cos2bnd  12042  3dvds  12146  n2dvdsm1  12195  n2dvds3  12197  flodddiv4  12218  3lcm2e6woprm  12379  6lcm4e12  12380  2prm  12420  3lcm2e6  12453  pockthi  12652  modsubi  12713  unennn  12739  ssnnctlemct  12788  structcnvcnv  12819  strleun  12907  starvndxnbasendx  12945  starvndxnplusgndx  12946  starvndxnmulrndx  12947  scandxnbasendx  12957  scandxnplusgndx  12958  scandxnmulrndx  12959  vscandxnbasendx  12962  vscandxnplusgndx  12963  vscandxnmulrndx  12964  vscandxnscandx  12965  ipndxnbasendx  12975  ipndxnplusgndx  12976  ipndxnmulrndx  12977  slotsdifipndx  12978  tsetndxnplusgndx  12995  tsetndxnmulrndx  12996  tsetndxnstarvndx  12997  slotstnscsi  12998  plendxnplusgndx  13009  plendxnmulrndx  13010  plendxnscandx  13011  plendxnvscandx  13012  slotsdifplendx  13013  basendxnocndx  13016  plendxnocndx  13017  dsndxnplusgndx  13024  dsndxnmulrndx  13025  slotsdnscsi  13026  dsndxntsetndx  13027  slotsdifdsndx  13028  unifndxntsetndx  13034  slotsdifunifndx  13035  restid  13053  prdsval  13076  mgmidmo  13175  rrgmex  13994  lssmex  14088  lidlmex  14208  2idlmex  14234  fczpsrbag  14404  tgdom  14515  tgidm  14517  resttopon  14614  rest0  14622  psmetrel  14765  metrel  14785  xmetrel  14786  xmetf  14793  0met  14827  mopnrel  14884  setsmsbasg  14922  setsmsdsg  14923  qtopbasss  14964  reldvg  15122  dvexp  15154  dveflem  15169  elply2  15178  elplyd  15184  ply1term  15186  plymullem  15193  efcn  15211  sinhalfpilem  15234  sincosq1lem  15268  tangtx  15281  sincos4thpi  15283  pigt3  15287  dfrelog  15303  relogf1o  15304  log1  15309  loge  15310  relogiso  15316  2logb9irr  15414  2logb9irrap  15420  2sqlem9  15572  2sqlem10  15573  ex-fl  15623  bj-nndcALT  15656  bj-axempty  15791  bj-axempty2  15792  bdinex1  15797  bj-zfpair2  15808  bj-uniex2  15814  bj-indint  15829  bj-omind  15832  bj-omex  15840  bj-omelon  15859  0nninf  15903  dceqnconst  15961  dcapnconst  15962