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  702  stabnot  845  mpbir2an  955  mpbir3an  1210  tru  1406  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  mpgbir  1506  nfxfr  1527  19.8a  1643  sbt  1837  dveeq2  1868  dveeq2or  1869  sbequilem  1891  cbvex2  1978  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  nfeuv  2104  moaneu  2163  moanmo  2164  eqeltri  2311  nfcxfr  2389  neir  2423  neirr  2429  eqnetri  2443  nesymir  2467  nelir  2518  mprgbir  2608  vex  2824  issetri  2831  moeq  3001  cdeqi  3036  ru  3050  eqsstri  3280  3sstr4i  3289  mosn  3741  rabrsndc  3775  tpid1  3819  tpid2  3821  tpid3  3824  pwv  3929  uni0  3957  eqbrtri  4146  tr0  4235  trv  4236  zfnuleu  4252  0ex  4255  inex1  4262  elpwi2  4289  0elpw  4296  axpow2  4308  axpow3  4309  vpwex  4311  zfpair2  4342  exss  4362  opwo0id  4384  moop2  4387  pwundifss  4425  po0  4451  epse  4482  fr0  4491  0elon  4532  onm  4541  uniex2  4576  uniex2OLD  4577  snnex  4589  ordtriexmidlem  4661  ordtriexmid  4663  ontr2exmid  4667  ordtri2or2exmidlem  4668  onsucsssucexmid  4669  onsucelsucexmidlem  4671  ruALT  4693  zfregfr  4716  dcextest  4723  zfinf2  4731  omex  4735  finds  4742  finds2  4743  ordom  4749  omsinds  4764  relsnop  4876  relxp  4879  rel0  4897  relopabiv  4898  relopabi  4900  eliunxp  4914  opeliunxp2  4915  dmi  4991  xpidtr  5173  cnvcnv  5235  dmsn0  5250  cnvsn0  5251  funmpt  5410  funmpt2  5411  funinsn  5425  isarep2  5463  f0  5578  f10  5669  f10d  5670  f1o00  5671  f1oi  5674  f1osn  5676  brprcneu  5683  fvopab3ig  5773  opabex  5932  eufnfv  5939  rinvf1o  6025  mpofun  6180  reldmmpo  6190  ovid  6195  ovidig  6196  ovidi  6197  ovig  6200  ovi3  6216  relmptopab  6281  oprabex  6351  oprabex3  6352  f1stres  6383  f2ndres  6384  opeliunxp2f  6499  tpos0  6535  issmo  6549  tfrlem6  6577  tfrlem8  6579  tfri1dALT  6612  tfrcl  6625  rdgfun  6634  frecfun  6656  frecfcllem  6665  0lt1o  6703  eqer  6829  ecopover  6897  ecopoverg  6900  th3qcor  6903  mapsnf1o3  6969  ssdomg  7055  ensn1  7073  xpcomf1o  7113  fiunsnnn  7175  finexdc  7197  elssdc  7199  exmidpw  7205  fissfi  7253  dcfi  7305  omct  7447  infnninf  7454  infnninfOLD  7455  pm54.43  7526  exmidonfinlem  7535  pw1on  7575  pw1dom2  7576  pw1ne1  7578  2oneel  7612  dmaddpi  7682  dmmulpi  7683  1lt2pi  7697  indpi  7699  1lt2nq  7763  genpelxp  7868  ltexprlempr  7965  recexprlempr  7989  cauappcvgprlemcl  8010  cauappcvgprlemladd  8015  caucvgprlemcl  8033  caucvgprprlemcl  8061  m1p1sr  8117  m1m1sr  8118  0lt1sr  8122  peano1nnnn  8209  ax1cn  8218  ax1re  8219  axaddf  8225  axmulf  8226  ax0lt1  8233  0lt1  8443  subaddrii  8605  ixi  8901  1ap0  8908  sup3exmid  9277  nn1suc  9302  neg1lt0  9391  4d2e2  9444  iap0  9507  un0mulcl  9576  pnf0xnn0  9616  3halfnz  9722  nummac  9800  uzf  9903  mnfltpnf  10166  ixxf  10279  ioof  10352  fzf  10394  fzp1disj  10465  fzp1nel  10489  fzo0  10555  frecfzennn  10841  frechashgf1o  10843  xnn0nnen  10852  fxnn0nninf  10854  seq3f1olemp  10930  sq0  11045  irec  11054  hash0  11213  prhash2ex  11228  hashfibclem  11260  hashf1lem1  11263  climmo  12042  sum0  12133  fisumcom2  12183  prod0  12330  fprodcom2fi  12371  cos1bnd  12504  cos2bnd  12505  3dvds  12609  n2dvdsm1  12658  n2dvds3  12660  flodddiv4  12681  3lcm2e6woprm  12842  6lcm4e12  12843  2prm  12883  3lcm2e6  12916  pockthi  13115  modsubi  13176  ballotfilemcdc  13201  ballotfilem2  13206  ballotfilemic  13228  ballotfilem7  13257  ballotfilemth  13259  unennn  13266  ssnnctlemct  13315  structcnvcnv  13346  strleun  13435  starvndxnbasendx  13473  starvndxnplusgndx  13474  starvndxnmulrndx  13475  scandxnbasendx  13485  scandxnplusgndx  13486  scandxnmulrndx  13487  vscandxnbasendx  13490  vscandxnplusgndx  13491  vscandxnmulrndx  13492  vscandxnscandx  13493  ipndxnbasendx  13503  ipndxnplusgndx  13504  ipndxnmulrndx  13505  slotsdifipndx  13506  tsetndxnplusgndx  13523  tsetndxnmulrndx  13524  tsetndxnstarvndx  13525  slotstnscsi  13526  plendxnplusgndx  13537  plendxnmulrndx  13538  plendxnscandx  13539  plendxnvscandx  13540  slotsdifplendx  13541  basendxnocndx  13544  plendxnocndx  13545  dsndxnplusgndx  13552  dsndxnmulrndx  13553  slotsdnscsi  13554  dsndxntsetndx  13555  slotsdifdsndx  13556  unifndxntsetndx  13562  slotsdifunifndx  13563  restid  13581  mgmidmo  13669  gsum0cmn  14131  prdsval  14150  opprringb  14359  reldvdsr  14371  rrgmex  14542  lssmex  14664  lidlmex  14784  2idlmex  14810  fczpsrbag  14979  tgdom  15096  tgidm  15098  resttopon  15195  rest0  15203  psmetrel  15346  metrel  15366  xmetrel  15367  xmetf  15374  0met  15408  mopnrel  15465  setsmsbasg  15503  setsmsdsg  15504  qtopbasss  15545  reldvg  15703  dvexp  15735  dveflem  15750  elply2  15759  elplyd  15765  ply1term  15767  plymullem  15774  efcn  15792  sinhalfpilem  15815  sincosq1lem  15849  tangtx  15862  sincos4thpi  15864  pigt3  15868  dfrelog  15884  relogf1o  15885  log1  15890  loge  15891  relogiso  15897  2logb9irr  15996  2logb9irrap  16002  2sqlem9  16157  2sqlem10  16158  uhgr0e  16237  uhgr0  16240  umgrbien  16265  usgr0  16394  griedg0prc  16405  1loopgruspgr  16458  konigsbergumgr  16642  konigsberglem1  16643  ex-fl  16653  bj-nndcALT  16700  bj-axempty  16833  bj-axempty2  16834  bdinex1  16839  bj-zfpair2  16850  bj-uniex2  16856  bj-indint  16871  bj-omind  16874  bj-omex  16882  bj-omelon  16901  pw1ndom3  16934  0nninf  16952  dceqnconst  17015  dcapnconst  17016