Theorem mpbi 143

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

Syntax hints:   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.74i  178  pm4.71i  383  pm4.71ri  384  pm5.32i  442  pm3.24  660  olc  665  orc  666  dn1dc  904  3ori  1234  mptxor  1358  mpgbi  1384  dveeq2  1740  dveeq2or  1741  sbequilem  1763  nfsb  1867  sbco  1887  sbcocom  1889  elsb3  1897  elsb4  1898  hbsbd  1903  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  eqcomi  2089  eqtri  2105  eleqtri  2159  neii  2253  neeqtri  2278  nesymi  2297  necomi  2336  nemtbir  2340  neli  2348  nrex  2461  rexlimi  2478  isseti  2621  eueq1  2778  euxfr2dc  2791  cdeqri  2815  sseqtri  3047  3sstr3i  3053  equncomi  3135  unssi  3164  ssini  3212  unabs  3219  inabs  3220  ddifss  3226  inssddif  3229  rgenm  3371  snid  3458  rabrsndc  3493  rintm  3800  breqtri  3843  bm1.3ii  3935  zfnuleu  3938  zfpow  3985  undifexmid  4002  copsexg  4045  uniop  4056  pwundifss  4086  onunisuci  4233  zfun  4235  op1stb  4273  op1stbg  4274  ordtriexmidlem  4309  ordtriexmid  4311  ordtri2orexmid  4312  2ordpr  4313  ontr2exmid  4314  onsucsssucexmid  4316  onsucelsucexmid  4319  dtruex  4348  ordsoexmid  4351  0elsucexmid  4354  ordtri2or2exmid  4360  dcextest  4369  tfi  4370  relop  4554  rn0  4657  dmresi  4734  issref  4781  cnvcnv  4849  rescnvcnv  4859  cnvcnvres  4860  cnvsn  4879  cocnvcnv2  4908  cores2  4909  co01  4911  relcoi1  4928  cnviinm  4938  fnopab  5103  mpt0  5106  fnmpti  5107  f1cnvcnv  5190  f1ovi  5255  fmpti  5414  fvsnun2  5458  oprabss  5691  2nd0  5873  f1stres  5887  f2ndres  5888  reldmtpos  5972  dftpos4  5982  tpostpos  5983  tpos0  5993  smo0  6017  frecfnom  6120  oasuc  6179  ssdomg  6447  xpcomf1o  6493  ssfilem  6543  diffitest  6555  inffiexmid  6574  card0  6760  dju1p1e2  6767  dmaddpi  6828  dmmulpi  6829  1lt2pi  6843  1lt2nq  6909  gtso  7508  subf  7628  negne0i  7701  negdii  7710  ltapii  8051  neg1ap0  8466  halflt1  8566  nn0ssz  8701  3halfnz  8776  zeo  8784  numlt  8833  numltc  8834  le9lt10  8835  decle  8842  uzf  8954  indstr  9013  infrenegsupex  9014  ixxf  9248  iooval2  9265  ioof  9321  unirnioo  9323  fzval2  9359  fzf  9360  fz10  9392  fzpreddisj  9415  4fvwrd4  9479  fzof  9483  fldiv4p1lem1div2  9640  sqrt2gt1lt2  10377  fclim  10575  n2dvds1  10787  flodddiv4  10809  gcdf  10839  eucalgf  10912  2prm  10984  dfphi2  11071  znnen  11086  ex-fl  11091  bdceqi  11172  bdcriota  11212  bdsepnfALT  11218  bdbm1.3ii  11220  bj-d0clsepcl  11258  nninfsellemeqinf  11346