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  693  stabnot  835  mpbir2an  945  mpbir3an  1182  tru  1377  dcfromnotnotr  1467  dcfromcon  1468  dcfrompeirce  1469  mpgbir  1476  nfxfr  1497  19.8a  1613  sbt  1807  dveeq2  1838  dveeq2or  1839  sbequilem  1861  cbvex2  1946  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  nfeuv  2072  moaneu  2130  moanmo  2131  eqeltri  2278  nfcxfr  2345  neir  2379  neirr  2385  eqnetri  2399  nesymir  2423  nelir  2474  mprgbir  2564  vex  2775  issetri  2781  moeq  2948  cdeqi  2983  ru  2997  eqsstri  3225  3sstr4i  3234  mosn  3669  rabrsndc  3701  tpid1  3744  tpid2  3746  tpid3  3749  pwv  3849  uni0  3877  eqbrtri  4065  tr0  4153  trv  4154  zfnuleu  4168  0ex  4171  inex1  4178  elpwi2  4202  0elpw  4208  axpow2  4220  axpow3  4221  vpwex  4223  zfpair2  4254  exss  4271  opwo0id  4293  moop2  4296  pwundifss  4332  po0  4358  epse  4389  fr0  4398  0elon  4439  onm  4448  uniex2  4483  snnex  4495  ordtriexmidlem  4567  ordtriexmid  4569  ontr2exmid  4573  ordtri2or2exmidlem  4574  onsucsssucexmid  4575  onsucelsucexmidlem  4577  ruALT  4599  zfregfr  4622  dcextest  4629  zfinf2  4637  omex  4641  finds  4648  finds2  4649  ordom  4655  omsinds  4670  relsnop  4781  relxp  4784  rel0  4800  relopabiv  4801  relopabi  4803  eliunxp  4817  opeliunxp2  4818  dmi  4893  xpidtr  5073  cnvcnv  5135  dmsn0  5150  cnvsn0  5151  funmpt  5309  funmpt2  5310  funinsn  5323  isarep2  5361  f0  5466  f10  5556  f1o00  5557  f1oi  5560  f1osn  5562  brprcneu  5569  fvopab3ig  5653  opabex  5808  eufnfv  5815  mpofun  6047  reldmmpo  6057  ovid  6062  ovidig  6063  ovidi  6064  ovig  6067  ovi3  6083  oprabex  6213  oprabex3  6214  f1stres  6245  f2ndres  6246  opeliunxp2f  6324  tpos0  6360  issmo  6374  tfrlem6  6402  tfrlem8  6404  tfri1dALT  6437  tfrcl  6450  rdgfun  6459  frecfun  6481  frecfcllem  6490  0lt1o  6526  eqer  6652  ecopover  6720  ecopoverg  6723  th3qcor  6726  mapsnf1o3  6784  ssdomg  6870  ensn1  6888  xpcomf1o  6920  fiunsnnn  6978  finexdc  6999  exmidpw  7005  dcfi  7083  omct  7219  infnninf  7226  infnninfOLD  7227  pm54.43  7298  exmidonfinlem  7301  pw1on  7338  pw1dom2  7339  pw1ne1  7341  2oneel  7368  dmaddpi  7438  dmmulpi  7439  1lt2pi  7453  indpi  7455  1lt2nq  7519  genpelxp  7624  ltexprlempr  7721  recexprlempr  7745  cauappcvgprlemcl  7766  cauappcvgprlemladd  7771  caucvgprlemcl  7789  caucvgprprlemcl  7817  m1p1sr  7873  m1m1sr  7874  0lt1sr  7878  peano1nnnn  7965  ax1cn  7974  ax1re  7975  axaddf  7981  axmulf  7982  ax0lt1  7989  0lt1  8199  subaddrii  8361  ixi  8656  1ap0  8663  sup3exmid  9030  nn1suc  9055  neg1lt0  9144  4d2e2  9197  iap0  9260  un0mulcl  9329  pnf0xnn0  9365  3halfnz  9470  nummac  9548  uzf  9651  mnfltpnf  9907  ixxf  10020  ioof  10093  fzf  10134  fzp1disj  10202  fzp1nel  10226  fzo0  10292  frecfzennn  10571  frechashgf1o  10573  xnn0nnen  10582  fxnn0nninf  10584  seq3f1olemp  10660  sq0  10775  irec  10784  hash0  10941  prhash2ex  10954  climmo  11609  sum0  11699  fisumcom2  11749  prod0  11896  fprodcom2fi  11937  cos1bnd  12070  cos2bnd  12071  3dvds  12175  n2dvdsm1  12224  n2dvds3  12226  flodddiv4  12247  3lcm2e6woprm  12408  6lcm4e12  12409  2prm  12449  3lcm2e6  12482  pockthi  12681  modsubi  12742  unennn  12768  ssnnctlemct  12817  structcnvcnv  12848  strleun  12936  starvndxnbasendx  12974  starvndxnplusgndx  12975  starvndxnmulrndx  12976  scandxnbasendx  12986  scandxnplusgndx  12987  scandxnmulrndx  12988  vscandxnbasendx  12991  vscandxnplusgndx  12992  vscandxnmulrndx  12993  vscandxnscandx  12994  ipndxnbasendx  13004  ipndxnplusgndx  13005  ipndxnmulrndx  13006  slotsdifipndx  13007  tsetndxnplusgndx  13024  tsetndxnmulrndx  13025  tsetndxnstarvndx  13026  slotstnscsi  13027  plendxnplusgndx  13038  plendxnmulrndx  13039  plendxnscandx  13040  plendxnvscandx  13041  slotsdifplendx  13042  basendxnocndx  13045  plendxnocndx  13046  dsndxnplusgndx  13053  dsndxnmulrndx  13054  slotsdnscsi  13055  dsndxntsetndx  13056  slotsdifdsndx  13057  unifndxntsetndx  13063  slotsdifunifndx  13064  restid  13082  prdsval  13105  mgmidmo  13204  rrgmex  14023  lssmex  14117  lidlmex  14237  2idlmex  14263  fczpsrbag  14433  tgdom  14544  tgidm  14546  resttopon  14643  rest0  14651  psmetrel  14794  metrel  14814  xmetrel  14815  xmetf  14822  0met  14856  mopnrel  14913  setsmsbasg  14951  setsmsdsg  14952  qtopbasss  14993  reldvg  15151  dvexp  15183  dveflem  15198  elply2  15207  elplyd  15213  ply1term  15215  plymullem  15222  efcn  15240  sinhalfpilem  15263  sincosq1lem  15297  tangtx  15310  sincos4thpi  15312  pigt3  15316  dfrelog  15332  relogf1o  15333  log1  15338  loge  15339  relogiso  15345  2logb9irr  15443  2logb9irrap  15449  2sqlem9  15601  2sqlem10  15602  ex-fl  15661  bj-nndcALT  15694  bj-axempty  15829  bj-axempty2  15830  bdinex1  15835  bj-zfpair2  15846  bj-uniex2  15852  bj-indint  15867  bj-omind  15870  bj-omex  15878  bj-omelon  15897  0nninf  15941  dceqnconst  15999  dcapnconst  16000