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  693  olc  711  orc  712  dcnn  848  dn1dc  960  3ori  1300  mptxor  1424  mpgbi  1452  dveeq2  1815  dveeq2or  1816  sbequilem  1838  nfsb  1946  sbco  1968  sbcocom  1970  hbsbd  1982  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  hbe1a  2023  elsb1  2155  elsb2  2156  eqcomi  2181  eqtri  2198  eleqtri  2252  neii  2349  neeqtri  2374  nesymi  2393  necomi  2432  nemtbir  2436  neli  2444  nrex  2569  rexlimi  2587  isseti  2747  eueq1  2911  euxfr2dc  2924  cdeqri  2950  sseqtri  3191  3sstr3i  3197  equncomi  3283  unssi  3312  ssini  3360  unabs  3368  inabs  3369  ddifss  3375  inssddif  3378  rgenm  3527  snid  3625  rabrsndc  3662  rintm  3981  breqtri  4030  bm1.3ii  4126  zfnuleu  4129  zfpow  4177  undifexmid  4195  copsexg  4246  uniop  4257  pwundifss  4287  onunisuci  4434  zfun  4436  op1stb  4480  op1stbg  4481  ordtriexmidlem  4520  ordtriexmid  4522  ordtri2orexmid  4524  2ordpr  4525  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  dtruex  4560  ordsoexmid  4563  0elsucexmid  4566  ordtri2or2exmid  4572  dcextest  4582  tfi  4583  relop  4779  dmxpid  4850  rn0  4885  dmresi  4964  issref  5013  cnvcnv  5083  rescnvcnv  5093  cnvcnvres  5094  cnvsn  5113  cocnvcnv2  5142  cores2  5143  co01  5145  relcoi1  5162  cnviinm  5172  fnopab  5342  mpt0  5345  fnmpti  5346  f1cnvcnv  5434  f1ovi  5502  fmpti  5670  fvsnun2  5716  oprabss  5963  2nd0  6148  f1stres  6162  f2ndres  6163  reldmtpos  6256  dftpos4  6266  tpostpos  6267  tpos0  6277  smo0  6301  frecfnom  6404  oasuc  6467  uniixp  6723  ssdomg  6780  xpcomf1o  6827  ssfilem  6877  diffitest  6889  inffiexmid  6908  fiintim  6930  caseinl  7092  caseinr  7093  eninl  7098  eninr  7099  card0  7189  dju1p1e2  7198  pw1on  7227  dmaddpi  7326  dmmulpi  7327  1lt2pi  7341  1lt2nq  7407  suplocsrlempr  7808  gtso  8038  subf  8161  negne0i  8234  negdii  8243  ltapii  8594  sup3exmid  8916  neg1ap0  9030  halflt1  9138  nn0ssz  9273  3halfnz  9352  zeo  9360  numlt  9410  numltc  9411  le9lt10  9412  decle  9419  uzf  9533  indstr  9595  infrenegsupex  9596  xaddf  9846  ixxf  9900  iooval2  9917  ioof  9973  unirnioo  9975  fzval2  10013  fzf  10014  fz10  10048  fzpreddisj  10073  4fvwrd4  10142  fzof  10146  fldiv4p1lem1div2  10307  sqrt2gt1lt2  11060  infxrnegsupex  11273  fclim  11304  fsumrelem  11481  arisum2  11509  geo2sum2  11525  0.999...  11531  ege2le3  11681  sin0  11739  ef01bndlem  11766  cos2bnd  11770  cos01gt0  11772  sincos2sgn  11775  sin4lt0  11776  egt2lt3  11789  n2dvds1  11919  flodddiv4  11941  gcdf  11975  eucalgf  12057  2prm  12129  dfphi2  12222  pockthi  12358  znnen  12401  ennnfonelem1  12410  qnnen  12434  ctiunct  12443  ssnnctlemct  12449  structcnvcnv  12480  structfn  12483  xpsff1o  12773  rmodislmod  13446  cnfld0  13504  cnfld1  13505  eltpsi  13580  unitg  13601  epttop  13629  txuni2  13795  retopon  14065  dedekindicclemicc  14149  reldvg  14187  dvrecap  14216  dvef  14227  sinhalfpilem  14251  coseq00topi  14295  coseq0negpitopi  14296  sincos4thpi  14300  sincos6thpi  14302  pigt3  14304  cos02pilt1  14311  logltb  14334  rpabscxpbnd  14398  lgsdir2lem2  14469  lgsdir2lem3  14470  ex-fl  14516  ex-exp  14518  bdceqi  14634  bdcriota  14674  bdsepnfALT  14680  bdbm1.3ii  14682  bj-d0clsepcl  14716  nninfsellemeqinf  14804