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  6494  ltexprlempr  6582  recexprlempr  6604  cauappcvgprlemcl  6625  cauappcvgprlemladd  6630  caucvgprlemcl  6647  m1p1sr  6688  m1m1sr  6689  0lt1sr  6693  ax1cn  6747  ax1re  6748  ax0lt1  6760  ax-0lt1  6789  0lt1  6938  subaddrii  7096  ixi  7367  1ap0  7374  nn1suc  7714  neg1lt0  7803  4d2e2  7854  iap0  7925  un0mulcl  7992  nummac  8175  uzf  8252  mnfltpnf  8476  ixxf  8537  ioof  8610  fzf  8648  fzp1disj  8712  fzp1nel  8736  fzo0  8794  frecfzennn  8884  frechashgf1o  8886  sq0  8997  irec  9005  bj-axempty  9348  bj-axempty2  9349  bdinex1  9354  bj-zfpair2  9365  bj-uniex2  9371  bj-indint  9390  bj-omind  9393  bj-omex  9402  bj-omelon  9421