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  2026  dvelimfv  2027  dvelimor  2034  nfeuv  2060  moaneu  2118  moanmo  2119  eqeltri  2266  nfcxfr  2333  neir  2367  neirr  2373  eqnetri  2387  nesymir  2411  nelir  2462  mprgbir  2552  vex  2763  issetri  2769  moeq  2935  cdeqi  2970  ru  2984  eqsstri  3211  3sstr4i  3220  mosn  3654  rabrsndc  3686  tpid1  3729  tpid2  3731  tpid3  3734  pwv  3834  uni0  3862  eqbrtri  4050  tr0  4138  trv  4139  zfnuleu  4153  0ex  4156  inex1  4163  elpwi2  4187  0elpw  4193  axpow2  4205  axpow3  4206  vpwex  4208  zfpair2  4239  exss  4256  moop2  4280  pwundifss  4316  po0  4342  epse  4373  fr0  4382  0elon  4423  onm  4432  uniex2  4467  snnex  4479  ordtriexmidlem  4551  ordtriexmid  4553  ontr2exmid  4557  ordtri2or2exmidlem  4558  onsucsssucexmid  4559  onsucelsucexmidlem  4561  ruALT  4583  zfregfr  4606  dcextest  4613  zfinf2  4621  omex  4625  finds  4632  finds2  4633  ordom  4639  omsinds  4654  relsnop  4765  relxp  4768  rel0  4784  relopabiv  4785  relopabi  4787  eliunxp  4801  opeliunxp2  4802  dmi  4877  xpidtr  5056  cnvcnv  5118  dmsn0  5133  cnvsn0  5134  funmpt  5292  funmpt2  5293  funinsn  5303  isarep2  5341  f0  5444  f10  5534  f1o00  5535  f1oi  5538  f1osn  5540  brprcneu  5547  fvopab3ig  5631  opabex  5782  eufnfv  5789  mpofun  6020  reldmmpo  6030  ovid  6035  ovidig  6036  ovidi  6037  ovig  6040  ovi3  6055  oprabex  6180  oprabex3  6181  f1stres  6212  f2ndres  6213  opeliunxp2f  6291  tpos0  6327  issmo  6341  tfrlem6  6369  tfrlem8  6371  tfri1dALT  6404  tfrcl  6417  rdgfun  6426  frecfun  6448  frecfcllem  6457  0lt1o  6493  eqer  6619  ecopover  6687  ecopoverg  6690  th3qcor  6693  mapsnf1o3  6751  ssdomg  6832  ensn1  6850  xpcomf1o  6879  fiunsnnn  6937  finexdc  6958  exmidpw  6964  dcfi  7040  omct  7176  infnninf  7183  infnninfOLD  7184  pm54.43  7250  exmidonfinlem  7253  pw1on  7286  pw1dom2  7287  pw1ne1  7289  2oneel  7316  dmaddpi  7385  dmmulpi  7386  1lt2pi  7400  indpi  7402  1lt2nq  7466  genpelxp  7571  ltexprlempr  7668  recexprlempr  7692  cauappcvgprlemcl  7713  cauappcvgprlemladd  7718  caucvgprlemcl  7736  caucvgprprlemcl  7764  m1p1sr  7820  m1m1sr  7821  0lt1sr  7825  peano1nnnn  7912  ax1cn  7921  ax1re  7922  axaddf  7928  axmulf  7929  ax0lt1  7936  0lt1  8146  subaddrii  8308  ixi  8602  1ap0  8609  sup3exmid  8976  nn1suc  9001  neg1lt0  9090  4d2e2  9142  iap0  9205  un0mulcl  9274  pnf0xnn0  9310  3halfnz  9414  nummac  9492  uzf  9595  mnfltpnf  9851  ixxf  9964  ioof  10037  fzf  10078  fzp1disj  10146  fzp1nel  10170  fzo0  10235  frecfzennn  10497  frechashgf1o  10499  xnn0nnen  10508  fxnn0nninf  10510  seq3f1olemp  10586  sq0  10701  irec  10710  hash0  10867  prhash2ex  10880  climmo  11441  sum0  11531  fisumcom2  11581  prod0  11728  fprodcom2fi  11769  cos1bnd  11902  cos2bnd  11903  n2dvdsm1  12054  n2dvds3  12056  flodddiv4  12075  3lcm2e6woprm  12224  6lcm4e12  12225  2prm  12265  3lcm2e6  12298  pockthi  12496  unennn  12554  ssnnctlemct  12603  structcnvcnv  12634  strleun  12722  starvndxnbasendx  12759  starvndxnplusgndx  12760  starvndxnmulrndx  12761  scandxnbasendx  12771  scandxnplusgndx  12772  scandxnmulrndx  12773  vscandxnbasendx  12776  vscandxnplusgndx  12777  vscandxnmulrndx  12778  vscandxnscandx  12779  ipndxnbasendx  12789  ipndxnplusgndx  12790  ipndxnmulrndx  12791  slotsdifipndx  12792  tsetndxnplusgndx  12809  tsetndxnmulrndx  12810  tsetndxnstarvndx  12811  slotstnscsi  12812  plendxnplusgndx  12823  plendxnmulrndx  12824  plendxnscandx  12825  plendxnvscandx  12826  slotsdifplendx  12827  dsndxnplusgndx  12834  dsndxnmulrndx  12835  slotsdnscsi  12836  dsndxntsetndx  12837  slotsdifdsndx  12838  unifndxntsetndx  12844  slotsdifunifndx  12845  restid  12861  mgmidmo  12955  rrgmex  13757  lssmex  13851  lidlmex  13971  2idlmex  13997  fczpsrbag  14157  tgdom  14240  tgidm  14242  resttopon  14339  rest0  14347  psmetrel  14490  metrel  14510  xmetrel  14511  xmetf  14518  0met  14552  mopnrel  14609  setsmsbasg  14647  setsmsdsg  14648  qtopbasss  14689  reldvg  14833  dvexp  14860  dveflem  14872  elply2  14881  elplyd  14887  ply1term  14889  plymullem  14896  efcn  14903  sinhalfpilem  14926  sincosq1lem  14960  tangtx  14973  sincos4thpi  14975  pigt3  14979  dfrelog  14995  relogf1o  14996  log1  15001  loge  15002  relogiso  15008  2logb9irr  15103  2logb9irrap  15109  2sqlem9  15211  2sqlem10  15212  ex-fl  15217  bj-nndcALT  15250  bj-axempty  15385  bj-axempty2  15386  bdinex1  15391  bj-zfpair2  15402  bj-uniex2  15408  bj-indint  15423  bj-omind  15426  bj-omex  15434  bj-omelon  15453  0nninf  15494  dceqnconst  15550  dcapnconst  15551