Theorem mpbir 134

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

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  625  stabnot  741  mpbir2an  849  mpbir3an  1086  tru  1247  mpgbir  1342  nfxfr  1363  19.8a  1482  sbt  1667  dveeq2  1696  dveeq2or  1697  sbequilem  1719  cbvex2  1797  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  nfeuv  1918  moaneu  1976  moanmo  1977  eqeltri  2110  nfcxfr  2175  neir  2209  neirr  2215  eqnetri  2228  nesymir  2252  nelir  2300  mprgbir  2379  vex  2560  issetri  2564  moeq  2716  cdeqi  2749  ru  2763  eqsstri  2975  3sstr4i  2984  rgenm  3323  mosn  3406  rabrsndc  3438  tpid1  3481  tpid2  3482  tpid3  3484  pwv  3579  uni0  3607  eqbrtri  3783  tr0  3865  trv  3866  zfnuleu  3881  0ex  3884  inex1  3891  0elpw  3917  axpow2  3929  axpow3  3930  pwex  3932  zfpair2  3945  exss  3963  moop2  3988  pwundifss  4022  po0  4048  epse  4079  fr0  4088  0elon  4129  onm  4138  uniex2  4173  snnex  4181  ordtriexmidlem  4245  ordtriexmid  4247  ontr2exmid  4250  ordtri2or2exmidlem  4251  onsucsssucexmid  4252  onsucelsucexmidlem  4254  ruALT  4275  zfregfr  4298  zfinf2  4312  omex  4316  finds  4323  finds2  4324  ordom  4329  relsnop  4444  relxp  4447  rel0  4462  relopabi  4463  eliunxp  4475  opeliunxp2  4476  dmi  4550  xpidtr  4715  cnvcnv  4773  dmsn0  4788  cnvsn0  4789  funmpt  4938  funmpt2  4939  isarep2  4986  f0  5080  f10  5160  f1o00  5161  f1oi  5164  f1osn  5166  brprcneu  5171  fvopab3ig  5246  opabex  5385  eufnfv  5389  mpt2fun  5603  reldmmpt2  5612  ovid  5617  ovidig  5618  ovidi  5619  ovig  5622  ovi3  5637  oprabex  5755  oprabex3  5756  f1stres  5786  f2ndres  5787  tpos0  5889  issmo  5903  tfrlem6  5932  tfrlem8  5934  rdgfun  5960  0lt1o  6023  eqer  6138  ecopover  6204  ecopoverg  6207  th3qcor  6210  ssdomg  6258  ensn1  6276  xpcomf1o  6299  fiunsnnn  6338  dmaddpi  6423  dmmulpi  6424  1lt2pi  6438  indpi  6440  1lt2nq  6504  genpelxp  6609  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  cauappcvgprlemladd  6756  caucvgprlemcl  6774  caucvgprprlemcl  6802  m1p1sr  6845  m1m1sr  6846  0lt1sr  6850  peano1nnnn  6928  ax1cn  6937  ax1re  6938  ax0lt1  6950  ax-0lt1  6990  0lt1  7141  subaddrii  7300  ixi  7574  1ap0  7581  nn1suc  7933  neg1lt0  8025  4d2e2  8076  iap0  8148  un0mulcl  8216  nummac  8399  uzf  8476  mnfltpnf  8706  ixxf  8767  ioof  8840  fzf  8878  fzp1disj  8942  fzp1nel  8966  fzo0  9024  frecfzennn  9203  frechashgf1o  9205  sq0  9344  irec  9352  climmo  9819  ex-fl  9895  bj-axempty  10013  bj-axempty2  10014  bdinex1  10019  bj-zfpair2  10030  bj-uniex2  10036  bj-indint  10055  bj-omind  10058  bj-omex  10067  bj-omelon  10086