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  695  stabnot  838  mpbir2an  948  mpbir3an  1203  tru  1399  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpgbir  1499  nfxfr  1520  19.8a  1636  sbt  1830  dveeq2  1861  dveeq2or  1862  sbequilem  1884  cbvex2  1969  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  nfeuv  2095  moaneu  2154  moanmo  2155  eqeltri  2302  nfcxfr  2369  neir  2403  neirr  2409  eqnetri  2423  nesymir  2447  nelir  2498  mprgbir  2588  vex  2803  issetri  2810  moeq  2979  cdeqi  3014  ru  3028  eqsstri  3257  3sstr4i  3266  mosn  3703  rabrsndc  3737  tpid1  3781  tpid2  3783  tpid3  3786  pwv  3890  uni0  3918  eqbrtri  4107  tr0  4196  trv  4197  zfnuleu  4211  0ex  4214  inex1  4221  elpwi2  4246  0elpw  4252  axpow2  4264  axpow3  4265  vpwex  4267  zfpair2  4298  exss  4317  opwo0id  4339  moop2  4342  pwundifss  4380  po0  4406  epse  4437  fr0  4446  0elon  4487  onm  4496  uniex2  4531  snnex  4543  ordtriexmidlem  4615  ordtriexmid  4617  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucsssucexmid  4623  onsucelsucexmidlem  4625  ruALT  4647  zfregfr  4670  dcextest  4677  zfinf2  4685  omex  4689  finds  4696  finds2  4697  ordom  4703  omsinds  4718  relsnop  4830  relxp  4833  rel0  4850  relopabiv  4851  relopabi  4853  eliunxp  4867  opeliunxp2  4868  dmi  4944  xpidtr  5125  cnvcnv  5187  dmsn0  5202  cnvsn0  5203  funmpt  5362  funmpt2  5363  funinsn  5376  isarep2  5414  f0  5524  f10  5614  f10d  5615  f1o00  5616  f1oi  5619  f1osn  5621  brprcneu  5628  fvopab3ig  5716  opabex  5873  eufnfv  5880  mpofun  6118  reldmmpo  6128  ovid  6133  ovidig  6134  ovidi  6135  ovig  6138  ovi3  6154  relmptopab  6219  oprabex  6285  oprabex3  6286  f1stres  6317  f2ndres  6318  opeliunxp2f  6399  tpos0  6435  issmo  6449  tfrlem6  6477  tfrlem8  6479  tfri1dALT  6512  tfrcl  6525  rdgfun  6534  frecfun  6556  frecfcllem  6565  0lt1o  6603  eqer  6729  ecopover  6797  ecopoverg  6800  th3qcor  6803  mapsnf1o3  6861  ssdomg  6947  ensn1  6965  xpcomf1o  7004  fiunsnnn  7063  finexdc  7085  elssdc  7087  exmidpw  7093  dcfi  7171  omct  7307  infnninf  7314  infnninfOLD  7315  pm54.43  7386  exmidonfinlem  7394  pw1on  7434  pw1dom2  7435  pw1ne1  7437  2oneel  7465  dmaddpi  7535  dmmulpi  7536  1lt2pi  7550  indpi  7552  1lt2nq  7616  genpelxp  7721  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  cauappcvgprlemladd  7868  caucvgprlemcl  7886  caucvgprprlemcl  7914  m1p1sr  7970  m1m1sr  7971  0lt1sr  7975  peano1nnnn  8062  ax1cn  8071  ax1re  8072  axaddf  8078  axmulf  8079  ax0lt1  8086  0lt1  8296  subaddrii  8458  ixi  8753  1ap0  8760  sup3exmid  9127  nn1suc  9152  neg1lt0  9241  4d2e2  9294  iap0  9357  un0mulcl  9426  pnf0xnn0  9462  3halfnz  9567  nummac  9645  uzf  9748  mnfltpnf  10010  ixxf  10123  ioof  10196  fzf  10237  fzp1disj  10305  fzp1nel  10329  fzo0  10395  frecfzennn  10678  frechashgf1o  10680  xnn0nnen  10689  fxnn0nninf  10691  seq3f1olemp  10767  sq0  10882  irec  10891  hash0  11048  prhash2ex  11063  climmo  11849  sum0  11939  fisumcom2  11989  prod0  12136  fprodcom2fi  12177  cos1bnd  12310  cos2bnd  12311  3dvds  12415  n2dvdsm1  12464  n2dvds3  12466  flodddiv4  12487  3lcm2e6woprm  12648  6lcm4e12  12649  2prm  12689  3lcm2e6  12722  pockthi  12921  modsubi  12982  unennn  13008  ssnnctlemct  13057  structcnvcnv  13088  strleun  13177  starvndxnbasendx  13215  starvndxnplusgndx  13216  starvndxnmulrndx  13217  scandxnbasendx  13227  scandxnplusgndx  13228  scandxnmulrndx  13229  vscandxnbasendx  13232  vscandxnplusgndx  13233  vscandxnmulrndx  13234  vscandxnscandx  13235  ipndxnbasendx  13245  ipndxnplusgndx  13246  ipndxnmulrndx  13247  slotsdifipndx  13248  tsetndxnplusgndx  13265  tsetndxnmulrndx  13266  tsetndxnstarvndx  13267  slotstnscsi  13268  plendxnplusgndx  13279  plendxnmulrndx  13280  plendxnscandx  13281  plendxnvscandx  13282  slotsdifplendx  13283  basendxnocndx  13286  plendxnocndx  13287  dsndxnplusgndx  13294  dsndxnmulrndx  13295  slotsdnscsi  13296  dsndxntsetndx  13297  slotsdifdsndx  13298  unifndxntsetndx  13304  slotsdifunifndx  13305  restid  13323  prdsval  13346  mgmidmo  13445  reldvdsr  14095  rrgmex  14265  lssmex  14359  lidlmex  14479  2idlmex  14505  fczpsrbag  14675  tgdom  14786  tgidm  14788  resttopon  14885  rest0  14893  psmetrel  15036  metrel  15056  xmetrel  15057  xmetf  15064  0met  15098  mopnrel  15155  setsmsbasg  15193  setsmsdsg  15194  qtopbasss  15235  reldvg  15393  dvexp  15425  dveflem  15440  elply2  15449  elplyd  15455  ply1term  15457  plymullem  15464  efcn  15482  sinhalfpilem  15505  sincosq1lem  15539  tangtx  15552  sincos4thpi  15554  pigt3  15558  dfrelog  15574  relogf1o  15575  log1  15580  loge  15581  relogiso  15587  2logb9irr  15685  2logb9irrap  15691  2sqlem9  15843  2sqlem10  15844  uhgr0e  15923  uhgr0  15926  umgrbien  15951  usgr0  16078  griedg0prc  16089  1loopgruspgr  16109  ex-fl  16257  bj-nndcALT  16290  bj-axempty  16424  bj-axempty2  16425  bdinex1  16430  bj-zfpair2  16441  bj-uniex2  16447  bj-indint  16462  bj-omind  16465  bj-omex  16473  bj-omelon  16492  pw1ndom3  16525  0nninf  16542  dceqnconst  16600  dcapnconst  16601