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  691  stabnot  833  mpbir2an  942  mpbir3an  1179  tru  1357  mpgbir  1453  nfxfr  1474  19.8a  1590  sbt  1784  dveeq2  1815  dveeq2or  1816  sbequilem  1838  cbvex2  1922  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  nfeuv  2044  moaneu  2102  moanmo  2103  eqeltri  2250  nfcxfr  2316  neir  2350  neirr  2356  eqnetri  2370  nesymir  2394  nelir  2445  mprgbir  2535  vex  2740  issetri  2746  moeq  2912  cdeqi  2947  ru  2961  eqsstri  3187  3sstr4i  3196  rgenm  3525  mosn  3628  rabrsndc  3660  tpid1  3703  tpid2  3705  tpid3  3708  pwv  3808  uni0  3836  eqbrtri  4024  tr0  4112  trv  4113  zfnuleu  4127  0ex  4130  inex1  4137  elpwi2  4158  0elpw  4164  axpow2  4176  axpow3  4177  vpwex  4179  zfpair2  4210  exss  4227  moop2  4251  pwundifss  4285  po0  4311  epse  4342  fr0  4351  0elon  4392  onm  4401  uniex2  4436  snnex  4448  ordtriexmidlem  4518  ordtriexmid  4520  ontr2exmid  4524  ordtri2or2exmidlem  4525  onsucsssucexmid  4526  onsucelsucexmidlem  4528  ruALT  4550  zfregfr  4573  dcextest  4580  zfinf2  4588  omex  4592  finds  4599  finds2  4600  ordom  4606  omsinds  4621  relsnop  4732  relxp  4735  rel0  4751  relopabi  4752  eliunxp  4766  opeliunxp2  4767  dmi  4842  xpidtr  5019  cnvcnv  5081  dmsn0  5096  cnvsn0  5097  funmpt  5254  funmpt2  5255  funinsn  5265  isarep2  5303  f0  5406  f10  5495  f1o00  5496  f1oi  5499  f1osn  5501  brprcneu  5508  fvopab3ig  5590  opabex  5740  eufnfv  5747  mpofun  5976  reldmmpo  5985  ovid  5990  ovidig  5991  ovidi  5992  ovig  5995  ovi3  6010  oprabex  6128  oprabex3  6129  f1stres  6159  f2ndres  6160  opeliunxp2f  6238  tpos0  6274  issmo  6288  tfrlem6  6316  tfrlem8  6318  tfri1dALT  6351  tfrcl  6364  rdgfun  6373  frecfun  6395  frecfcllem  6404  0lt1o  6440  eqer  6566  ecopover  6632  ecopoverg  6635  th3qcor  6638  mapsnf1o3  6696  ssdomg  6777  ensn1  6795  xpcomf1o  6824  fiunsnnn  6880  finexdc  6901  exmidpw  6907  dcfi  6979  omct  7115  infnninf  7121  infnninfOLD  7122  pm54.43  7188  exmidonfinlem  7191  pw1on  7224  pw1dom2  7225  pw1ne1  7227  2oneel  7254  dmaddpi  7323  dmmulpi  7324  1lt2pi  7338  indpi  7340  1lt2nq  7404  genpelxp  7509  ltexprlempr  7606  recexprlempr  7630  cauappcvgprlemcl  7651  cauappcvgprlemladd  7656  caucvgprlemcl  7674  caucvgprprlemcl  7702  m1p1sr  7758  m1m1sr  7759  0lt1sr  7763  peano1nnnn  7850  ax1cn  7859  ax1re  7860  axaddf  7866  axmulf  7867  ax0lt1  7874  0lt1  8082  subaddrii  8244  ixi  8538  1ap0  8545  sup3exmid  8912  nn1suc  8936  neg1lt0  9025  4d2e2  9077  iap0  9140  un0mulcl  9208  pnf0xnn0  9244  3halfnz  9348  nummac  9426  uzf  9529  mnfltpnf  9783  ixxf  9896  ioof  9969  fzf  10010  fzp1disj  10077  fzp1nel  10101  fzo0  10165  frecfzennn  10423  frechashgf1o  10425  fxnn0nninf  10435  seq3f1olemp  10499  sq0  10607  irec  10616  hash0  10771  prhash2ex  10784  climmo  11301  sum0  11391  fisumcom2  11441  prod0  11588  fprodcom2fi  11629  cos1bnd  11762  cos2bnd  11763  n2dvdsm1  11912  n2dvds3  11914  flodddiv4  11933  3lcm2e6woprm  12080  6lcm4e12  12081  2prm  12121  3lcm2e6  12154  pockthi  12350  unennn  12392  ssnnctlemct  12441  structcnvcnv  12472  strleun  12557  starvndxnbasendx  12594  starvndxnplusgndx  12595  starvndxnmulrndx  12596  scandxnbasendx  12606  scandxnplusgndx  12607  scandxnmulrndx  12608  vscandxnbasendx  12611  vscandxnplusgndx  12612  vscandxnmulrndx  12613  vscandxnscandx  12614  ipndxnbasendx  12624  ipndxnplusgndx  12625  ipndxnmulrndx  12626  slotsdifipndx  12627  tsetndxnplusgndx  12641  tsetndxnmulrndx  12642  tsetndxnstarvndx  12643  slotstnscsi  12644  plendxnplusgndx  12655  plendxnmulrndx  12656  plendxnscandx  12657  plendxnvscandx  12658  slotsdifplendx  12659  dsndxnplusgndx  12666  dsndxnmulrndx  12667  slotsdnscsi  12668  dsndxntsetndx  12669  slotsdifdsndx  12670  unifndxntsetndx  12676  slotsdifunifndx  12677  restid  12689  mgmidmo  12745  tgdom  13465  tgidm  13467  resttopon  13564  rest0  13572  psmetrel  13715  metrel  13735  xmetrel  13736  xmetf  13743  0met  13777  mopnrel  13834  setsmsbasg  13872  setsmsdsg  13873  qtopbasss  13914  reldvg  14041  dvexp  14068  dveflem  14080  efcn  14082  sinhalfpilem  14105  sincosq1lem  14139  tangtx  14152  sincos4thpi  14154  pigt3  14158  dfrelog  14174  relogf1o  14175  log1  14180  loge  14181  relogiso  14187  2logb9irr  14282  2logb9irrap  14288  2sqlem9  14353  2sqlem10  14354  ex-fl  14359  bj-nndcALT  14392  bj-axempty  14527  bj-axempty2  14528  bdinex1  14533  bj-zfpair2  14544  bj-uniex2  14550  bj-indint  14565  bj-omind  14568  bj-omex  14576  bj-omelon  14595  0nninf  14635  dceqnconst  14689  dcapnconst  14690