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  ltexprlempr  6581  recexprlempr  6603  cauappcvgprlemcl  6624  cauappcvgprlemladd  6629  m1p1sr  6668  m1m1sr  6669  0lt1sr  6673  ax1cn  6727  ax1re  6728  ax0lt1  6740  ax-0lt1  6769  0lt1  6918  subaddrii  7076  ixi  7347  1ap0  7354  nn1suc  7694  neg1lt0  7783  4d2e2  7834  iap0  7905  un0mulcl  7972  nummac  8155  uzf  8232  mnfltpnf  8456  ixxf  8517  ioof  8590  fzf  8628  fzp1disj  8692  fzp1nel  8716  fzo0  8774  frecfzennn  8864  frechashgf1o  8866  sq0  8977  irec  8985  bdinex1  9330  bj-zfpair2  9341  bj-uniex2  9347  bj-indint  9366  bj-omind  9368  bj-omex  9376  bj-omelon  9393