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  695  stabnot  838  mpbir2an  948  mpbir3an  1203  tru  1399  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpgbir  1499  nfxfr  1520  19.8a  1636  sbt  1830  dveeq2  1861  dveeq2or  1862  sbequilem  1884  cbvex2  1969  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  nfeuv  2095  moaneu  2154  moanmo  2155  eqeltri  2302  nfcxfr  2369  neir  2403  neirr  2409  eqnetri  2423  nesymir  2447  nelir  2498  mprgbir  2588  vex  2803  issetri  2810  moeq  2979  cdeqi  3014  ru  3028  eqsstri  3257  3sstr4i  3266  mosn  3703  rabrsndc  3737  tpid1  3781  tpid2  3783  tpid3  3786  pwv  3890  uni0  3918  eqbrtri  4107  tr0  4196  trv  4197  zfnuleu  4211  0ex  4214  inex1  4221  elpwi2  4246  0elpw  4252  axpow2  4264  axpow3  4265  vpwex  4267  zfpair2  4298  exss  4317  opwo0id  4339  moop2  4342  pwundifss  4380  po0  4406  epse  4437  fr0  4446  0elon  4487  onm  4496  uniex2  4531  snnex  4543  ordtriexmidlem  4615  ordtriexmid  4617  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucsssucexmid  4623  onsucelsucexmidlem  4625  ruALT  4647  zfregfr  4670  dcextest  4677  zfinf2  4685  omex  4689  finds  4696  finds2  4697  ordom  4703  omsinds  4718  relsnop  4830  relxp  4833  rel0  4850  relopabiv  4851  relopabi  4853  eliunxp  4867  opeliunxp2  4868  dmi  4944  xpidtr  5125  cnvcnv  5187  dmsn0  5202  cnvsn0  5203  funmpt  5362  funmpt2  5363  funinsn  5376  isarep2  5414  f0  5524  f10  5614  f10d  5615  f1o00  5616  f1oi  5619  f1osn  5621  brprcneu  5628  fvopab3ig  5716  opabex  5873  eufnfv  5880  mpofun  6118  reldmmpo  6128  ovid  6133  ovidig  6134  ovidi  6135  ovig  6138  ovi3  6154  relmptopab  6219  oprabex  6285  oprabex3  6286  f1stres  6317  f2ndres  6318  opeliunxp2f  6399  tpos0  6435  issmo  6449  tfrlem6  6477  tfrlem8  6479  tfri1dALT  6512  tfrcl  6525  rdgfun  6534  frecfun  6556  frecfcllem  6565  0lt1o  6603  eqer  6729  ecopover  6797  ecopoverg  6800  th3qcor  6803  mapsnf1o3  6861  ssdomg  6947  ensn1  6965  xpcomf1o  7004  fiunsnnn  7065  finexdc  7087  elssdc  7089  exmidpw  7095  dcfi  7174  omct  7310  infnninf  7317  infnninfOLD  7318  pm54.43  7389  exmidonfinlem  7397  pw1on  7437  pw1dom2  7438  pw1ne1  7440  2oneel  7468  dmaddpi  7538  dmmulpi  7539  1lt2pi  7553  indpi  7555  1lt2nq  7619  genpelxp  7724  ltexprlempr  7821  recexprlempr  7845  cauappcvgprlemcl  7866  cauappcvgprlemladd  7871  caucvgprlemcl  7889  caucvgprprlemcl  7917  m1p1sr  7973  m1m1sr  7974  0lt1sr  7978  peano1nnnn  8065  ax1cn  8074  ax1re  8075  axaddf  8081  axmulf  8082  ax0lt1  8089  0lt1  8299  subaddrii  8461  ixi  8756  1ap0  8763  sup3exmid  9130  nn1suc  9155  neg1lt0  9244  4d2e2  9297  iap0  9360  un0mulcl  9429  pnf0xnn0  9465  3halfnz  9570  nummac  9648  uzf  9751  mnfltpnf  10013  ixxf  10126  ioof  10199  fzf  10240  fzp1disj  10308  fzp1nel  10332  fzo0  10398  frecfzennn  10681  frechashgf1o  10683  xnn0nnen  10692  fxnn0nninf  10694  seq3f1olemp  10770  sq0  10885  irec  10894  hash0  11051  prhash2ex  11066  climmo  11852  sum0  11942  fisumcom2  11992  prod0  12139  fprodcom2fi  12180  cos1bnd  12313  cos2bnd  12314  3dvds  12418  n2dvdsm1  12467  n2dvds3  12469  flodddiv4  12490  3lcm2e6woprm  12651  6lcm4e12  12652  2prm  12692  3lcm2e6  12725  pockthi  12924  modsubi  12985  unennn  13011  ssnnctlemct  13060  structcnvcnv  13091  strleun  13180  starvndxnbasendx  13218  starvndxnplusgndx  13219  starvndxnmulrndx  13220  scandxnbasendx  13230  scandxnplusgndx  13231  scandxnmulrndx  13232  vscandxnbasendx  13235  vscandxnplusgndx  13236  vscandxnmulrndx  13237  vscandxnscandx  13238  ipndxnbasendx  13248  ipndxnplusgndx  13249  ipndxnmulrndx  13250  slotsdifipndx  13251  tsetndxnplusgndx  13268  tsetndxnmulrndx  13269  tsetndxnstarvndx  13270  slotstnscsi  13271  plendxnplusgndx  13282  plendxnmulrndx  13283  plendxnscandx  13284  plendxnvscandx  13285  slotsdifplendx  13286  basendxnocndx  13289  plendxnocndx  13290  dsndxnplusgndx  13297  dsndxnmulrndx  13298  slotsdnscsi  13299  dsndxntsetndx  13300  slotsdifdsndx  13301  unifndxntsetndx  13307  slotsdifunifndx  13308  restid  13326  prdsval  13349  mgmidmo  13448  reldvdsr  14098  rrgmex  14268  lssmex  14362  lidlmex  14482  2idlmex  14508  fczpsrbag  14678  tgdom  14789  tgidm  14791  resttopon  14888  rest0  14896  psmetrel  15039  metrel  15059  xmetrel  15060  xmetf  15067  0met  15101  mopnrel  15158  setsmsbasg  15196  setsmsdsg  15197  qtopbasss  15238  reldvg  15396  dvexp  15428  dveflem  15443  elply2  15452  elplyd  15458  ply1term  15460  plymullem  15467  efcn  15485  sinhalfpilem  15508  sincosq1lem  15542  tangtx  15555  sincos4thpi  15557  pigt3  15561  dfrelog  15577  relogf1o  15578  log1  15583  loge  15584  relogiso  15590  2logb9irr  15688  2logb9irrap  15694  2sqlem9  15846  2sqlem10  15847  uhgr0e  15926  uhgr0  15929  umgrbien  15954  usgr0  16083  griedg0prc  16094  1loopgruspgr  16114  ex-fl  16271  bj-nndcALT  16304  bj-axempty  16438  bj-axempty2  16439  bdinex1  16444  bj-zfpair2  16455  bj-uniex2  16461  bj-indint  16476  bj-omind  16479  bj-omex  16487  bj-omelon  16506  pw1ndom3  16539  0nninf  16556  dceqnconst  16614  dcapnconst  16615  gfsum0  16632