Theorem mpbi 199

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbi.min	⊢ φ
mpbi.maj	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mpbi	⊢ ψ

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ φ
2		mpbi.maj	. . 3 ⊢ (φ ↔ ψ)
3	2	biimpi 186	. 2 ⊢ (φ → ψ)
4	1, 3	ax-mp 5	1 ⊢ ψ

Syntax hints:   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  pm5.74i  236  notbii  287  pm5.19  349  ori  364  imori  402  pm4.71i  613  pm4.71ri  614  pm5.32i  618  pm3.24  852  pm5.16  860  biluk  899  4exmid  905  dn1  932  3ori  1242  trubifal  1351  nic-dfim  1434  nic-dfneg  1435  nic-mp  1436  nic-mpALT  1437  tbw-negdf  1464  rb-imdf  1515  mpto2  1534  mpto2OLD  1535  mtp-xorOLD  1537  mpgbi  1549  19.35i  1601  19.36i  1872  19.37aiv  1900  sbco  2083  sbidm  2085  axi12  2333  eqcomi  2357  eqtri  2373  eleqtri  2425  neeqtri  2537  necomi  2598  nemtbir  2604  nrex  2716  rexlimi  2731  isseti  2865  vtocl2  2910  vtocl3  2911  eueq1  3009  euxfr2  3021  sseqtri  3303  3sstr3i  3309  pssn2lp  3370  equncomi  3410  unssi  3438  ssini  3478  unabs  3485  inabs  3486  dfin4  3495  npss0  3589  difid  3618  disjdif  3622  difin0  3623  snid  3760  snsssn  3873  iinrab2  4029  rintn0  4056  axxpprim  4090  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  iota4an  4358  ltfinirr  4457  evenoddnnnul  4514  evenodddisj  4516  vfinspeqtncv  4553  0cnelphi  4597  copsexg  4607  opeq  4619  breqtri  4662  rn0  4969  dmresi  5004  nfunv  5138  fnopab  5207  xpsn  5435  fvi  5442  fvsnun2  5448  xpnedisj  5513  fnmpti  5690  fmpti  5693  fncup  5813  addcfn  5825  epprc  5827  fncross  5846  fnfullfun  5858  fvfullfun  5864  fnmap  6007  fnpm  6008  dmen  6041  xpsnen  6049  xpcomen  6052  xpassen  6057  enpw1pw  6075  ncpwpw1  6153  ce0addcnnul  6179  sbthlem1  6203  cet  6234  0lt1c  6258  nmembers1lem2  6269  ltcirr  6272  nnc3n3p1  6278  nchoicelem5  6293  fnfreclem2  6318  fnfreclem3  6319