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  698  stabnot  841  mpbir2an  951  mpbir3an  1206  tru  1402  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  mpgbir  1502  nfxfr  1523  19.8a  1639  sbt  1833  dveeq2  1864  dveeq2or  1865  sbequilem  1887  cbvex2  1974  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  nfeuv  2100  moaneu  2159  moanmo  2160  eqeltri  2307  nfcxfr  2383  neir  2417  neirr  2423  eqnetri  2437  nesymir  2461  nelir  2512  mprgbir  2602  vex  2818  issetri  2825  moeq  2994  cdeqi  3029  ru  3043  eqsstri  3272  3sstr4i  3281  mosn  3727  rabrsndc  3761  tpid1  3805  tpid2  3807  tpid3  3810  pwv  3915  uni0  3943  eqbrtri  4132  tr0  4221  trv  4222  zfnuleu  4236  0ex  4239  inex1  4246  elpwi2  4272  0elpw  4279  axpow2  4291  axpow3  4292  vpwex  4294  zfpair2  4325  exss  4345  opwo0id  4367  moop2  4370  pwundifss  4408  po0  4434  epse  4465  fr0  4474  0elon  4515  onm  4524  uniex2  4559  snnex  4571  ordtriexmidlem  4643  ordtriexmid  4645  ontr2exmid  4649  ordtri2or2exmidlem  4650  onsucsssucexmid  4651  onsucelsucexmidlem  4653  ruALT  4675  zfregfr  4698  dcextest  4705  zfinf2  4713  omex  4717  finds  4724  finds2  4725  ordom  4731  omsinds  4746  relsnop  4858  relxp  4861  rel0  4879  relopabiv  4880  relopabi  4882  eliunxp  4896  opeliunxp2  4897  dmi  4973  xpidtr  5155  cnvcnv  5217  dmsn0  5232  cnvsn0  5233  funmpt  5392  funmpt2  5393  funinsn  5407  isarep2  5445  f0  5560  f10  5651  f10d  5652  f1o00  5653  f1oi  5656  f1osn  5658  brprcneu  5665  fvopab3ig  5753  opabex  5912  eufnfv  5919  mpofun  6157  reldmmpo  6167  ovid  6172  ovidig  6173  ovidi  6174  ovig  6177  ovi3  6193  relmptopab  6258  oprabex  6323  oprabex3  6324  f1stres  6355  f2ndres  6356  opeliunxp2f  6471  tpos0  6507  issmo  6521  tfrlem6  6549  tfrlem8  6551  tfri1dALT  6584  tfrcl  6597  rdgfun  6606  frecfun  6628  frecfcllem  6637  0lt1o  6675  eqer  6801  ecopover  6869  ecopoverg  6872  th3qcor  6875  mapsnf1o3  6934  ssdomg  7020  ensn1  7038  xpcomf1o  7078  fiunsnnn  7140  finexdc  7162  elssdc  7164  exmidpw  7170  fissfi  7218  dcfi  7270  omct  7410  infnninf  7417  infnninfOLD  7418  pm54.43  7489  exmidonfinlem  7498  pw1on  7538  pw1dom2  7539  pw1ne1  7541  2oneel  7575  dmaddpi  7645  dmmulpi  7646  1lt2pi  7660  indpi  7662  1lt2nq  7726  genpelxp  7831  ltexprlempr  7928  recexprlempr  7952  cauappcvgprlemcl  7973  cauappcvgprlemladd  7978  caucvgprlemcl  7996  caucvgprprlemcl  8024  m1p1sr  8080  m1m1sr  8081  0lt1sr  8085  peano1nnnn  8172  ax1cn  8181  ax1re  8182  axaddf  8188  axmulf  8189  ax0lt1  8196  0lt1  8405  subaddrii  8567  ixi  8862  1ap0  8869  sup3exmid  9236  nn1suc  9261  neg1lt0  9350  4d2e2  9403  iap0  9466  un0mulcl  9535  pnf0xnn0  9575  3halfnz  9681  nummac  9759  uzf  9862  mnfltpnf  10124  ixxf  10237  ioof  10310  fzf  10352  fzp1disj  10421  fzp1nel  10445  fzo0  10511  frecfzennn  10795  frechashgf1o  10797  xnn0nnen  10806  fxnn0nninf  10808  seq3f1olemp  10884  sq0  10999  irec  11008  hash0  11167  prhash2ex  11182  hashfibclem  11214  climmo  11991  sum0  12082  fisumcom2  12132  prod0  12279  fprodcom2fi  12320  cos1bnd  12453  cos2bnd  12454  3dvds  12558  n2dvdsm1  12607  n2dvds3  12609  flodddiv4  12630  3lcm2e6woprm  12791  6lcm4e12  12792  2prm  12832  3lcm2e6  12865  pockthi  13064  modsubi  13125  ballotfilemcdc  13150  ballotfilem2  13153  unennn  13169  ssnnctlemct  13218  structcnvcnv  13249  strleun  13338  starvndxnbasendx  13376  starvndxnplusgndx  13377  starvndxnmulrndx  13378  scandxnbasendx  13388  scandxnplusgndx  13389  scandxnmulrndx  13390  vscandxnbasendx  13393  vscandxnplusgndx  13394  vscandxnmulrndx  13395  vscandxnscandx  13396  ipndxnbasendx  13406  ipndxnplusgndx  13407  ipndxnmulrndx  13408  slotsdifipndx  13409  tsetndxnplusgndx  13426  tsetndxnmulrndx  13427  tsetndxnstarvndx  13428  slotstnscsi  13429  plendxnplusgndx  13440  plendxnmulrndx  13441  plendxnscandx  13442  plendxnvscandx  13443  slotsdifplendx  13444  basendxnocndx  13447  plendxnocndx  13448  dsndxnplusgndx  13455  dsndxnmulrndx  13456  slotsdnscsi  13457  dsndxntsetndx  13458  slotsdifdsndx  13459  unifndxntsetndx  13465  slotsdifunifndx  13466  restid  13484  prdsval  13507  mgmidmo  13606  opprringb  14246  reldvdsr  14258  rrgmex  14429  lssmex  14552  lidlmex  14672  2idlmex  14698  fczpsrbag  14869  tgdom  14986  tgidm  14988  resttopon  15085  rest0  15093  psmetrel  15236  metrel  15256  xmetrel  15257  xmetf  15264  0met  15298  mopnrel  15355  setsmsbasg  15393  setsmsdsg  15394  qtopbasss  15435  reldvg  15593  dvexp  15625  dveflem  15640  elply2  15649  elplyd  15655  ply1term  15657  plymullem  15664  efcn  15682  sinhalfpilem  15705  sincosq1lem  15739  tangtx  15752  sincos4thpi  15754  pigt3  15758  dfrelog  15774  relogf1o  15775  log1  15780  loge  15781  relogiso  15787  2logb9irr  15885  2logb9irrap  15891  2sqlem9  16046  2sqlem10  16047  uhgr0e  16126  uhgr0  16129  umgrbien  16154  usgr0  16283  griedg0prc  16294  1loopgruspgr  16347  konigsbergumgr  16531  konigsberglem1  16532  ex-fl  16542  bj-nndcALT  16579  bj-axempty  16712  bj-axempty2  16713  bdinex1  16718  bj-zfpair2  16729  bj-uniex2  16735  bj-indint  16750  bj-omind  16753  bj-omex  16761  bj-omelon  16780  pw1ndom3  16813  0nninf  16831  dceqnconst  16895  dcapnconst  16896  gfsum0  16913