Theorem mpbir 145

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

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74ri  180  imnani  681  stabnot  823  mpbir2an  932  mpbir3an  1169  tru  1347  mpgbir  1441  nfxfr  1462  19.8a  1578  sbt  1772  dveeq2  1803  dveeq2or  1804  sbequilem  1826  cbvex2  1910  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  nfeuv  2032  moaneu  2090  moanmo  2091  eqeltri  2238  nfcxfr  2304  neir  2338  neirr  2344  eqnetri  2358  nesymir  2382  nelir  2433  mprgbir  2523  vex  2728  issetri  2734  moeq  2900  cdeqi  2935  ru  2949  eqsstri  3173  3sstr4i  3182  rgenm  3510  mosn  3611  rabrsndc  3643  tpid1  3686  tpid2  3688  tpid3  3691  pwv  3787  uni0  3815  eqbrtri  4002  tr0  4090  trv  4091  zfnuleu  4105  0ex  4108  inex1  4115  elpwi2  4136  0elpw  4142  axpow2  4154  axpow3  4155  vpwex  4157  zfpair2  4187  exss  4204  moop2  4228  pwundifss  4262  po0  4288  epse  4319  fr0  4328  0elon  4369  onm  4378  uniex2  4413  snnex  4425  ordtriexmidlem  4495  ordtriexmid  4497  ontr2exmid  4501  ordtri2or2exmidlem  4502  onsucsssucexmid  4503  onsucelsucexmidlem  4505  ruALT  4527  zfregfr  4550  dcextest  4557  zfinf2  4565  omex  4569  finds  4576  finds2  4577  ordom  4583  omsinds  4598  relsnop  4709  relxp  4712  rel0  4728  relopabi  4729  eliunxp  4742  opeliunxp2  4743  dmi  4818  xpidtr  4993  cnvcnv  5055  dmsn0  5070  cnvsn0  5071  funmpt  5225  funmpt2  5226  funinsn  5236  isarep2  5274  f0  5377  f10  5465  f1o00  5466  f1oi  5469  f1osn  5471  brprcneu  5478  fvopab3ig  5559  opabex  5708  eufnfv  5714  mpofun  5940  reldmmpo  5949  ovid  5954  ovidig  5955  ovidi  5956  ovig  5959  ovi3  5974  oprabex  6093  oprabex3  6094  f1stres  6124  f2ndres  6125  opeliunxp2f  6202  tpos0  6238  issmo  6252  tfrlem6  6280  tfrlem8  6282  tfri1dALT  6315  tfrcl  6328  rdgfun  6337  frecfun  6359  frecfcllem  6368  0lt1o  6404  eqer  6529  ecopover  6595  ecopoverg  6598  th3qcor  6601  mapsnf1o3  6659  ssdomg  6740  ensn1  6758  xpcomf1o  6787  fiunsnnn  6843  finexdc  6864  exmidpw  6870  dcfi  6942  omct  7078  infnninf  7084  infnninfOLD  7085  pm54.43  7142  exmidonfinlem  7145  pw1on  7178  pw1dom2  7179  pw1ne1  7181  dmaddpi  7262  dmmulpi  7263  1lt2pi  7277  indpi  7279  1lt2nq  7343  genpelxp  7448  ltexprlempr  7545  recexprlempr  7569  cauappcvgprlemcl  7590  cauappcvgprlemladd  7595  caucvgprlemcl  7613  caucvgprprlemcl  7641  m1p1sr  7697  m1m1sr  7698  0lt1sr  7702  peano1nnnn  7789  ax1cn  7798  ax1re  7799  axaddf  7805  axmulf  7806  ax0lt1  7813  0lt1  8021  subaddrii  8183  ixi  8477  1ap0  8484  sup3exmid  8848  nn1suc  8872  neg1lt0  8961  4d2e2  9013  iap0  9076  un0mulcl  9144  pnf0xnn0  9180  3halfnz  9284  nummac  9362  uzf  9465  mnfltpnf  9717  ixxf  9830  ioof  9903  fzf  9944  fzp1disj  10011  fzp1nel  10035  fzo0  10099  frecfzennn  10357  frechashgf1o  10359  fxnn0nninf  10369  seq3f1olemp  10433  sq0  10541  irec  10550  hash0  10706  prhash2ex  10718  climmo  11235  sum0  11325  fisumcom2  11375  prod0  11522  fprodcom2fi  11563  cos1bnd  11696  cos2bnd  11697  n2dvdsm1  11846  n2dvds3  11848  flodddiv4  11867  3lcm2e6woprm  12014  6lcm4e12  12015  2prm  12055  3lcm2e6  12088  pockthi  12284  unennn  12326  ssnnctlemct  12375  structcnvcnv  12406  strleun  12479  restid  12562  tgdom  12672  tgidm  12674  resttopon  12771  rest0  12779  psmetrel  12922  metrel  12942  xmetrel  12943  xmetf  12950  0met  12984  mopnrel  13041  setsmsbasg  13079  setsmsdsg  13080  qtopbasss  13121  reldvg  13248  dvexp  13275  dveflem  13287  efcn  13289  sinhalfpilem  13312  sincosq1lem  13346  tangtx  13359  sincos4thpi  13361  pigt3  13365  dfrelog  13381  relogf1o  13382  log1  13387  loge  13388  relogiso  13394  2logb9irr  13489  2logb9irrap  13495  2sqlem9  13560  2sqlem10  13561  ex-fl  13566  bj-nndcALT  13599  bj-axempty  13735  bj-axempty2  13736  bdinex1  13741  bj-zfpair2  13752  bj-uniex2  13758  bj-indint  13773  bj-omind  13776  bj-omex  13784  bj-omelon  13803  0nninf  13844  dceqnconst  13898  dcapnconst  13899