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  697  stabnot  840  mpbir2an  950  mpbir3an  1205  tru  1401  dcfromnotnotr  1492  dcfromcon  1493  dcfrompeirce  1494  mpgbir  1501  nfxfr  1522  19.8a  1638  sbt  1831  dveeq2  1862  dveeq2or  1863  sbequilem  1885  cbvex2  1970  dvelimALT  2062  dvelimfv  2063  dvelimor  2070  nfeuv  2096  moaneu  2155  moanmo  2156  eqeltri  2303  nfcxfr  2370  neir  2404  neirr  2410  eqnetri  2424  nesymir  2448  nelir  2499  mprgbir  2589  vex  2804  issetri  2811  moeq  2980  cdeqi  3015  ru  3029  eqsstri  3258  3sstr4i  3267  mosn  3706  rabrsndc  3740  tpid1  3784  tpid2  3786  tpid3  3789  pwv  3893  uni0  3921  eqbrtri  4110  tr0  4199  trv  4200  zfnuleu  4214  0ex  4217  inex1  4224  elpwi2  4249  0elpw  4256  axpow2  4268  axpow3  4269  vpwex  4271  zfpair2  4302  exss  4321  opwo0id  4343  moop2  4346  pwundifss  4384  po0  4410  epse  4441  fr0  4450  0elon  4491  onm  4500  uniex2  4535  snnex  4547  ordtriexmidlem  4619  ordtriexmid  4621  ontr2exmid  4625  ordtri2or2exmidlem  4626  onsucsssucexmid  4627  onsucelsucexmidlem  4629  ruALT  4651  zfregfr  4674  dcextest  4681  zfinf2  4689  omex  4693  finds  4700  finds2  4701  ordom  4707  omsinds  4722  relsnop  4834  relxp  4837  rel0  4854  relopabiv  4855  relopabi  4857  eliunxp  4871  opeliunxp2  4872  dmi  4948  xpidtr  5129  cnvcnv  5191  dmsn0  5206  cnvsn0  5207  funmpt  5366  funmpt2  5367  funinsn  5381  isarep2  5419  f0  5530  f10  5621  f10d  5622  f1o00  5623  f1oi  5626  f1osn  5628  brprcneu  5635  fvopab3ig  5723  opabex  5883  eufnfv  5890  mpofun  6128  reldmmpo  6138  ovid  6143  ovidig  6144  ovidi  6145  ovig  6148  ovi3  6164  relmptopab  6229  oprabex  6295  oprabex3  6296  f1stres  6327  f2ndres  6328  opeliunxp2f  6409  tpos0  6445  issmo  6459  tfrlem6  6487  tfrlem8  6489  tfri1dALT  6522  tfrcl  6535  rdgfun  6544  frecfun  6566  frecfcllem  6575  0lt1o  6613  eqer  6739  ecopover  6807  ecopoverg  6810  th3qcor  6813  mapsnf1o3  6871  ssdomg  6957  ensn1  6975  xpcomf1o  7014  fiunsnnn  7075  finexdc  7097  elssdc  7099  exmidpw  7105  dcfi  7185  omct  7321  infnninf  7328  infnninfOLD  7329  pm54.43  7400  exmidonfinlem  7409  pw1on  7449  pw1dom2  7450  pw1ne1  7452  2oneel  7480  dmaddpi  7550  dmmulpi  7551  1lt2pi  7565  indpi  7567  1lt2nq  7631  genpelxp  7736  ltexprlempr  7833  recexprlempr  7857  cauappcvgprlemcl  7878  cauappcvgprlemladd  7883  caucvgprlemcl  7901  caucvgprprlemcl  7929  m1p1sr  7985  m1m1sr  7986  0lt1sr  7990  peano1nnnn  8077  ax1cn  8086  ax1re  8087  axaddf  8093  axmulf  8094  ax0lt1  8101  0lt1  8311  subaddrii  8473  ixi  8768  1ap0  8775  sup3exmid  9142  nn1suc  9167  neg1lt0  9256  4d2e2  9309  iap0  9372  un0mulcl  9441  pnf0xnn0  9477  3halfnz  9582  nummac  9660  uzf  9763  mnfltpnf  10025  ixxf  10138  ioof  10211  fzf  10252  fzp1disj  10320  fzp1nel  10344  fzo0  10410  frecfzennn  10694  frechashgf1o  10696  xnn0nnen  10705  fxnn0nninf  10707  seq3f1olemp  10783  sq0  10898  irec  10907  hash0  11064  prhash2ex  11079  climmo  11881  sum0  11972  fisumcom2  12022  prod0  12169  fprodcom2fi  12210  cos1bnd  12343  cos2bnd  12344  3dvds  12448  n2dvdsm1  12497  n2dvds3  12499  flodddiv4  12520  3lcm2e6woprm  12681  6lcm4e12  12682  2prm  12722  3lcm2e6  12755  pockthi  12954  modsubi  13015  unennn  13041  ssnnctlemct  13090  structcnvcnv  13121  strleun  13210  starvndxnbasendx  13248  starvndxnplusgndx  13249  starvndxnmulrndx  13250  scandxnbasendx  13260  scandxnplusgndx  13261  scandxnmulrndx  13262  vscandxnbasendx  13265  vscandxnplusgndx  13266  vscandxnmulrndx  13267  vscandxnscandx  13268  ipndxnbasendx  13278  ipndxnplusgndx  13279  ipndxnmulrndx  13280  slotsdifipndx  13281  tsetndxnplusgndx  13298  tsetndxnmulrndx  13299  tsetndxnstarvndx  13300  slotstnscsi  13301  plendxnplusgndx  13312  plendxnmulrndx  13313  plendxnscandx  13314  plendxnvscandx  13315  slotsdifplendx  13316  basendxnocndx  13319  plendxnocndx  13320  dsndxnplusgndx  13327  dsndxnmulrndx  13328  slotsdnscsi  13329  dsndxntsetndx  13330  slotsdifdsndx  13331  unifndxntsetndx  13337  slotsdifunifndx  13338  restid  13356  prdsval  13379  mgmidmo  13478  reldvdsr  14129  rrgmex  14299  lssmex  14393  lidlmex  14513  2idlmex  14539  fczpsrbag  14709  tgdom  14825  tgidm  14827  resttopon  14924  rest0  14932  psmetrel  15075  metrel  15095  xmetrel  15096  xmetf  15103  0met  15137  mopnrel  15194  setsmsbasg  15232  setsmsdsg  15233  qtopbasss  15274  reldvg  15432  dvexp  15464  dveflem  15479  elply2  15488  elplyd  15494  ply1term  15496  plymullem  15503  efcn  15521  sinhalfpilem  15544  sincosq1lem  15578  tangtx  15591  sincos4thpi  15593  pigt3  15597  dfrelog  15613  relogf1o  15614  log1  15619  loge  15620  relogiso  15626  2logb9irr  15724  2logb9irrap  15730  2sqlem9  15882  2sqlem10  15883  uhgr0e  15962  uhgr0  15965  umgrbien  15990  usgr0  16119  griedg0prc  16130  1loopgruspgr  16183  konigsbergumgr  16367  konigsberglem1  16368  ex-fl  16378  bj-nndcALT  16415  bj-axempty  16548  bj-axempty2  16549  bdinex1  16554  bj-zfpair2  16565  bj-uniex2  16571  bj-indint  16586  bj-omind  16589  bj-omex  16597  bj-omelon  16616  pw1ndom3  16649  0nninf  16669  dceqnconst  16732  dcapnconst  16733  gfsum0  16750