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  612  stabnot  729  mpbir2an  835  mpbir3an  1069  tru  1230  mpto1  1295  mpgbir  1318  nfxfr  1339  19.8a  1460  sbt  1645  dveeq2  1674  dveeq2or  1675  sbequilem  1697  cbvex2  1775  dvelimALT  1864  dvelimfv  1865  dvelimor  1872  nfeuv  1896  moaneu  1954  moanmo  1955  eqeltri  2088  nfcxfr  2153  neir  2187  neirr  2190  eqnetri  2202  nesymir  2226  nelir  2274  mprgbir  2353  vex  2534  issetri  2538  moeq  2689  cdeqi  2722  ru  2736  eqsstri  2948  3sstr4i  2957  rgenm  3298  mosn  3377  rabrsndc  3408  tpid1  3451  tpid2  3452  tpid3  3454  pwv  3549  uni0  3577  eqbrtri  3753  tr0  3835  trv  3836  zfnuleu  3851  0ex  3854  inex1  3861  0elpw  3887  axpow2  3899  axpow3  3900  pwex  3902  zfpair2  3915  exss  3933  moop2  3958  pwundifss  3992  po0  4018  epse  4043  0elon  4074  onm  4083  uniex2  4119  snnex  4127  ordtriexmidlem  4188  ordtriexmid  4190  onsucsssucexmid  4192  onsucelsucexmidlem  4194  ruALT  4209  zfinf2  4235  omex  4239  finds  4246  finds2  4247  ordom  4252  relsnop  4367  relxp  4370  rel0  4385  relopabi  4386  eliunxp  4398  opeliunxp2  4399  dmi  4473  xpidtr  4638  cnvcnv  4696  dmsn0  4711  cnvsn0  4712  funmpt  4860  funmpt2  4861  isarep2  4908  f0  5001  f10  5081  f1o00  5082  f1oi  5085  f1osn  5087  brprcneu  5092  fvopab3ig  5167  opabex  5306  eufnfv  5310  mpt2fun  5522  reldmmpt2  5531  ovid  5536  ovidig  5537  ovidi  5538  ovig  5541  ovi3  5556  oprabex  5674  oprabex3  5675  f1stres  5705  f2ndres  5706  tpos0  5807  issmo  5821  tfrlem6  5850  tfrlem8  5852  tfri1  5869  rdgfun  5877  0lt1o  5934  eqer  6045  ecopover  6111  ecopoverg  6114  th3qcor  6117  dmaddpi  6179  dmmulpi  6180  1lt2pi  6194  1lt2nq  6258  genpelxp  6359  genpelpw  6365  ltexprlempr  6439  recexprlempr  6460  m1p1sr  6501  m1m1sr  6502  0lt1sr  6506  ax1cn  6551  ax1re  6552  ax0lt1  6564  ax-0lt1  6590  0lt1  6728  subaddrii  6886  bdinex1  7261  bj-zfpair2  7272  bj-uniex2  7278  bj-indint  7293  bj-omind  7295  bj-omex  7303  bj-omelon  7320