Theorem mpbir 200

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

Hypotheses

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

Assertion

Ref	Expression
mpbir	|- ph

Proof of Theorem mpbir

Step	Hyp	Ref	Expression
1		mpbir.min	. 2 |- ps
2		mpbir.maj	. . 3 |- (ph <-> ps)
3	2	biimpri 197	. 2 |- (ps -> ph)
4	1, 3	ax-mp 5	1 |- ph

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.74ri  237  con4bii  288  orri  365  imorri  403  imnani  412  mpbir2an  886  mpbir3an  1134  tru  1321  nic-mpALT  1437  nic-ax  1438  nic-axALT  1439  mpto2OLD  1535  mtp-xor  1536  mtp-xorOLD  1537  mpgbir  1550  nfxfr  1570  19.35ri  1602  a9ev  1656  exiftruOLD  1658  a9e  1951  cbval2  2004  cbvex2  2005  sbt  2033  moaneu  2263  moanmo  2264  axi12  2333  axext2  2335  eqeltri  2423  nfcxfr  2487  neirr  2522  exmidne  2523  eqnetri  2534  mprgbir  2685  vex  2863  issetri  2867  moeq  3013  ru  3046  eqsstri  3302  3sstr4i  3311  necompl  3545  tpid1  3830  tpid2  3831  tpid3  3833  pwv  3887  uni0  3919  nincompl  4073  ninexg  4098  snex  4112  opkth1g  4131  snel1c  4141  1cex  4143  0nel1c  4160  opkabssvvk  4209  eqrelkriiv  4214  sikss1c1c  4268  ins2kss  4280  ins3kss  4281  xpkvexg  4286  ins2kexg  4306  ins3kexg  4307  0cnsuc  4402  nulel0c  4423  0fin  4424  nnsucelr  4429  vfin1cltv  4548  phiall  4619  eqbrtri  4659  dmi  4920  coi2  5096  funi  5138  funsn  5148  fun0  5155  f10  5317  f1o00  5318  f1oi  5321  f1ovi  5322  f1osn  5323  fvopab3ig  5388  1stfo  5506  2ndfo  5507  swapf1o  5512  swapres  5513  opfv1st  5515  opfv2nd  5516  dmep  5525  ovidig  5594  ovidi  5595  ovig  5598  ov3  5600  funmpt  5688  op1st2nd  5791  composefn  5819  fnfullfun  5859  fvfullfunlem2  5863  ssetpov  5945  fundmen  6044  xpassen  6058  enprmaplem5  6081  enpw  6088  muccom  6135  mucass  6136  1cnc  6140  df1c3  6141  mucid1  6144  ncaddccl  6145  ncpwpw1  6154  1p1e2c  6156  2p1e3c  6157  tcdi  6165  fnce  6177  ce0addcnnul  6180  ce0nulnc  6185  fce  6189  ce2  6193  tlenc1c  6241  ncvsq  6257  0lt1c  6259  nmembers1lem2  6270  nchoicelem9  6298  dmfrec  6317