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  698  stabnot  841  mpbir2an  951  mpbir3an  1206  tru  1402  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  mpgbir  1502  nfxfr  1523  19.8a  1639  sbt  1832  dveeq2  1863  dveeq2or  1864  sbequilem  1886  cbvex2  1971  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  nfeuv  2097  moaneu  2156  moanmo  2157  eqeltri  2304  nfcxfr  2372  neir  2406  neirr  2412  eqnetri  2426  nesymir  2450  nelir  2501  mprgbir  2591  vex  2806  issetri  2813  moeq  2982  cdeqi  3017  ru  3031  eqsstri  3260  3sstr4i  3269  mosn  3709  rabrsndc  3743  tpid1  3787  tpid2  3789  tpid3  3792  pwv  3897  uni0  3925  eqbrtri  4114  tr0  4203  trv  4204  zfnuleu  4218  0ex  4221  inex1  4228  elpwi2  4253  0elpw  4260  axpow2  4272  axpow3  4273  vpwex  4275  zfpair2  4306  exss  4325  opwo0id  4347  moop2  4350  pwundifss  4388  po0  4414  epse  4445  fr0  4454  0elon  4495  onm  4504  uniex2  4539  snnex  4551  ordtriexmidlem  4623  ordtriexmid  4625  ontr2exmid  4629  ordtri2or2exmidlem  4630  onsucsssucexmid  4631  onsucelsucexmidlem  4633  ruALT  4655  zfregfr  4678  dcextest  4685  zfinf2  4693  omex  4697  finds  4704  finds2  4705  ordom  4711  omsinds  4726  relsnop  4838  relxp  4841  rel0  4858  relopabiv  4859  relopabi  4861  eliunxp  4875  opeliunxp2  4876  dmi  4952  xpidtr  5134  cnvcnv  5196  dmsn0  5211  cnvsn0  5212  funmpt  5371  funmpt2  5372  funinsn  5386  isarep2  5424  f0  5536  f10  5627  f10d  5628  f1o00  5629  f1oi  5632  f1osn  5634  brprcneu  5641  fvopab3ig  5729  opabex  5888  eufnfv  5895  mpofun  6133  reldmmpo  6143  ovid  6148  ovidig  6149  ovidi  6150  ovig  6153  ovi3  6169  relmptopab  6234  oprabex  6299  oprabex3  6300  f1stres  6331  f2ndres  6332  opeliunxp2f  6447  tpos0  6483  issmo  6497  tfrlem6  6525  tfrlem8  6527  tfri1dALT  6560  tfrcl  6573  rdgfun  6582  frecfun  6604  frecfcllem  6613  0lt1o  6651  eqer  6777  ecopover  6845  ecopoverg  6848  th3qcor  6851  mapsnf1o3  6909  ssdomg  6995  ensn1  7013  xpcomf1o  7052  fiunsnnn  7113  finexdc  7135  elssdc  7137  exmidpw  7143  dcfi  7223  omct  7359  infnninf  7366  infnninfOLD  7367  pm54.43  7438  exmidonfinlem  7447  pw1on  7487  pw1dom2  7488  pw1ne1  7490  2oneel  7518  dmaddpi  7588  dmmulpi  7589  1lt2pi  7603  indpi  7605  1lt2nq  7669  genpelxp  7774  ltexprlempr  7871  recexprlempr  7895  cauappcvgprlemcl  7916  cauappcvgprlemladd  7921  caucvgprlemcl  7939  caucvgprprlemcl  7967  m1p1sr  8023  m1m1sr  8024  0lt1sr  8028  peano1nnnn  8115  ax1cn  8124  ax1re  8125  axaddf  8131  axmulf  8132  ax0lt1  8139  0lt1  8348  subaddrii  8510  ixi  8805  1ap0  8812  sup3exmid  9179  nn1suc  9204  neg1lt0  9293  4d2e2  9346  iap0  9409  un0mulcl  9478  pnf0xnn0  9516  3halfnz  9621  nummac  9699  uzf  9802  mnfltpnf  10064  ixxf  10177  ioof  10250  fzf  10292  fzp1disj  10360  fzp1nel  10384  fzo0  10450  frecfzennn  10734  frechashgf1o  10736  xnn0nnen  10745  fxnn0nninf  10747  seq3f1olemp  10823  sq0  10938  irec  10947  hash0  11104  prhash2ex  11119  climmo  11921  sum0  12012  fisumcom2  12062  prod0  12209  fprodcom2fi  12250  cos1bnd  12383  cos2bnd  12384  3dvds  12488  n2dvdsm1  12537  n2dvds3  12539  flodddiv4  12560  3lcm2e6woprm  12721  6lcm4e12  12722  2prm  12762  3lcm2e6  12795  pockthi  12994  modsubi  13055  unennn  13081  ssnnctlemct  13130  structcnvcnv  13161  strleun  13250  starvndxnbasendx  13288  starvndxnplusgndx  13289  starvndxnmulrndx  13290  scandxnbasendx  13300  scandxnplusgndx  13301  scandxnmulrndx  13302  vscandxnbasendx  13305  vscandxnplusgndx  13306  vscandxnmulrndx  13307  vscandxnscandx  13308  ipndxnbasendx  13318  ipndxnplusgndx  13319  ipndxnmulrndx  13320  slotsdifipndx  13321  tsetndxnplusgndx  13338  tsetndxnmulrndx  13339  tsetndxnstarvndx  13340  slotstnscsi  13341  plendxnplusgndx  13352  plendxnmulrndx  13353  plendxnscandx  13354  plendxnvscandx  13355  slotsdifplendx  13356  basendxnocndx  13359  plendxnocndx  13360  dsndxnplusgndx  13367  dsndxnmulrndx  13368  slotsdnscsi  13369  dsndxntsetndx  13370  slotsdifdsndx  13371  unifndxntsetndx  13377  slotsdifunifndx  13378  restid  13396  prdsval  13419  mgmidmo  13518  reldvdsr  14169  rrgmex  14339  lssmex  14434  lidlmex  14554  2idlmex  14580  fczpsrbag  14750  tgdom  14866  tgidm  14868  resttopon  14965  rest0  14973  psmetrel  15116  metrel  15136  xmetrel  15137  xmetf  15144  0met  15178  mopnrel  15235  setsmsbasg  15273  setsmsdsg  15274  qtopbasss  15315  reldvg  15473  dvexp  15505  dveflem  15520  elply2  15529  elplyd  15535  ply1term  15537  plymullem  15544  efcn  15562  sinhalfpilem  15585  sincosq1lem  15619  tangtx  15632  sincos4thpi  15634  pigt3  15638  dfrelog  15654  relogf1o  15655  log1  15660  loge  15661  relogiso  15667  2logb9irr  15765  2logb9irrap  15771  2sqlem9  15926  2sqlem10  15927  uhgr0e  16006  uhgr0  16009  umgrbien  16034  usgr0  16163  griedg0prc  16174  1loopgruspgr  16227  konigsbergumgr  16411  konigsberglem1  16412  ex-fl  16422  bj-nndcALT  16459  bj-axempty  16592  bj-axempty2  16593  bdinex1  16598  bj-zfpair2  16609  bj-uniex2  16615  bj-indint  16630  bj-omind  16633  bj-omex  16641  bj-omelon  16660  pw1ndom3  16693  0nninf  16713  dceqnconst  16776  dcapnconst  16777  gfsum0  16794