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  1974  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  nfeuv  2100  moaneu  2159  moanmo  2160  eqeltri  2307  nfcxfr  2383  neir  2417  neirr  2423  eqnetri  2437  nesymir  2461  nelir  2512  mprgbir  2602  vex  2818  issetri  2825  moeq  2995  cdeqi  3030  ru  3044  eqsstri  3274  3sstr4i  3283  mosn  3730  rabrsndc  3764  tpid1  3808  tpid2  3810  tpid3  3813  pwv  3918  uni0  3946  eqbrtri  4135  tr0  4224  trv  4225  zfnuleu  4239  0ex  4242  inex1  4249  elpwi2  4275  0elpw  4282  axpow2  4294  axpow3  4295  vpwex  4297  zfpair2  4328  exss  4348  opwo0id  4370  moop2  4373  pwundifss  4411  po0  4437  epse  4468  fr0  4477  0elon  4518  onm  4527  uniex2  4562  snnex  4574  ordtriexmidlem  4646  ordtriexmid  4648  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucsssucexmid  4654  onsucelsucexmidlem  4656  ruALT  4678  zfregfr  4701  dcextest  4708  zfinf2  4716  omex  4720  finds  4727  finds2  4728  ordom  4734  omsinds  4749  relsnop  4861  relxp  4864  rel0  4882  relopabiv  4883  relopabi  4885  eliunxp  4899  opeliunxp2  4900  dmi  4976  xpidtr  5158  cnvcnv  5220  dmsn0  5235  cnvsn0  5236  funmpt  5395  funmpt2  5396  funinsn  5410  isarep2  5448  f0  5563  f10  5654  f10d  5655  f1o00  5656  f1oi  5659  f1osn  5661  brprcneu  5668  fvopab3ig  5756  opabex  5915  eufnfv  5922  rinvf1o  6008  mpofun  6163  reldmmpo  6173  ovid  6178  ovidig  6179  ovidi  6180  ovig  6183  ovi3  6199  relmptopab  6264  oprabex  6334  oprabex3  6335  f1stres  6366  f2ndres  6367  opeliunxp2f  6482  tpos0  6518  issmo  6532  tfrlem6  6560  tfrlem8  6562  tfri1dALT  6595  tfrcl  6608  rdgfun  6617  frecfun  6639  frecfcllem  6648  0lt1o  6686  eqer  6812  ecopover  6880  ecopoverg  6883  th3qcor  6886  mapsnf1o3  6945  ssdomg  7031  ensn1  7049  xpcomf1o  7089  fiunsnnn  7151  finexdc  7173  elssdc  7175  exmidpw  7181  fissfi  7229  dcfi  7281  omct  7421  infnninf  7428  infnninfOLD  7429  pm54.43  7500  exmidonfinlem  7509  pw1on  7549  pw1dom2  7550  pw1ne1  7552  2oneel  7586  dmaddpi  7656  dmmulpi  7657  1lt2pi  7671  indpi  7673  1lt2nq  7737  genpelxp  7842  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  cauappcvgprlemladd  7989  caucvgprlemcl  8007  caucvgprprlemcl  8035  m1p1sr  8091  m1m1sr  8092  0lt1sr  8096  peano1nnnn  8183  ax1cn  8192  ax1re  8193  axaddf  8199  axmulf  8200  ax0lt1  8207  0lt1  8417  subaddrii  8579  ixi  8875  1ap0  8882  sup3exmid  9251  nn1suc  9276  neg1lt0  9365  4d2e2  9418  iap0  9481  un0mulcl  9550  pnf0xnn0  9590  3halfnz  9696  nummac  9774  uzf  9877  mnfltpnf  10140  ixxf  10253  ioof  10326  fzf  10368  fzp1disj  10439  fzp1nel  10463  fzo0  10529  frecfzennn  10815  frechashgf1o  10817  xnn0nnen  10826  fxnn0nninf  10828  seq3f1olemp  10904  sq0  11019  irec  11028  hash0  11187  prhash2ex  11202  hashfibclem  11234  climmo  12011  sum0  12102  fisumcom2  12152  prod0  12299  fprodcom2fi  12340  cos1bnd  12473  cos2bnd  12474  3dvds  12578  n2dvdsm1  12627  n2dvds3  12629  flodddiv4  12650  3lcm2e6woprm  12811  6lcm4e12  12812  2prm  12852  3lcm2e6  12885  pockthi  13084  modsubi  13145  ballotfilemcdc  13170  ballotfilem2  13175  ballotfilemic  13197  ballotfilem7  13226  ballotfilemth  13228  unennn  13235  ssnnctlemct  13284  structcnvcnv  13315  strleun  13404  starvndxnbasendx  13442  starvndxnplusgndx  13443  starvndxnmulrndx  13444  scandxnbasendx  13454  scandxnplusgndx  13455  scandxnmulrndx  13456  vscandxnbasendx  13459  vscandxnplusgndx  13460  vscandxnmulrndx  13461  vscandxnscandx  13462  ipndxnbasendx  13472  ipndxnplusgndx  13473  ipndxnmulrndx  13474  slotsdifipndx  13475  tsetndxnplusgndx  13492  tsetndxnmulrndx  13493  tsetndxnstarvndx  13494  slotstnscsi  13495  plendxnplusgndx  13506  plendxnmulrndx  13507  plendxnscandx  13508  plendxnvscandx  13509  slotsdifplendx  13510  basendxnocndx  13513  plendxnocndx  13514  dsndxnplusgndx  13521  dsndxnmulrndx  13522  slotsdnscsi  13523  dsndxntsetndx  13524  slotsdifdsndx  13525  unifndxntsetndx  13531  slotsdifunifndx  13532  restid  13550  mgmidmo  13638  gfsum0  14107  prdsval  14118  opprringb  14327  reldvdsr  14339  rrgmex  14510  lssmex  14632  lidlmex  14752  2idlmex  14778  fczpsrbag  14949  tgdom  15066  tgidm  15068  resttopon  15165  rest0  15173  psmetrel  15316  metrel  15336  xmetrel  15337  xmetf  15344  0met  15378  mopnrel  15435  setsmsbasg  15473  setsmsdsg  15474  qtopbasss  15515  reldvg  15673  dvexp  15705  dveflem  15720  elply2  15729  elplyd  15735  ply1term  15737  plymullem  15744  efcn  15762  sinhalfpilem  15785  sincosq1lem  15819  tangtx  15832  sincos4thpi  15834  pigt3  15838  dfrelog  15854  relogf1o  15855  log1  15860  loge  15861  relogiso  15867  2logb9irr  15965  2logb9irrap  15971  2sqlem9  16126  2sqlem10  16127  uhgr0e  16206  uhgr0  16209  umgrbien  16234  usgr0  16363  griedg0prc  16374  1loopgruspgr  16427  konigsbergumgr  16611  konigsberglem1  16612  ex-fl  16622  bj-nndcALT  16669  bj-axempty  16802  bj-axempty2  16803  bdinex1  16808  bj-zfpair2  16819  bj-uniex2  16825  bj-indint  16840  bj-omind  16843  bj-omex  16851  bj-omelon  16870  pw1ndom3  16903  0nninf  16921  dceqnconst  16985  dcapnconst  16986