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  mpgbir  1464  nfxfr  1485  19.8a  1601  sbt  1795  dveeq2  1826  dveeq2or  1827  sbequilem  1849  cbvex2  1934  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  nfeuv  2060  moaneu  2118  moanmo  2119  eqeltri  2266  nfcxfr  2333  neir  2367  neirr  2373  eqnetri  2387  nesymir  2411  nelir  2462  mprgbir  2552  vex  2763  issetri  2769  moeq  2936  cdeqi  2971  ru  2985  eqsstri  3212  3sstr4i  3221  mosn  3655  rabrsndc  3687  tpid1  3730  tpid2  3732  tpid3  3735  pwv  3835  uni0  3863  eqbrtri  4051  tr0  4139  trv  4140  zfnuleu  4154  0ex  4157  inex1  4164  elpwi2  4188  0elpw  4194  axpow2  4206  axpow3  4207  vpwex  4209  zfpair2  4240  exss  4257  moop2  4281  pwundifss  4317  po0  4343  epse  4374  fr0  4383  0elon  4424  onm  4433  uniex2  4468  snnex  4480  ordtriexmidlem  4552  ordtriexmid  4554  ontr2exmid  4558  ordtri2or2exmidlem  4559  onsucsssucexmid  4560  onsucelsucexmidlem  4562  ruALT  4584  zfregfr  4607  dcextest  4614  zfinf2  4622  omex  4626  finds  4633  finds2  4634  ordom  4640  omsinds  4655  relsnop  4766  relxp  4769  rel0  4785  relopabiv  4786  relopabi  4788  eliunxp  4802  opeliunxp2  4803  dmi  4878  xpidtr  5057  cnvcnv  5119  dmsn0  5134  cnvsn0  5135  funmpt  5293  funmpt2  5294  funinsn  5304  isarep2  5342  f0  5445  f10  5535  f1o00  5536  f1oi  5539  f1osn  5541  brprcneu  5548  fvopab3ig  5632  opabex  5783  eufnfv  5790  mpofun  6021  reldmmpo  6031  ovid  6036  ovidig  6037  ovidi  6038  ovig  6041  ovi3  6057  oprabex  6182  oprabex3  6183  f1stres  6214  f2ndres  6215  opeliunxp2f  6293  tpos0  6329  issmo  6343  tfrlem6  6371  tfrlem8  6373  tfri1dALT  6406  tfrcl  6419  rdgfun  6428  frecfun  6450  frecfcllem  6459  0lt1o  6495  eqer  6621  ecopover  6689  ecopoverg  6692  th3qcor  6695  mapsnf1o3  6753  ssdomg  6834  ensn1  6852  xpcomf1o  6881  fiunsnnn  6939  finexdc  6960  exmidpw  6966  dcfi  7042  omct  7178  infnninf  7185  infnninfOLD  7186  pm54.43  7252  exmidonfinlem  7255  pw1on  7288  pw1dom2  7289  pw1ne1  7291  2oneel  7318  dmaddpi  7387  dmmulpi  7388  1lt2pi  7402  indpi  7404  1lt2nq  7468  genpelxp  7573  ltexprlempr  7670  recexprlempr  7694  cauappcvgprlemcl  7715  cauappcvgprlemladd  7720  caucvgprlemcl  7738  caucvgprprlemcl  7766  m1p1sr  7822  m1m1sr  7823  0lt1sr  7827  peano1nnnn  7914  ax1cn  7923  ax1re  7924  axaddf  7930  axmulf  7931  ax0lt1  7938  0lt1  8148  subaddrii  8310  ixi  8604  1ap0  8611  sup3exmid  8978  nn1suc  9003  neg1lt0  9092  4d2e2  9145  iap0  9208  un0mulcl  9277  pnf0xnn0  9313  3halfnz  9417  nummac  9495  uzf  9598  mnfltpnf  9854  ixxf  9967  ioof  10040  fzf  10081  fzp1disj  10149  fzp1nel  10173  fzo0  10238  frecfzennn  10500  frechashgf1o  10502  xnn0nnen  10511  fxnn0nninf  10513  seq3f1olemp  10589  sq0  10704  irec  10713  hash0  10870  prhash2ex  10883  climmo  11444  sum0  11534  fisumcom2  11584  prod0  11731  fprodcom2fi  11772  cos1bnd  11905  cos2bnd  11906  n2dvdsm1  12057  n2dvds3  12059  flodddiv4  12078  3lcm2e6woprm  12227  6lcm4e12  12228  2prm  12268  3lcm2e6  12301  pockthi  12499  unennn  12557  ssnnctlemct  12606  structcnvcnv  12637  strleun  12725  starvndxnbasendx  12762  starvndxnplusgndx  12763  starvndxnmulrndx  12764  scandxnbasendx  12774  scandxnplusgndx  12775  scandxnmulrndx  12776  vscandxnbasendx  12779  vscandxnplusgndx  12780  vscandxnmulrndx  12781  vscandxnscandx  12782  ipndxnbasendx  12792  ipndxnplusgndx  12793  ipndxnmulrndx  12794  slotsdifipndx  12795  tsetndxnplusgndx  12812  tsetndxnmulrndx  12813  tsetndxnstarvndx  12814  slotstnscsi  12815  plendxnplusgndx  12826  plendxnmulrndx  12827  plendxnscandx  12828  plendxnvscandx  12829  slotsdifplendx  12830  dsndxnplusgndx  12837  dsndxnmulrndx  12838  slotsdnscsi  12839  dsndxntsetndx  12840  slotsdifdsndx  12841  unifndxntsetndx  12847  slotsdifunifndx  12848  restid  12864  mgmidmo  12958  rrgmex  13760  lssmex  13854  lidlmex  13974  2idlmex  14000  fczpsrbag  14168  tgdom  14251  tgidm  14253  resttopon  14350  rest0  14358  psmetrel  14501  metrel  14521  xmetrel  14522  xmetf  14529  0met  14563  mopnrel  14620  setsmsbasg  14658  setsmsdsg  14659  qtopbasss  14700  reldvg  14858  dvexp  14890  dveflem  14905  elply2  14914  elplyd  14920  ply1term  14922  plymullem  14929  efcn  14944  sinhalfpilem  14967  sincosq1lem  15001  tangtx  15014  sincos4thpi  15016  pigt3  15020  dfrelog  15036  relogf1o  15037  log1  15042  loge  15043  relogiso  15049  2logb9irr  15144  2logb9irrap  15150  2sqlem9  15281  2sqlem10  15282  ex-fl  15287  bj-nndcALT  15320  bj-axempty  15455  bj-axempty2  15456  bdinex1  15461  bj-zfpair2  15472  bj-uniex2  15478  bj-indint  15493  bj-omind  15496  bj-omex  15504  bj-omelon  15523  0nninf  15564  dceqnconst  15620  dcapnconst  15621