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 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74i  179  pm4.71i  389  pm4.71ri  390  pm5.32i  450  biadanii  603  pm3.24  683  olc  701  orc  702  dcnn  838  dn1dc  950  3ori  1290  mptxor  1414  mpgbi  1440  dveeq2  1803  dveeq2or  1804  sbequilem  1826  nfsb  1934  sbco  1956  sbcocom  1958  hbsbd  1970  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  hbe1a  2011  elsb1  2143  elsb2  2144  eqcomi  2169  eqtri  2186  eleqtri  2241  neii  2338  neeqtri  2363  nesymi  2382  necomi  2421  nemtbir  2425  neli  2433  nrex  2558  rexlimi  2576  isseti  2734  eueq1  2898  euxfr2dc  2911  cdeqri  2937  sseqtri  3176  3sstr3i  3182  equncomi  3268  unssi  3297  ssini  3345  unabs  3353  inabs  3354  ddifss  3360  inssddif  3363  rgenm  3511  snid  3607  rabrsndc  3644  rintm  3958  breqtri  4007  bm1.3ii  4103  zfnuleu  4106  zfpow  4154  undifexmid  4172  copsexg  4222  uniop  4233  pwundifss  4263  onunisuci  4410  zfun  4412  op1stb  4456  op1stbg  4457  ordtriexmidlem  4496  ordtriexmid  4498  ordtri2orexmid  4500  2ordpr  4501  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  dtruex  4536  ordsoexmid  4539  0elsucexmid  4542  ordtri2or2exmid  4548  dcextest  4558  tfi  4559  relop  4754  dmxpid  4825  rn0  4860  dmresi  4939  issref  4986  cnvcnv  5056  rescnvcnv  5066  cnvcnvres  5067  cnvsn  5086  cocnvcnv2  5115  cores2  5116  co01  5118  relcoi1  5135  cnviinm  5145  fnopab  5312  mpt0  5315  fnmpti  5316  f1cnvcnv  5404  f1ovi  5471  fmpti  5637  fvsnun2  5683  oprabss  5928  2nd0  6113  f1stres  6127  f2ndres  6128  reldmtpos  6221  dftpos4  6231  tpostpos  6232  tpos0  6242  smo0  6266  frecfnom  6369  oasuc  6432  uniixp  6687  ssdomg  6744  xpcomf1o  6791  ssfilem  6841  diffitest  6853  inffiexmid  6872  fiintim  6894  caseinl  7056  caseinr  7057  eninl  7062  eninr  7063  card0  7144  dju1p1e2  7153  pw1on  7182  dmaddpi  7266  dmmulpi  7267  1lt2pi  7281  1lt2nq  7347  suplocsrlempr  7748  gtso  7977  subf  8100  negne0i  8173  negdii  8182  ltapii  8533  sup3exmid  8852  neg1ap0  8966  halflt1  9074  nn0ssz  9209  3halfnz  9288  zeo  9296  numlt  9346  numltc  9347  le9lt10  9348  decle  9355  uzf  9469  indstr  9531  infrenegsupex  9532  xaddf  9780  ixxf  9834  iooval2  9851  ioof  9907  unirnioo  9909  fzval2  9947  fzf  9948  fz10  9981  fzpreddisj  10006  4fvwrd4  10075  fzof  10079  fldiv4p1lem1div2  10240  sqrt2gt1lt2  10991  infxrnegsupex  11204  fclim  11235  fsumrelem  11412  arisum2  11440  geo2sum2  11456  0.999...  11462  ege2le3  11612  sin0  11670  ef01bndlem  11697  cos2bnd  11701  cos01gt0  11703  sincos2sgn  11706  sin4lt0  11707  egt2lt3  11720  n2dvds1  11849  flodddiv4  11871  gcdf  11905  eucalgf  11987  2prm  12059  dfphi2  12152  pockthi  12288  znnen  12331  ennnfonelem1  12340  qnnen  12364  ctiunct  12373  ssnnctlemct  12379  structcnvcnv  12410  structfn  12413  eltpsi  12679  unitg  12702  epttop  12730  txuni2  12896  retopon  13166  dedekindicclemicc  13250  reldvg  13288  dvrecap  13317  dvef  13328  sinhalfpilem  13352  coseq00topi  13396  coseq0negpitopi  13397  sincos4thpi  13401  sincos6thpi  13403  pigt3  13405  cos02pilt1  13412  logltb  13435  rpabscxpbnd  13499  lgsdir2lem2  13570  lgsdir2lem3  13571  ex-fl  13606  ex-exp  13608  bdceqi  13725  bdcriota  13765  bdsepnfALT  13771  bdbm1.3ii  13773  bj-d0clsepcl  13807  nninfsellemeqinf  13896