Theorem mpbi 199

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

Hypotheses

Ref	Expression
mpbi.min	|- ph
mpbi.maj	|- (ph <-> ps)

Assertion

Ref	Expression
mpbi	|- ps

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 |- ph
2		mpbi.maj	. . 3 |- (ph <-> ps)
3	2	biimpi 186	. 2 |- (ph -> ps)
4	1, 3	ax-mp 5	1 |- ps

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  2538  necomi  2599  nemtbir  2605  nrex  2717  rexlimi  2732  isseti  2866  vtocl2  2911  vtocl3  2912  eueq1  3010  euxfr2  3022  sseqtri  3304  3sstr3i  3310  pssn2lp  3371  equncomi  3411  unssi  3439  ssini  3479  unabs  3486  inabs  3487  dfin4  3496  npss0  3590  difid  3619  disjdif  3623  difin0  3624  snid  3761  snsssn  3874  iinrab2  4030  rintn0  4057  axxpprim  4091  axcnvprim  4092  axssetprim  4093  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  iota4an  4359  ltfinirr  4458  evenoddnnnul  4515  evenodddisj  4517  vfinspeqtncv  4554  0cnelphi  4598  copsexg  4608  opeq  4620  breqtri  4663  rn0  4970  dmresi  5005  nfunv  5139  fnopab  5208  xpsn  5436  fvi  5443  fvsnun2  5449  xpnedisj  5514  fnmpti  5691  fmpti  5694  fncup  5814  addcfn  5826  epprc  5828  fncross  5847  fnfullfun  5859  fvfullfun  5865  fnmap  6008  fnpm  6009  dmen  6042  xpsnen  6050  xpcomen  6053  xpassen  6058  enpw1pw  6076  ncpwpw1  6154  ce0addcnnul  6180  sbthlem1  6204  cet  6235  0lt1c  6259  nmembers1lem2  6270  ltcirr  6273  nnc3n3p1  6279  nchoicelem5  6294  fnfreclem2  6319  fnfreclem3  6320