Theorem mpbir 146

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

Syntax hints:   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74ri  181  imnani  692  stabnot  834  mpbir2an  944  mpbir3an  1181  tru  1368  mpgbir  1464  nfxfr  1485  19.8a  1601  sbt  1795  dveeq2  1826  dveeq2or  1827  sbequilem  1849  cbvex2  1934  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  nfeuv  2056  moaneu  2114  moanmo  2115  eqeltri  2262  nfcxfr  2329  neir  2363  neirr  2369  eqnetri  2383  nesymir  2407  nelir  2458  mprgbir  2548  vex  2759  issetri  2765  moeq  2931  cdeqi  2966  ru  2980  eqsstri  3206  3sstr4i  3215  rgenm  3544  mosn  3650  rabrsndc  3682  tpid1  3725  tpid2  3727  tpid3  3730  pwv  3830  uni0  3858  eqbrtri  4046  tr0  4134  trv  4135  zfnuleu  4149  0ex  4152  inex1  4159  elpwi2  4183  0elpw  4189  axpow2  4201  axpow3  4202  vpwex  4204  zfpair2  4235  exss  4252  moop2  4276  pwundifss  4310  po0  4336  epse  4367  fr0  4376  0elon  4417  onm  4426  uniex2  4461  snnex  4473  ordtriexmidlem  4543  ordtriexmid  4545  ontr2exmid  4549  ordtri2or2exmidlem  4550  onsucsssucexmid  4551  onsucelsucexmidlem  4553  ruALT  4575  zfregfr  4598  dcextest  4605  zfinf2  4613  omex  4617  finds  4624  finds2  4625  ordom  4631  omsinds  4646  relsnop  4757  relxp  4760  rel0  4776  relopabi  4777  eliunxp  4791  opeliunxp2  4792  dmi  4867  xpidtr  5044  cnvcnv  5106  dmsn0  5121  cnvsn0  5122  funmpt  5280  funmpt2  5281  funinsn  5291  isarep2  5329  f0  5432  f10  5521  f1o00  5522  f1oi  5525  f1osn  5527  brprcneu  5534  fvopab3ig  5618  opabex  5768  eufnfv  5775  mpofun  6006  reldmmpo  6016  ovid  6021  ovidig  6022  ovidi  6023  ovig  6026  ovi3  6041  oprabex  6161  oprabex3  6162  f1stres  6192  f2ndres  6193  opeliunxp2f  6271  tpos0  6307  issmo  6321  tfrlem6  6349  tfrlem8  6351  tfri1dALT  6384  tfrcl  6397  rdgfun  6406  frecfun  6428  frecfcllem  6437  0lt1o  6473  eqer  6599  ecopover  6667  ecopoverg  6670  th3qcor  6673  mapsnf1o3  6731  ssdomg  6812  ensn1  6830  xpcomf1o  6859  fiunsnnn  6917  finexdc  6938  exmidpw  6944  dcfi  7019  omct  7155  infnninf  7162  infnninfOLD  7163  pm54.43  7229  exmidonfinlem  7232  pw1on  7265  pw1dom2  7266  pw1ne1  7268  2oneel  7295  dmaddpi  7364  dmmulpi  7365  1lt2pi  7379  indpi  7381  1lt2nq  7445  genpelxp  7550  ltexprlempr  7647  recexprlempr  7671  cauappcvgprlemcl  7692  cauappcvgprlemladd  7697  caucvgprlemcl  7715  caucvgprprlemcl  7743  m1p1sr  7799  m1m1sr  7800  0lt1sr  7804  peano1nnnn  7891  ax1cn  7900  ax1re  7901  axaddf  7907  axmulf  7908  ax0lt1  7915  0lt1  8125  subaddrii  8287  ixi  8581  1ap0  8588  sup3exmid  8955  nn1suc  8979  neg1lt0  9068  4d2e2  9120  iap0  9183  un0mulcl  9251  pnf0xnn0  9287  3halfnz  9391  nummac  9469  uzf  9572  mnfltpnf  9827  ixxf  9940  ioof  10013  fzf  10054  fzp1disj  10122  fzp1nel  10146  fzo0  10210  frecfzennn  10469  frechashgf1o  10471  xnn0nnen  10480  fxnn0nninf  10482  seq3f1olemp  10547  sq0  10657  irec  10666  hash0  10823  prhash2ex  10836  climmo  11353  sum0  11443  fisumcom2  11493  prod0  11640  fprodcom2fi  11681  cos1bnd  11814  cos2bnd  11815  n2dvdsm1  11965  n2dvds3  11967  flodddiv4  11986  3lcm2e6woprm  12135  6lcm4e12  12136  2prm  12176  3lcm2e6  12209  pockthi  12407  unennn  12465  ssnnctlemct  12514  structcnvcnv  12545  strleun  12633  starvndxnbasendx  12670  starvndxnplusgndx  12671  starvndxnmulrndx  12672  scandxnbasendx  12682  scandxnplusgndx  12683  scandxnmulrndx  12684  vscandxnbasendx  12687  vscandxnplusgndx  12688  vscandxnmulrndx  12689  vscandxnscandx  12690  ipndxnbasendx  12700  ipndxnplusgndx  12701  ipndxnmulrndx  12702  slotsdifipndx  12703  tsetndxnplusgndx  12720  tsetndxnmulrndx  12721  tsetndxnstarvndx  12722  slotstnscsi  12723  plendxnplusgndx  12734  plendxnmulrndx  12735  plendxnscandx  12736  plendxnvscandx  12737  slotsdifplendx  12738  dsndxnplusgndx  12745  dsndxnmulrndx  12746  slotsdnscsi  12747  dsndxntsetndx  12748  slotsdifdsndx  12749  unifndxntsetndx  12755  slotsdifunifndx  12756  restid  12772  mgmidmo  12866  lssmex  13714  lidlmex  13834  2idlmex  13860  fczpsrbag  14010  tgdom  14093  tgidm  14095  resttopon  14192  rest0  14200  psmetrel  14343  metrel  14363  xmetrel  14364  xmetf  14371  0met  14405  mopnrel  14462  setsmsbasg  14500  setsmsdsg  14501  qtopbasss  14542  reldvg  14686  dvexp  14713  dveflem  14725  efcn  14727  sinhalfpilem  14750  sincosq1lem  14784  tangtx  14797  sincos4thpi  14799  pigt3  14803  dfrelog  14819  relogf1o  14820  log1  14825  loge  14826  relogiso  14832  2logb9irr  14927  2logb9irrap  14933  2sqlem9  15010  2sqlem10  15011  ex-fl  15016  bj-nndcALT  15049  bj-axempty  15184  bj-axempty2  15185  bdinex1  15190  bj-zfpair2  15201  bj-uniex2  15207  bj-indint  15222  bj-omind  15225  bj-omex  15233  bj-omelon  15252  0nninf  15293  dceqnconst  15349  dcapnconst  15350