Theorem mpbir 134

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

Hypotheses

Ref	Expression
mpbir.min	⊢ ψ
mpbir.maj	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mpbir	⊢ φ

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 ⊢ ψ
2		mpbir.maj	. . 3 ⊢ (φ ↔ ψ)
3	2	biimpri 124	. 2 ⊢ (ψ → φ)
4	1, 3	ax-mp 7	1 ⊢ φ

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.74ri  170  imnani  624  stabnot  740  mpbir2an  848  mpbir3an  1085  tru  1246  mpto1  1311  mpgbir  1339  nfxfr  1360  19.8a  1479  sbt  1664  dveeq2  1693  dveeq2or  1694  sbequilem  1716  cbvex2  1794  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  nfeuv  1915  moaneu  1973  moanmo  1974  eqeltri  2107  nfcxfr  2172  neir  2206  neirr  2210  eqnetri  2222  nesymir  2246  nelir  2294  mprgbir  2373  vex  2554  issetri  2558  moeq  2710  cdeqi  2743  ru  2757  eqsstri  2969  3sstr4i  2978  rgenm  3317  mosn  3398  rabrsndc  3429  tpid1  3472  tpid2  3473  tpid3  3475  pwv  3570  uni0  3598  eqbrtri  3774  tr0  3856  trv  3857  zfnuleu  3872  0ex  3875  inex1  3882  0elpw  3908  axpow2  3920  axpow3  3921  pwex  3923  zfpair2  3936  exss  3954  moop2  3979  pwundifss  4013  po0  4039  epse  4064  0elon  4095  onm  4104  uniex2  4139  snnex  4147  ordtriexmidlem  4208  ordtriexmid  4210  onsucsssucexmid  4212  onsucelsucexmidlem  4214  ruALT  4229  zfinf2  4255  omex  4259  finds  4266  finds2  4267  ordom  4272  relsnop  4387  relxp  4390  rel0  4405  relopabi  4406  eliunxp  4418  opeliunxp2  4419  dmi  4493  xpidtr  4658  cnvcnv  4716  dmsn0  4731  cnvsn0  4732  funmpt  4881  funmpt2  4882  isarep2  4929  f0  5023  f10  5103  f1o00  5104  f1oi  5107  f1osn  5109  brprcneu  5114  fvopab3ig  5189  opabex  5328  eufnfv  5332  mpt2fun  5545  reldmmpt2  5554  ovid  5559  ovidig  5560  ovidi  5561  ovig  5564  ovi3  5579  oprabex  5697  oprabex3  5698  f1stres  5728  f2ndres  5729  tpos0  5830  issmo  5844  tfrlem6  5873  tfrlem8  5875  rdgfun  5900  0lt1o  5962  eqer  6074  ecopover  6140  ecopoverg  6143  th3qcor  6146  ssdomg  6194  ensn1  6212  xpcomf1o  6235  dmaddpi  6309  dmmulpi  6310  1lt2pi  6324  indpi  6326  1lt2nq  6389  genpelxp  6493  genpelpw  6499  ltexprlempr  6580  recexprlempr  6602  m1p1sr  6648  m1m1sr  6649  0lt1sr  6653  ax1cn  6707  ax1re  6708  ax0lt1  6720  ax-0lt1  6749  0lt1  6898  subaddrii  7056  ixi  7327  1ap0  7334  nn1suc  7674  neg1lt0  7763  4d2e2  7814  iap0  7885  un0mulcl  7952  nummac  8135  uzf  8212  mnfltpnf  8436  ixxf  8497  ioof  8570  fzf  8608  fzp1disj  8672  fzp1nel  8696  fzo0  8754  frecfzennn  8844  frechashgf1o  8846  sq0  8957  irec  8965  bdinex1  9284  bj-zfpair2  9295  bj-uniex2  9301  bj-indint  9320  bj-omind  9322  bj-omex  9330  bj-omelon  9347