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

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3745  rabrsndc  3779  tpid1  3824  tpid2  3826  tpid3  3829  pwv  3934  uni0  3962  eqbrtri  4152  tr0  4242  trv  4243  zfnuleu  4259  0ex  4262  inex1  4269  elpwi2  4296  0elpw  4303  axpow2  4315  axpow3  4316  vpwex  4318  zfpair2  4349  exss  4369  opwo0id  4391  moop2  4394  pwundifss  4432  po0  4458  epse  4489  fr0  4498  0elon  4539  onm  4548  uniex2  4583  uniex2OLD  4584  snnex  4596  ordtriexmidlem  4668  ordtriexmid  4670  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucsssucexmid  4676  onsucelsucexmidlem  4678  ruALT  4700  zfregfr  4723  dcextest  4730  zfinf2  4738  omex  4742  finds  4749  finds2  4750  ordom  4756  omsinds  4771  relsnop  4883  relxp  4886  rel0  4904  relopabiv  4905  relopabi  4907  eliunxp  4921  opeliunxp2  4922  dmi  4998  xpidtr  5181  cnvcnv  5243  dmsn0  5258  cnvsn0  5259  funmpt  5418  funmpt2  5419  funinsn  5433  isarep2  5471  f0  5586  f10  5677  f10d  5678  f1o00  5679  f1oi  5682  f1osn  5684  brprcneu  5691  fvopab3ig  5782  opabex  5944  eufnfv  5952  rinvf1o  6038  mpofun  6193  reldmmpo  6203  ovid  6208  ovidig  6209  ovidi  6210  ovig  6213  ovi3  6229  relmptopab  6294  oprabex  6365  oprabex3  6366  f1stres  6397  f2ndres  6398  opeliunxp2f  6514  tpos0  6550  issmo  6564  tfrlem6  6592  tfrlem8  6594  tfri1dALT  6627  tfrcl  6640  rdgfun  6649  frecfun  6671  frecfcllem  6680  0lt1o  6718  eqer  6844  ecopover  6912  ecopoverg  6915  th3qcor  6918  mapsnf1o3  6985  ssdomg  7071  ensn1  7089  xpcomf1o  7129  fiunsnnn  7191  finexdc  7213  elssdc  7215  exmidpw  7221  fissfi  7269  dcfi  7320  omct  7463  infnninf  7470  infnninfOLD  7471  pm54.43  7542  exmidonfinlem  7551  pw1on  7591  pw1dom2  7592  pw1ne1  7594  2oneel  7628  dmaddpi  7698  dmmulpi  7699  1lt2pi  7713  indpi  7715  1lt2nq  7779  genpelxp  7884  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  cauappcvgprlemladd  8031  caucvgprlemcl  8049  caucvgprprlemcl  8077  m1p1sr  8133  m1m1sr  8134  0lt1sr  8138  peano1nnnn  8225  ax1cn  8234  ax1re  8235  axaddf  8241  axmulf  8242  ax0lt1  8249  0lt1  8460  subaddrii  8622  ixi  8919  1ap0  8926  sup3exmid  9295  indconst0  9311  nn1suc  9332  neg1lt0  9421  4d2e2  9476  iap0  9539  un0mulcl  9608  pnf0xnn0  9646  3halfnz  9753  nummac  9836  uzf  9939  mnfltpnf  10203  ixxf  10316  ioof  10389  fzf  10431  fzp1disj  10503  fzp1nel  10527  fzo0  10593  frecfzennn  10883  frechashgf1o  10885  xnn0nnen  10894  fxnn0nninf  10896  seq3f1olemp  10972  sq0  11087  irec  11096  hash0  11256  prhash2ex  11271  hashfibclem  11303  hashf1lem1  11306  climmo  12088  sum0  12179  fisumcom2  12229  prod0  12376  fprodcom2fi  12417  cos1bnd  12550  cos2bnd  12551  3dvds  12655  n2dvdsm1  12704  n2dvds3  12706  flodddiv4  12727  3lcm2e6woprm  12888  6lcm4e12  12889  2prm  12929  3lcm2e6  12963  pockthi  13165  mod2xnegi  13226  modsubi  13227  ballotfilemcdc  13280  ballotfilem2  13285  ballotfilemic  13307  ballotfilem7  13336  ballotfilemth  13338  unennn  13345  ssnnctlemct  13394  structcnvcnv  13425  strleun  13516  starvndxnbasendx  13554  starvndxnplusgndx  13555  starvndxnmulrndx  13556  scandxnbasendx  13566  scandxnplusgndx  13567  scandxnmulrndx  13568  vscandxnbasendx  13571  vscandxnplusgndx  13572  vscandxnmulrndx  13573  vscandxnscandx  13574  ipndxnbasendx  13584  ipndxnplusgndx  13585  ipndxnmulrndx  13586  slotsdifipndx  13587  tsetndxnplusgndx  13604  tsetndxnmulrndx  13605  tsetndxnstarvndx  13606  slotstnscsi  13607  plendxnplusgndx  13618  plendxnmulrndx  13619  plendxnscandx  13620  plendxnvscandx  13621  slotsdifplendx  13622  basendxnocndx  13625  plendxnocndx  13626  dsndxnplusgndx  13633  dsndxnmulrndx  13634  slotsdnscsi  13635  dsndxntsetndx  13636  slotsdifdsndx  13637  unifndxntsetndx  13643  slotsdifunifndx  13644  restid  13662  mgmidmo  13750  gsum0cmn  14243  gsum2d2fi  14273  gsumcom2fi  14274  prdsval  14279  mgpplusg  14328  ringidval  14371  opprringb  14494  reldvdsr  14506  rrgmex  14677  lssmex  14800  lidlmex  14920  2idlmex  14946  asclfval  15129  fczpsrbag  15169  tgdom  15315  tgidm  15317  resttopon  15414  rest0  15422  psmetrel  15565  metrel  15585  xmetrel  15586  xmetf  15593  0met  15627  mopnrel  15684  setsmsbasg  15722  setsmsdsg  15723  qtopbasss  15764  reldvg  15922  dvexp  15954  dveflem  15969  elply2  15978  elplyd  15984  ply1term  15986  plymullem  15993  efcn  16011  sinhalfpilem  16035  sincosq1lem  16069  tangtx  16082  sincos4thpi  16084  pigt3  16088  dfrelog  16106  relogf1o  16107  log1  16112  loge  16113  relogiso  16120  2logb9irr  16224  2logb9irrap  16230  log2ublem1  16238  birthdaylog2  16245  ppiqltx  16298  ppiublem1  16308  ppiqub  16310  bclbnd  16324  bpos1lem  16326  bposlem8  16335  2sqlem9  16465  2sqlem10  16466  uhgr0e  16545  uhgr0  16548  umgrbien  16573  usgr0  16702  griedg0prc  16713  1loopgruspgr  16766  konigsbergumgr  16950  konigsberglem1  16951  ex-fl  16961  bj-nndcALT  17008  bj-axempty  17141  bj-axempty2  17142  bdinex1  17147  bj-zfpair2  17158  bj-uniex2  17164  bj-indint  17179  bj-omind  17182  bj-omex  17190  bj-omelon  17209  pw1ndom3  17242  wexmiddifxylem  17267  0nninf  17270  dceqnconst  17334  dcapnconst  17335