Theorem mpbir 200

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 197	. 2 ⊢ (ψ → φ)
4	1, 3	ax-mp 8	1 ⊢ φ

Syntax hints:   ↔ wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2486  neirr  2521  exmidne  2522  eqnetri  2533  mprgbir  2684  vex  2862  issetri  2866  moeq  3012  ru  3045  eqsstri  3301  3sstr4i  3310  necompl  3544  tpid1  3829  tpid2  3830  tpid3  3832  pwv  3886  uni0  3918  nincompl  4072  ninexg  4097  snex  4111  opkth1g  4130  snel1c  4140  1cex  4142  0nel1c  4159  opkabssvvk  4208  eqrelkriiv  4213  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  xpkvexg  4285  ins2kexg  4305  ins3kexg  4306  0cnsuc  4401  nulel0c  4422  0fin  4423  nnsucelr  4428  vfin1cltv  4547  phiall  4618  eqbrtri  4658  dmi  4919  coi2  5095  funi  5137  funsn  5147  fun0  5154  f10  5316  f1o00  5317  f1oi  5320  f1ovi  5321  f1osn  5322  fvopab3ig  5387  1stfo  5505  2ndfo  5506  swapf1o  5511  swapres  5512  opfv1st  5514  opfv2nd  5515  dmep  5524  ovidig  5593  ovidi  5594  ovig  5597  ov3  5599  funmpt  5687  op1st2nd  5790  composefn  5818  fnfullfun  5858  fvfullfunlem2  5862  ssetpov  5944  fundmen  6043  xpassen  6057  enprmaplem5  6080  enpw  6087  muccom  6134  mucass  6135  1cnc  6139  df1c3  6140  mucid1  6143  ncaddccl  6144  ncpwpw1  6153  1p1e2c  6155  2p1e3c  6156  tcdi  6164  fnce  6176  ce0addcnnul  6179  ce0nulnc  6184  fce  6188  ce2  6192  tlenc1c  6240  ncvsq  6256  0lt1c  6258  nmembers1lem2  6269  nchoicelem9  6297  dmfrec  6316