Theorem mpbi 145

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74i  180  pm4.71i  391  pm4.71ri  392  pm5.32i  454  biadanii  613  pm3.24  694  olc  712  orc  713  dcnn  849  dn1dc  962  3ori  1311  mptxor  1435  mpgbi  1463  dveeq2  1826  dveeq2or  1827  sbequilem  1849  nfsb  1958  sbco  1980  sbcocom  1982  hbsbd  1994  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  hbe1a  2035  elsb1  2167  elsb2  2168  eqcomi  2193  eqtri  2210  eleqtri  2264  neii  2362  neeqtri  2387  nesymi  2406  necomi  2445  nemtbir  2449  neli  2457  nrex  2582  rexlimi  2600  isseti  2760  eueq1  2924  euxfr2dc  2937  cdeqri  2963  sseqtri  3204  3sstr3i  3210  equncomi  3296  unssi  3325  ssini  3373  unabs  3381  inabs  3382  ddifss  3388  inssddif  3391  rgenm  3540  snid  3638  rabrsndc  3675  rintm  3994  breqtri  4043  bm1.3ii  4139  zfnuleu  4142  zfpow  4193  undifexmid  4211  copsexg  4262  uniop  4273  pwundifss  4303  onunisuci  4450  zfun  4452  op1stb  4496  op1stbg  4497  ordtriexmidlem  4536  ordtriexmid  4538  ordtri2orexmid  4540  2ordpr  4541  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmid  4547  dtruex  4576  ordsoexmid  4579  0elsucexmid  4582  ordtri2or2exmid  4588  dcextest  4598  tfi  4599  relop  4795  dmxpid  4866  rn0  4901  dmresi  4980  issref  5029  cnvcnv  5099  rescnvcnv  5109  cnvcnvres  5110  cnvsn  5129  cocnvcnv2  5158  cores2  5159  co01  5161  relcoi1  5178  cnviinm  5188  fnopab  5359  mpt0  5362  fnmpti  5363  f1cnvcnv  5451  f1ovi  5519  fmpti  5689  fvsnun2  5735  oprabss  5983  2nd0  6171  f1stres  6185  f2ndres  6186  reldmtpos  6279  dftpos4  6289  tpostpos  6290  tpos0  6300  smo0  6324  frecfnom  6427  oasuc  6490  uniixp  6748  ssdomg  6805  xpcomf1o  6852  ssfilem  6904  diffitest  6916  inffiexmid  6935  fiintim  6958  caseinl  7121  caseinr  7122  eninl  7127  eninr  7128  card0  7218  dju1p1e2  7227  pw1on  7256  dmaddpi  7355  dmmulpi  7356  1lt2pi  7370  1lt2nq  7436  suplocsrlempr  7837  gtso  8067  subf  8190  negne0i  8263  negdii  8272  ltapii  8623  sup3exmid  8945  neg1ap0  9059  halflt1  9167  nn0ssz  9302  3halfnz  9381  zeo  9389  numlt  9439  numltc  9440  le9lt10  9441  decle  9448  uzf  9562  indstr  9625  infrenegsupex  9626  xaddf  9876  ixxf  9930  iooval2  9947  ioof  10003  unirnioo  10005  fzval2  10043  fzf  10044  fz10  10078  fzpreddisj  10103  4fvwrd4  10172  fzof  10176  fldiv4p1lem1div2  10338  sqrt2gt1lt2  11093  infxrnegsupex  11306  fclim  11337  fsumrelem  11514  arisum2  11542  geo2sum2  11558  0.999...  11564  ege2le3  11714  sin0  11772  ef01bndlem  11799  cos2bnd  11803  cos01gt0  11805  sincos2sgn  11808  sin4lt0  11809  egt2lt3  11822  n2dvds1  11952  flodddiv4  11974  gcdf  12008  eucalgf  12090  2prm  12162  dfphi2  12255  pockthi  12393  znnen  12452  ennnfonelem1  12461  qnnen  12485  ctiunct  12494  ssnnctlemct  12500  structcnvcnv  12531  structfn  12534  relelbasov  12577  xpsff1o  12828  rmodislmod  13684  cnfld0  13891  cnfld1  13892  eltpsi  14018  unitg  14039  epttop  14067  txuni2  14233  retopon  14503  dedekindicclemicc  14587  reldvg  14625  dvrecap  14654  dvef  14665  sinhalfpilem  14689  coseq00topi  14733  coseq0negpitopi  14734  sincos4thpi  14738  sincos6thpi  14740  pigt3  14742  cos02pilt1  14749  logltb  14772  rpabscxpbnd  14836  lgsdir2lem2  14908  lgsdir2lem3  14909  ex-fl  14955  ex-exp  14957  bdceqi  15073  bdcriota  15113  bdsepnfALT  15119  bdbm1.3ii  15121  bj-d0clsepcl  15155  nninfsellemeqinf  15244