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  692  stabnot  834  mpbir2an  944  mpbir3an  1181  tru  1368  dcfromnotnotr  1458  dcfromcon  1459  dcfrompeirce  1460  mpgbir  1467  nfxfr  1488  19.8a  1604  sbt  1798  dveeq2  1829  dveeq2or  1830  sbequilem  1852  cbvex2  1937  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  nfeuv  2063  moaneu  2121  moanmo  2122  eqeltri  2269  nfcxfr  2336  neir  2370  neirr  2376  eqnetri  2390  nesymir  2414  nelir  2465  mprgbir  2555  vex  2766  issetri  2772  moeq  2939  cdeqi  2974  ru  2988  eqsstri  3215  3sstr4i  3224  mosn  3658  rabrsndc  3690  tpid1  3733  tpid2  3735  tpid3  3738  pwv  3838  uni0  3866  eqbrtri  4054  tr0  4142  trv  4143  zfnuleu  4157  0ex  4160  inex1  4167  elpwi2  4191  0elpw  4197  axpow2  4209  axpow3  4210  vpwex  4212  zfpair2  4243  exss  4260  moop2  4284  pwundifss  4320  po0  4346  epse  4377  fr0  4386  0elon  4427  onm  4436  uniex2  4471  snnex  4483  ordtriexmidlem  4555  ordtriexmid  4557  ontr2exmid  4561  ordtri2or2exmidlem  4562  onsucsssucexmid  4563  onsucelsucexmidlem  4565  ruALT  4587  zfregfr  4610  dcextest  4617  zfinf2  4625  omex  4629  finds  4636  finds2  4637  ordom  4643  omsinds  4658  relsnop  4769  relxp  4772  rel0  4788  relopabiv  4789  relopabi  4791  eliunxp  4805  opeliunxp2  4806  dmi  4881  xpidtr  5060  cnvcnv  5122  dmsn0  5137  cnvsn0  5138  funmpt  5296  funmpt2  5297  funinsn  5307  isarep2  5345  f0  5448  f10  5538  f1o00  5539  f1oi  5542  f1osn  5544  brprcneu  5551  fvopab3ig  5635  opabex  5786  eufnfv  5793  mpofun  6024  reldmmpo  6034  ovid  6039  ovidig  6040  ovidi  6041  ovig  6044  ovi3  6060  oprabex  6185  oprabex3  6186  f1stres  6217  f2ndres  6218  opeliunxp2f  6296  tpos0  6332  issmo  6346  tfrlem6  6374  tfrlem8  6376  tfri1dALT  6409  tfrcl  6422  rdgfun  6431  frecfun  6453  frecfcllem  6462  0lt1o  6498  eqer  6624  ecopover  6692  ecopoverg  6695  th3qcor  6698  mapsnf1o3  6756  ssdomg  6837  ensn1  6855  xpcomf1o  6884  fiunsnnn  6942  finexdc  6963  exmidpw  6969  dcfi  7047  omct  7183  infnninf  7190  infnninfOLD  7191  pm54.43  7257  exmidonfinlem  7260  pw1on  7293  pw1dom2  7294  pw1ne1  7296  2oneel  7323  dmaddpi  7392  dmmulpi  7393  1lt2pi  7407  indpi  7409  1lt2nq  7473  genpelxp  7578  ltexprlempr  7675  recexprlempr  7699  cauappcvgprlemcl  7720  cauappcvgprlemladd  7725  caucvgprlemcl  7743  caucvgprprlemcl  7771  m1p1sr  7827  m1m1sr  7828  0lt1sr  7832  peano1nnnn  7919  ax1cn  7928  ax1re  7929  axaddf  7935  axmulf  7936  ax0lt1  7943  0lt1  8153  subaddrii  8315  ixi  8610  1ap0  8617  sup3exmid  8984  nn1suc  9009  neg1lt0  9098  4d2e2  9151  iap0  9214  un0mulcl  9283  pnf0xnn0  9319  3halfnz  9423  nummac  9501  uzf  9604  mnfltpnf  9860  ixxf  9973  ioof  10046  fzf  10087  fzp1disj  10155  fzp1nel  10179  fzo0  10244  frecfzennn  10518  frechashgf1o  10520  xnn0nnen  10529  fxnn0nninf  10531  seq3f1olemp  10607  sq0  10722  irec  10731  hash0  10888  prhash2ex  10901  climmo  11463  sum0  11553  fisumcom2  11603  prod0  11750  fprodcom2fi  11791  cos1bnd  11924  cos2bnd  11925  3dvds  12029  n2dvdsm1  12078  n2dvds3  12080  flodddiv4  12101  3lcm2e6woprm  12254  6lcm4e12  12255  2prm  12295  3lcm2e6  12328  pockthi  12527  modsubi  12588  unennn  12614  ssnnctlemct  12663  structcnvcnv  12694  strleun  12782  starvndxnbasendx  12819  starvndxnplusgndx  12820  starvndxnmulrndx  12821  scandxnbasendx  12831  scandxnplusgndx  12832  scandxnmulrndx  12833  vscandxnbasendx  12836  vscandxnplusgndx  12837  vscandxnmulrndx  12838  vscandxnscandx  12839  ipndxnbasendx  12849  ipndxnplusgndx  12850  ipndxnmulrndx  12851  slotsdifipndx  12852  tsetndxnplusgndx  12869  tsetndxnmulrndx  12870  tsetndxnstarvndx  12871  slotstnscsi  12872  plendxnplusgndx  12883  plendxnmulrndx  12884  plendxnscandx  12885  plendxnvscandx  12886  slotsdifplendx  12887  dsndxnplusgndx  12894  dsndxnmulrndx  12895  slotsdnscsi  12896  dsndxntsetndx  12897  slotsdifdsndx  12898  unifndxntsetndx  12904  slotsdifunifndx  12905  restid  12921  mgmidmo  13015  rrgmex  13817  lssmex  13911  lidlmex  14031  2idlmex  14057  fczpsrbag  14225  tgdom  14308  tgidm  14310  resttopon  14407  rest0  14415  psmetrel  14558  metrel  14578  xmetrel  14579  xmetf  14586  0met  14620  mopnrel  14677  setsmsbasg  14715  setsmsdsg  14716  qtopbasss  14757  reldvg  14915  dvexp  14947  dveflem  14962  elply2  14971  elplyd  14977  ply1term  14979  plymullem  14986  efcn  15004  sinhalfpilem  15027  sincosq1lem  15061  tangtx  15074  sincos4thpi  15076  pigt3  15080  dfrelog  15096  relogf1o  15097  log1  15102  loge  15103  relogiso  15109  2logb9irr  15207  2logb9irrap  15213  2sqlem9  15365  2sqlem10  15366  ex-fl  15371  bj-nndcALT  15404  bj-axempty  15539  bj-axempty2  15540  bdinex1  15545  bj-zfpair2  15556  bj-uniex2  15562  bj-indint  15577  bj-omind  15580  bj-omex  15588  bj-omelon  15607  0nninf  15648  dceqnconst  15704  dcapnconst  15705