Theorem mpbir 144

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 131	. 2 |- ( ps -> ph )
4	1, 3	ax-mp 7	1 |- ph

Syntax hints:   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.74ri  179  imnani  657  stabnot  774  mpbir2an  883  mpbir3an  1120  tru  1288  mpgbir  1382  nfxfr  1403  19.8a  1522  sbt  1707  dveeq2  1736  dveeq2or  1737  sbequilem  1759  cbvex2  1838  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  nfeuv  1959  moaneu  2017  moanmo  2018  eqeltri  2151  nfcxfr  2216  neir  2248  neirr  2254  eqnetri  2268  nesymir  2292  nelir  2342  mprgbir  2421  vex  2604  issetri  2608  moeq  2767  cdeqi  2800  ru  2814  eqsstri  3029  3sstr4i  3038  rgenm  3343  mosn  3429  rabrsndc  3460  tpid1  3503  tpid2  3504  tpid3  3506  pwv  3600  uni0  3628  eqbrtri  3804  tr0  3886  trv  3887  zfnuleu  3902  0ex  3905  inex1  3912  0elpw  3938  axpow2  3950  axpow3  3951  pwex  3953  zfpair2  3965  exss  3982  moop2  4006  pwundifss  4040  po0  4066  epse  4097  fr0  4106  0elon  4147  onm  4156  uniex2  4191  snnex  4199  ordtriexmidlem  4263  ordtriexmid  4265  ontr2exmid  4268  ordtri2or2exmidlem  4269  onsucsssucexmid  4270  onsucelsucexmidlem  4272  ruALT  4294  zfregfr  4316  zfinf2  4330  omex  4334  finds  4341  finds2  4342  ordom  4347  relsnop  4462  relxp  4465  rel0  4480  relopabi  4481  eliunxp  4493  opeliunxp2  4494  dmi  4568  xpidtr  4735  cnvcnv  4793  dmsn0  4808  cnvsn0  4809  funmpt  4958  funmpt2  4959  isarep2  5006  f0  5100  f10  5180  f1o00  5181  f1oi  5184  f1osn  5186  brprcneu  5191  fvopab3ig  5267  opabex  5406  eufnfv  5410  mpt2fun  5623  reldmmpt2  5632  ovid  5637  ovidig  5638  ovidi  5639  ovig  5642  ovi3  5657  oprabex  5775  oprabex3  5776  f1stres  5806  f2ndres  5807  tpos0  5912  issmo  5926  tfrlem6  5955  tfrlem8  5957  rdgfun  5983  0lt1o  6046  eqer  6161  ecopover  6227  ecopoverg  6230  th3qcor  6233  ssdomg  6281  ensn1  6299  xpcomf1o  6322  fiunsnnn  6365  pm54.43  6459  dmaddpi  6515  dmmulpi  6516  1lt2pi  6530  indpi  6532  1lt2nq  6596  genpelxp  6701  ltexprlempr  6798  recexprlempr  6822  cauappcvgprlemcl  6843  cauappcvgprlemladd  6848  caucvgprlemcl  6866  caucvgprprlemcl  6894  m1p1sr  6937  m1m1sr  6938  0lt1sr  6942  peano1nnnn  7020  ax1cn  7029  ax1re  7030  ax0lt1  7042  0lt1  7236  subaddrii  7397  ixi  7683  1ap0  7690  nn1suc  8058  neg1lt0  8147  4d2e2  8192  iap0  8254  un0mulcl  8322  3halfnz  8444  nummac  8521  uzf  8622  mnfltpnf  8860  ixxf  8921  ioof  8994  fzf  9033  fzp1disj  9097  fzp1nel  9121  fzo0  9177  frecfzennn  9419  frechashgf1o  9421  sq0  9566  irec  9574  climmo  10137  n2dvdsm1  10313  n2dvds3  10315  flodddiv4  10334  3lcm2e6woprm  10468  6lcm4e12  10469  2prm  10509  3lcm2e6  10539  ex-fl  10563  bj-axempty  10684  bj-axempty2  10685  bdinex1  10690  bj-zfpair2  10701  bj-uniex2  10707  bj-indint  10726  bj-omind  10729  bj-omex  10737  bj-omelon  10756