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  5878  eufnfv  5885  mpofun  6123  reldmmpo  6133  ovid  6138  ovidig  6139  ovidi  6140  ovig  6143  ovi3  6159  relmptopab  6224  oprabex  6290  oprabex3  6291  f1stres  6322  f2ndres  6323  opeliunxp2f  6404  tpos0  6440  issmo  6454  tfrlem6  6482  tfrlem8  6484  tfri1dALT  6517  tfrcl  6530  rdgfun  6539  frecfun  6561  frecfcllem  6570  0lt1o  6608  eqer  6734  ecopover  6802  ecopoverg  6805  th3qcor  6808  mapsnf1o3  6866  ssdomg  6952  ensn1  6970  xpcomf1o  7009  fiunsnnn  7070  finexdc  7092  elssdc  7094  exmidpw  7100  dcfi  7180  omct  7316  infnninf  7323  infnninfOLD  7324  pm54.43  7395  exmidonfinlem  7404  pw1on  7444  pw1dom2  7445  pw1ne1  7447  2oneel  7475  dmaddpi  7545  dmmulpi  7546  1lt2pi  7560  indpi  7562  1lt2nq  7626  genpelxp  7731  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  cauappcvgprlemladd  7878  caucvgprlemcl  7896  caucvgprprlemcl  7924  m1p1sr  7980  m1m1sr  7981  0lt1sr  7985  peano1nnnn  8072  ax1cn  8081  ax1re  8082  axaddf  8088  axmulf  8089  ax0lt1  8096  0lt1  8306  subaddrii  8468  ixi  8763  1ap0  8770  sup3exmid  9137  nn1suc  9162  neg1lt0  9251  4d2e2  9304  iap0  9367  un0mulcl  9436  pnf0xnn0  9472  3halfnz  9577  nummac  9655  uzf  9758  mnfltpnf  10020  ixxf  10133  ioof  10206  fzf  10247  fzp1disj  10315  fzp1nel  10339  fzo0  10405  frecfzennn  10689  frechashgf1o  10691  xnn0nnen  10700  fxnn0nninf  10702  seq3f1olemp  10778  sq0  10893  irec  10902  hash0  11059  prhash2ex  11074  climmo  11876  sum0  11967  fisumcom2  12017  prod0  12164  fprodcom2fi  12205  cos1bnd  12338  cos2bnd  12339  3dvds  12443  n2dvdsm1  12492  n2dvds3  12494  flodddiv4  12515  3lcm2e6woprm  12676  6lcm4e12  12677  2prm  12717  3lcm2e6  12750  pockthi  12949  modsubi  13010  unennn  13036  ssnnctlemct  13085  structcnvcnv  13116  strleun  13205  starvndxnbasendx  13243  starvndxnplusgndx  13244  starvndxnmulrndx  13245  scandxnbasendx  13255  scandxnplusgndx  13256  scandxnmulrndx  13257  vscandxnbasendx  13260  vscandxnplusgndx  13261  vscandxnmulrndx  13262  vscandxnscandx  13263  ipndxnbasendx  13273  ipndxnplusgndx  13274  ipndxnmulrndx  13275  slotsdifipndx  13276  tsetndxnplusgndx  13293  tsetndxnmulrndx  13294  tsetndxnstarvndx  13295  slotstnscsi  13296  plendxnplusgndx  13307  plendxnmulrndx  13308  plendxnscandx  13309  plendxnvscandx  13310  slotsdifplendx  13311  basendxnocndx  13314  plendxnocndx  13315  dsndxnplusgndx  13322  dsndxnmulrndx  13323  slotsdnscsi  13324  dsndxntsetndx  13325  slotsdifdsndx  13326  unifndxntsetndx  13332  slotsdifunifndx  13333  restid  13351  prdsval  13374  mgmidmo  13473  reldvdsr  14124  rrgmex  14294  lssmex  14388  lidlmex  14508  2idlmex  14534  fczpsrbag  14704  tgdom  14815  tgidm  14817  resttopon  14914  rest0  14922  psmetrel  15065  metrel  15085  xmetrel  15086  xmetf  15093  0met  15127  mopnrel  15184  setsmsbasg  15222  setsmsdsg  15223  qtopbasss  15264  reldvg  15422  dvexp  15454  dveflem  15469  elply2  15478  elplyd  15484  ply1term  15486  plymullem  15493  efcn  15511  sinhalfpilem  15534  sincosq1lem  15568  tangtx  15581  sincos4thpi  15583  pigt3  15587  dfrelog  15603  relogf1o  15604  log1  15609  loge  15610  relogiso  15616  2logb9irr  15714  2logb9irrap  15720  2sqlem9  15872  2sqlem10  15873  uhgr0e  15952  uhgr0  15955  umgrbien  15980  usgr0  16109  griedg0prc  16120  1loopgruspgr  16173  konigsbergumgr  16357  konigsberglem1  16358  ex-fl  16368  bj-nndcALT  16405  bj-axempty  16539  bj-axempty2  16540  bdinex1  16545  bj-zfpair2  16556  bj-uniex2  16562  bj-indint  16577  bj-omind  16580  bj-omex  16588  bj-omelon  16607  pw1ndom3  16640  0nninf  16657  dceqnconst  16716  dcapnconst  16717  gfsum0  16734