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  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  11860  sum0  11951  fisumcom2  12001  prod0  12148  fprodcom2fi  12189  cos1bnd  12322  cos2bnd  12323  3dvds  12427  n2dvdsm1  12476  n2dvds3  12478  flodddiv4  12499  3lcm2e6woprm  12660  6lcm4e12  12661  2prm  12701  3lcm2e6  12734  pockthi  12933  modsubi  12994  unennn  13020  ssnnctlemct  13069  structcnvcnv  13100  strleun  13189  starvndxnbasendx  13227  starvndxnplusgndx  13228  starvndxnmulrndx  13229  scandxnbasendx  13239  scandxnplusgndx  13240  scandxnmulrndx  13241  vscandxnbasendx  13244  vscandxnplusgndx  13245  vscandxnmulrndx  13246  vscandxnscandx  13247  ipndxnbasendx  13257  ipndxnplusgndx  13258  ipndxnmulrndx  13259  slotsdifipndx  13260  tsetndxnplusgndx  13277  tsetndxnmulrndx  13278  tsetndxnstarvndx  13279  slotstnscsi  13280  plendxnplusgndx  13291  plendxnmulrndx  13292  plendxnscandx  13293  plendxnvscandx  13294  slotsdifplendx  13295  basendxnocndx  13298  plendxnocndx  13299  dsndxnplusgndx  13306  dsndxnmulrndx  13307  slotsdnscsi  13308  dsndxntsetndx  13309  slotsdifdsndx  13310  unifndxntsetndx  13316  slotsdifunifndx  13317  restid  13335  prdsval  13358  mgmidmo  13457  reldvdsr  14108  rrgmex  14278  lssmex  14372  lidlmex  14492  2idlmex  14518  fczpsrbag  14688  tgdom  14799  tgidm  14801  resttopon  14898  rest0  14906  psmetrel  15049  metrel  15069  xmetrel  15070  xmetf  15077  0met  15111  mopnrel  15168  setsmsbasg  15206  setsmsdsg  15207  qtopbasss  15248  reldvg  15406  dvexp  15438  dveflem  15453  elply2  15462  elplyd  15468  ply1term  15470  plymullem  15477  efcn  15495  sinhalfpilem  15518  sincosq1lem  15552  tangtx  15565  sincos4thpi  15567  pigt3  15571  dfrelog  15587  relogf1o  15588  log1  15593  loge  15594  relogiso  15600  2logb9irr  15698  2logb9irrap  15704  2sqlem9  15856  2sqlem10  15857  uhgr0e  15936  uhgr0  15939  umgrbien  15964  usgr0  16093  griedg0prc  16104  1loopgruspgr  16157  ex-fl  16338  bj-nndcALT  16375  bj-axempty  16509  bj-axempty2  16510  bdinex1  16515  bj-zfpair2  16526  bj-uniex2  16532  bj-indint  16547  bj-omind  16550  bj-omex  16558  bj-omelon  16577  pw1ndom3  16610  0nninf  16627  dceqnconst  16685  dcapnconst  16686  gfsum0  16703