Theorem mpbi 144

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 119	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 7	1 ⊢ 𝜓

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74i  179  pm4.71i  386  pm4.71ri  387  pm5.32i  447  biadanii  585  pm3.24  665  olc  683  orc  684  dcnn  816  dn1dc  927  3ori  1261  mptxor  1385  mpgbi  1411  dveeq2  1769  dveeq2or  1770  sbequilem  1792  nfsb  1897  sbco  1917  sbcocom  1919  elsb3  1927  elsb4  1928  hbsbd  1933  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  eqcomi  2119  eqtri  2135  eleqtri  2189  neii  2284  neeqtri  2309  nesymi  2328  necomi  2367  nemtbir  2371  neli  2379  nrex  2498  rexlimi  2516  isseti  2665  eueq1  2825  euxfr2dc  2838  cdeqri  2864  sseqtri  3097  3sstr3i  3103  equncomi  3188  unssi  3217  ssini  3265  unabs  3273  inabs  3274  ddifss  3280  inssddif  3283  rgenm  3431  snid  3522  rabrsndc  3557  rintm  3871  breqtri  3918  bm1.3ii  4009  zfnuleu  4012  zfpow  4059  undifexmid  4077  copsexg  4126  uniop  4137  pwundifss  4167  onunisuci  4314  zfun  4316  op1stb  4359  op1stbg  4360  ordtriexmidlem  4395  ordtriexmid  4397  ordtri2orexmid  4398  2ordpr  4399  ontr2exmid  4400  onsucsssucexmid  4402  onsucelsucexmid  4405  dtruex  4434  ordsoexmid  4437  0elsucexmid  4440  ordtri2or2exmid  4446  dcextest  4455  tfi  4456  relop  4649  dmxpid  4720  rn0  4753  dmresi  4832  issref  4879  cnvcnv  4949  rescnvcnv  4959  cnvcnvres  4960  cnvsn  4979  cocnvcnv2  5008  cores2  5009  co01  5011  relcoi1  5028  cnviinm  5038  fnopab  5205  mpt0  5208  fnmpti  5209  f1cnvcnv  5297  f1ovi  5362  fmpti  5526  fvsnun2  5572  oprabss  5811  2nd0  5997  f1stres  6011  f2ndres  6012  reldmtpos  6104  dftpos4  6114  tpostpos  6115  tpos0  6125  smo0  6149  frecfnom  6252  oasuc  6314  uniixp  6569  ssdomg  6626  xpcomf1o  6672  ssfilem  6722  diffitest  6734  inffiexmid  6753  fiintim  6770  caseinl  6928  caseinr  6929  eninl  6934  eninr  6935  card0  6994  dju1p1e2  7001  dmaddpi  7081  dmmulpi  7082  1lt2pi  7096  1lt2nq  7162  gtso  7766  subf  7887  negne0i  7960  negdii  7969  ltapii  8314  sup3exmid  8625  neg1ap0  8739  halflt1  8841  nn0ssz  8976  3halfnz  9052  zeo  9060  numlt  9110  numltc  9111  le9lt10  9112  decle  9119  uzf  9231  indstr  9290  infrenegsupex  9291  xaddf  9520  ixxf  9574  iooval2  9591  ioof  9647  unirnioo  9649  fzval2  9686  fzf  9687  fz10  9719  fzpreddisj  9744  4fvwrd4  9810  fzof  9814  fldiv4p1lem1div2  9971  sqrt2gt1lt2  10713  infxrnegsupex  10924  fclim  10955  fsumrelem  11132  arisum2  11160  geo2sum2  11176  0.999...  11182  ege2le3  11228  sin0  11287  ef01bndlem  11314  cos2bnd  11318  cos01gt0  11320  sincos2sgn  11323  sin4lt0  11324  egt2lt3  11334  n2dvds1  11457  flodddiv4  11479  gcdf  11509  eucalgf  11582  2prm  11654  dfphi2  11741  znnen  11756  ennnfonelem1  11765  qnnen  11789  ctiunct  11796  structcnvcnv  11818  structfn  11821  eltpsi  12051  unitg  12074  epttop  12102  txuni2  12267  retopon  12515  reldvg  12603  ex-fl  12630  ex-exp  12632  bdceqi  12731  bdcriota  12771  bdsepnfALT  12777  bdbm1.3ii  12779  bj-d0clsepcl  12813  nninfsellemeqinf  12902