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  697  stabnot  840  mpbir2an  950  mpbir3an  1205  tru  1401  dcfromnotnotr  1492  dcfromcon  1493  dcfrompeirce  1494  mpgbir  1501  nfxfr  1522  19.8a  1638  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  2371  neir  2405  neirr  2411  eqnetri  2425  nesymir  2449  nelir  2500  mprgbir  2590  vex  2805  issetri  2812  moeq  2981  cdeqi  3016  ru  3030  eqsstri  3259  3sstr4i  3268  mosn  3705  rabrsndc  3739  tpid1  3783  tpid2  3785  tpid3  3788  pwv  3892  uni0  3920  eqbrtri  4109  tr0  4198  trv  4199  zfnuleu  4213  0ex  4216  inex1  4223  elpwi2  4248  0elpw  4254  axpow2  4266  axpow3  4267  vpwex  4269  zfpair2  4300  exss  4319  opwo0id  4341  moop2  4344  pwundifss  4382  po0  4408  epse  4439  fr0  4448  0elon  4489  onm  4498  uniex2  4533  snnex  4545  ordtriexmidlem  4617  ordtriexmid  4619  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucsssucexmid  4625  onsucelsucexmidlem  4627  ruALT  4649  zfregfr  4672  dcextest  4679  zfinf2  4687  omex  4691  finds  4698  finds2  4699  ordom  4705  omsinds  4720  relsnop  4832  relxp  4835  rel0  4852  relopabiv  4853  relopabi  4855  eliunxp  4869  opeliunxp2  4870  dmi  4946  xpidtr  5127  cnvcnv  5189  dmsn0  5204  cnvsn0  5205  funmpt  5364  funmpt2  5365  funinsn  5379  isarep2  5417  f0  5527  f10  5618  f10d  5619  f1o00  5620  f1oi  5623  f1osn  5625  brprcneu  5632  fvopab3ig  5720  opabex  5877  eufnfv  5884  mpofun  6122  reldmmpo  6132  ovid  6137  ovidig  6138  ovidi  6139  ovig  6142  ovi3  6158  relmptopab  6223  oprabex  6289  oprabex3  6290  f1stres  6321  f2ndres  6322  opeliunxp2f  6403  tpos0  6439  issmo  6453  tfrlem6  6481  tfrlem8  6483  tfri1dALT  6516  tfrcl  6529  rdgfun  6538  frecfun  6560  frecfcllem  6569  0lt1o  6607  eqer  6733  ecopover  6801  ecopoverg  6804  th3qcor  6807  mapsnf1o3  6865  ssdomg  6951  ensn1  6969  xpcomf1o  7008  fiunsnnn  7069  finexdc  7091  elssdc  7093  exmidpw  7099  dcfi  7179  omct  7315  infnninf  7322  infnninfOLD  7323  pm54.43  7394  exmidonfinlem  7403  pw1on  7443  pw1dom2  7444  pw1ne1  7446  2oneel  7474  dmaddpi  7544  dmmulpi  7545  1lt2pi  7559  indpi  7561  1lt2nq  7625  genpelxp  7730  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  cauappcvgprlemladd  7877  caucvgprlemcl  7895  caucvgprprlemcl  7923  m1p1sr  7979  m1m1sr  7980  0lt1sr  7984  peano1nnnn  8071  ax1cn  8080  ax1re  8081  axaddf  8087  axmulf  8088  ax0lt1  8095  0lt1  8305  subaddrii  8467  ixi  8762  1ap0  8769  sup3exmid  9136  nn1suc  9161  neg1lt0  9250  4d2e2  9303  iap0  9366  un0mulcl  9435  pnf0xnn0  9471  3halfnz  9576  nummac  9654  uzf  9757  mnfltpnf  10019  ixxf  10132  ioof  10205  fzf  10246  fzp1disj  10314  fzp1nel  10338  fzo0  10404  frecfzennn  10687  frechashgf1o  10689  xnn0nnen  10698  fxnn0nninf  10700  seq3f1olemp  10776  sq0  10891  irec  10900  hash0  11057  prhash2ex  11072  climmo  11858  sum0  11948  fisumcom2  11998  prod0  12145  fprodcom2fi  12186  cos1bnd  12319  cos2bnd  12320  3dvds  12424  n2dvdsm1  12473  n2dvds3  12475  flodddiv4  12496  3lcm2e6woprm  12657  6lcm4e12  12658  2prm  12698  3lcm2e6  12731  pockthi  12930  modsubi  12991  unennn  13017  ssnnctlemct  13066  structcnvcnv  13097  strleun  13186  starvndxnbasendx  13224  starvndxnplusgndx  13225  starvndxnmulrndx  13226  scandxnbasendx  13236  scandxnplusgndx  13237  scandxnmulrndx  13238  vscandxnbasendx  13241  vscandxnplusgndx  13242  vscandxnmulrndx  13243  vscandxnscandx  13244  ipndxnbasendx  13254  ipndxnplusgndx  13255  ipndxnmulrndx  13256  slotsdifipndx  13257  tsetndxnplusgndx  13274  tsetndxnmulrndx  13275  tsetndxnstarvndx  13276  slotstnscsi  13277  plendxnplusgndx  13288  plendxnmulrndx  13289  plendxnscandx  13290  plendxnvscandx  13291  slotsdifplendx  13292  basendxnocndx  13295  plendxnocndx  13296  dsndxnplusgndx  13303  dsndxnmulrndx  13304  slotsdnscsi  13305  dsndxntsetndx  13306  slotsdifdsndx  13307  unifndxntsetndx  13313  slotsdifunifndx  13314  restid  13332  prdsval  13355  mgmidmo  13454  reldvdsr  14104  rrgmex  14274  lssmex  14368  lidlmex  14488  2idlmex  14514  fczpsrbag  14684  tgdom  14795  tgidm  14797  resttopon  14894  rest0  14902  psmetrel  15045  metrel  15065  xmetrel  15066  xmetf  15073  0met  15107  mopnrel  15164  setsmsbasg  15202  setsmsdsg  15203  qtopbasss  15244  reldvg  15402  dvexp  15434  dveflem  15449  elply2  15458  elplyd  15464  ply1term  15466  plymullem  15473  efcn  15491  sinhalfpilem  15514  sincosq1lem  15548  tangtx  15561  sincos4thpi  15563  pigt3  15567  dfrelog  15583  relogf1o  15584  log1  15589  loge  15590  relogiso  15596  2logb9irr  15694  2logb9irrap  15700  2sqlem9  15852  2sqlem10  15853  uhgr0e  15932  uhgr0  15935  umgrbien  15960  usgr0  16089  griedg0prc  16100  1loopgruspgr  16153  ex-fl  16321  bj-nndcALT  16354  bj-axempty  16488  bj-axempty2  16489  bdinex1  16494  bj-zfpair2  16505  bj-uniex2  16511  bj-indint  16526  bj-omind  16529  bj-omex  16537  bj-omelon  16556  pw1ndom3  16589  0nninf  16606  dceqnconst  16664  dcapnconst  16665  gfsum0  16682