Theorem mpbir 145

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 132	. 2 ⊢ (𝜓 → 𝜑)
4	1, 3	ax-mp 5	1 ⊢ 𝜑

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74ri  180  imnani  681  stabnot  819  mpbir2an  927  mpbir3an  1164  tru  1336  mpgbir  1430  nfxfr  1451  19.8a  1570  sbt  1758  dveeq2  1788  dveeq2or  1789  sbequilem  1811  cbvex2  1895  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  nfeuv  2018  moaneu  2076  moanmo  2077  eqeltri  2213  nfcxfr  2279  neir  2312  neirr  2318  eqnetri  2332  nesymir  2356  nelir  2407  mprgbir  2493  vex  2692  issetri  2698  moeq  2863  cdeqi  2898  ru  2912  eqsstri  3134  3sstr4i  3143  rgenm  3470  mosn  3567  rabrsndc  3599  tpid1  3642  tpid2  3644  tpid3  3647  pwv  3743  uni0  3771  eqbrtri  3957  tr0  4045  trv  4046  zfnuleu  4060  0ex  4063  inex1  4070  0elpw  4096  axpow2  4108  axpow3  4109  vpwex  4111  zfpair2  4140  exss  4157  moop2  4181  pwundifss  4215  po0  4241  epse  4272  fr0  4281  0elon  4322  onm  4331  uniex2  4366  snnex  4377  ordtriexmidlem  4443  ordtriexmid  4445  ontr2exmid  4448  ordtri2or2exmidlem  4449  onsucsssucexmid  4450  onsucelsucexmidlem  4452  ruALT  4474  zfregfr  4496  dcextest  4503  zfinf2  4511  omex  4515  finds  4522  finds2  4523  ordom  4528  omsinds  4543  relsnop  4653  relxp  4656  rel0  4672  relopabi  4673  eliunxp  4686  opeliunxp2  4687  dmi  4762  xpidtr  4937  cnvcnv  4999  dmsn0  5014  cnvsn0  5015  funmpt  5169  funmpt2  5170  funinsn  5180  isarep2  5218  f0  5321  f10  5409  f1o00  5410  f1oi  5413  f1osn  5415  brprcneu  5422  fvopab3ig  5503  opabex  5652  eufnfv  5656  mpofun  5881  reldmmpo  5890  ovid  5895  ovidig  5896  ovidi  5897  ovig  5900  ovi3  5915  oprabex  6034  oprabex3  6035  f1stres  6065  f2ndres  6066  opeliunxp2f  6143  tpos0  6179  issmo  6193  tfrlem6  6221  tfrlem8  6223  tfri1dALT  6256  tfrcl  6269  rdgfun  6278  frecfun  6300  frecfcllem  6309  0lt1o  6345  eqer  6469  ecopover  6535  ecopoverg  6538  th3qcor  6541  mapsnf1o3  6599  ssdomg  6680  ensn1  6698  xpcomf1o  6727  fiunsnnn  6783  finexdc  6804  exmidpw  6810  omct  7010  infnninf  7030  nnnninf  7031  pm54.43  7063  exmidonfinlem  7066  dmaddpi  7157  dmmulpi  7158  1lt2pi  7172  indpi  7174  1lt2nq  7238  genpelxp  7343  ltexprlempr  7440  recexprlempr  7464  cauappcvgprlemcl  7485  cauappcvgprlemladd  7490  caucvgprlemcl  7508  caucvgprprlemcl  7536  m1p1sr  7592  m1m1sr  7593  0lt1sr  7597  peano1nnnn  7684  ax1cn  7693  ax1re  7694  axaddf  7700  axmulf  7701  ax0lt1  7708  0lt1  7913  subaddrii  8075  ixi  8369  1ap0  8376  sup3exmid  8739  nn1suc  8763  neg1lt0  8852  4d2e2  8904  iap0  8967  un0mulcl  9035  pnf0xnn0  9071  3halfnz  9172  nummac  9250  uzf  9353  mnfltpnf  9601  ixxf  9711  ioof  9784  fzf  9825  fzp1disj  9891  fzp1nel  9915  fzo0  9976  frecfzennn  10230  frechashgf1o  10232  fxnn0nninf  10242  seq3f1olemp  10306  sq0  10414  irec  10423  hash0  10575  prhash2ex  10587  climmo  11099  sum0  11189  fisumcom2  11239  cos1bnd  11502  cos2bnd  11503  n2dvdsm1  11646  n2dvds3  11648  flodddiv4  11667  3lcm2e6woprm  11803  6lcm4e12  11804  2prm  11844  3lcm2e6  11874  unennn  11946  structcnvcnv  12014  strleun  12087  restid  12170  tgdom  12280  tgidm  12282  resttopon  12379  rest0  12387  psmetrel  12530  metrel  12550  xmetrel  12551  xmetf  12558  0met  12592  mopnrel  12649  setsmsbasg  12687  setsmsdsg  12688  qtopbasss  12729  reldvg  12856  dvexp  12883  dveflem  12895  efcn  12897  sinhalfpilem  12920  sincosq1lem  12954  tangtx  12967  sincos4thpi  12969  pigt3  12973  dfrelog  12989  relogf1o  12990  log1  12995  loge  12996  relogiso  13002  2logb9irr  13096  2logb9irrap  13102  ex-fl  13108  bj-nndcALT  13134  bj-axempty  13262  bj-axempty2  13263  bdinex1  13268  bj-zfpair2  13279  bj-uniex2  13285  bj-indint  13300  bj-omind  13303  bj-omex  13311  bj-omelon  13330  pw1dom2  13361  0nninf  13372  dceqnconst  13423