Theorem mpbir 146

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbir.min	⊢ 𝜓
mpbir.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbir	⊢ 𝜑

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 ⊢ 𝜓
2		mpbir.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpri 133	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

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  1833  dveeq2  1864  dveeq2or  1865  sbequilem  1887  cbvex2  1972  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  nfeuv  2098  moaneu  2157  moanmo  2158  eqeltri  2305  nfcxfr  2381  neir  2415  neirr  2421  eqnetri  2435  nesymir  2459  nelir  2510  mprgbir  2600  vex  2815  issetri  2822  moeq  2991  cdeqi  3026  ru  3040  eqsstri  3269  3sstr4i  3278  mosn  3724  rabrsndc  3758  tpid1  3802  tpid2  3804  tpid3  3807  pwv  3912  uni0  3940  eqbrtri  4129  tr0  4218  trv  4219  zfnuleu  4233  0ex  4236  inex1  4243  elpwi2  4269  0elpw  4276  axpow2  4288  axpow3  4289  vpwex  4291  zfpair2  4322  exss  4342  opwo0id  4364  moop2  4367  pwundifss  4405  po0  4431  epse  4462  fr0  4471  0elon  4512  onm  4521  uniex2  4556  snnex  4568  ordtriexmidlem  4640  ordtriexmid  4642  ontr2exmid  4646  ordtri2or2exmidlem  4647  onsucsssucexmid  4648  onsucelsucexmidlem  4650  ruALT  4672  zfregfr  4695  dcextest  4702  zfinf2  4710  omex  4714  finds  4721  finds2  4722  ordom  4728  omsinds  4743  relsnop  4855  relxp  4858  rel0  4876  relopabiv  4877  relopabi  4879  eliunxp  4893  opeliunxp2  4894  dmi  4970  xpidtr  5152  cnvcnv  5214  dmsn0  5229  cnvsn0  5230  funmpt  5389  funmpt2  5390  funinsn  5404  isarep2  5442  f0  5557  f10  5648  f10d  5649  f1o00  5650  f1oi  5653  f1osn  5655  brprcneu  5662  fvopab3ig  5750  opabex  5909  eufnfv  5916  mpofun  6154  reldmmpo  6164  ovid  6169  ovidig  6170  ovidi  6171  ovig  6174  ovi3  6190  relmptopab  6255  oprabex  6320  oprabex3  6321  f1stres  6352  f2ndres  6353  opeliunxp2f  6468  tpos0  6504  issmo  6518  tfrlem6  6546  tfrlem8  6548  tfri1dALT  6581  tfrcl  6594  rdgfun  6603  frecfun  6625  frecfcllem  6634  0lt1o  6672  eqer  6798  ecopover  6866  ecopoverg  6869  th3qcor  6872  mapsnf1o3  6931  ssdomg  7017  ensn1  7035  xpcomf1o  7075  fiunsnnn  7137  finexdc  7159  elssdc  7161  exmidpw  7167  fissfi  7215  dcfi  7267  omct  7407  infnninf  7414  infnninfOLD  7415  pm54.43  7486  exmidonfinlem  7495  pw1on  7535  pw1dom2  7536  pw1ne1  7538  2oneel  7566  dmaddpi  7636  dmmulpi  7637  1lt2pi  7651  indpi  7653  1lt2nq  7717  genpelxp  7822  ltexprlempr  7919  recexprlempr  7943  cauappcvgprlemcl  7964  cauappcvgprlemladd  7969  caucvgprlemcl  7987  caucvgprprlemcl  8015  m1p1sr  8071  m1m1sr  8072  0lt1sr  8076  peano1nnnn  8163  ax1cn  8172  ax1re  8173  axaddf  8179  axmulf  8180  ax0lt1  8187  0lt1  8396  subaddrii  8558  ixi  8853  1ap0  8860  sup3exmid  9227  nn1suc  9252  neg1lt0  9341  4d2e2  9394  iap0  9457  un0mulcl  9526  pnf0xnn0  9566  3halfnz  9671  nummac  9749  uzf  9852  mnfltpnf  10114  ixxf  10227  ioof  10300  fzf  10342  fzp1disj  10410  fzp1nel  10434  fzo0  10500  frecfzennn  10784  frechashgf1o  10786  xnn0nnen  10795  fxnn0nninf  10797  seq3f1olemp  10873  sq0  10988  irec  10997  hash0  11154  prhash2ex  11169  hashfibclem  11199  climmo  11976  sum0  12067  fisumcom2  12117  prod0  12264  fprodcom2fi  12305  cos1bnd  12438  cos2bnd  12439  3dvds  12543  n2dvdsm1  12592  n2dvds3  12594  flodddiv4  12615  3lcm2e6woprm  12776  6lcm4e12  12777  2prm  12817  3lcm2e6  12850  pockthi  13049  modsubi  13110  unennn  13137  ssnnctlemct  13186  structcnvcnv  13217  strleun  13306  starvndxnbasendx  13344  starvndxnplusgndx  13345  starvndxnmulrndx  13346  scandxnbasendx  13356  scandxnplusgndx  13357  scandxnmulrndx  13358  vscandxnbasendx  13361  vscandxnplusgndx  13362  vscandxnmulrndx  13363  vscandxnscandx  13364  ipndxnbasendx  13374  ipndxnplusgndx  13375  ipndxnmulrndx  13376  slotsdifipndx  13377  tsetndxnplusgndx  13394  tsetndxnmulrndx  13395  tsetndxnstarvndx  13396  slotstnscsi  13397  plendxnplusgndx  13408  plendxnmulrndx  13409  plendxnscandx  13410  plendxnvscandx  13411  slotsdifplendx  13412  basendxnocndx  13415  plendxnocndx  13416  dsndxnplusgndx  13423  dsndxnmulrndx  13424  slotsdnscsi  13425  dsndxntsetndx  13426  slotsdifdsndx  13427  unifndxntsetndx  13433  slotsdifunifndx  13434  restid  13452  prdsval  13475  mgmidmo  13574  reldvdsr  14225  rrgmex  14395  lssmex  14490  lidlmex  14610  2idlmex  14636  fczpsrbag  14807  tgdom  14924  tgidm  14926  resttopon  15023  rest0  15031  psmetrel  15174  metrel  15194  xmetrel  15195  xmetf  15202  0met  15236  mopnrel  15293  setsmsbasg  15331  setsmsdsg  15332  qtopbasss  15373  reldvg  15531  dvexp  15563  dveflem  15578  elply2  15587  elplyd  15593  ply1term  15595  plymullem  15602  efcn  15620  sinhalfpilem  15643  sincosq1lem  15677  tangtx  15690  sincos4thpi  15692  pigt3  15696  dfrelog  15712  relogf1o  15713  log1  15718  loge  15719  relogiso  15725  2logb9irr  15823  2logb9irrap  15829  2sqlem9  15984  2sqlem10  15985  uhgr0e  16064  uhgr0  16067  umgrbien  16092  usgr0  16221  griedg0prc  16232  1loopgruspgr  16285  konigsbergumgr  16469  konigsberglem1  16470  ex-fl  16480  bj-nndcALT  16517  bj-axempty  16650  bj-axempty2  16651  bdinex1  16656  bj-zfpair2  16667  bj-uniex2  16673  bj-indint  16688  bj-omind  16691  bj-omex  16699  bj-omelon  16718  pw1ndom3  16751  0nninf  16769  dceqnconst  16832  dcapnconst  16833  gfsum0  16850