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  1466  dveeq2  1829  dveeq2or  1830  sbequilem  1852  nfsb  1965  sbco  1987  sbcocom  1989  hbsbd  2001  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  hbe1a  2042  elsb1  2174  elsb2  2175  eqcomi  2200  eqtri  2217  eleqtri  2271  neii  2369  neeqtri  2394  nesymi  2413  necomi  2452  nemtbir  2456  neli  2464  nrex  2589  rexlimi  2607  isseti  2771  eueq1  2936  euxfr2dc  2949  cdeqri  2975  sseqtri  3218  3sstr3i  3224  equncomi  3310  unssi  3339  ssini  3387  unabs  3395  inabs  3396  ddifss  3402  inssddif  3405  snid  3654  rabrsndc  3691  rintm  4010  breqtri  4059  bm1.3ii  4155  zfnuleu  4158  zfpow  4209  undifexmid  4227  copsexg  4278  uniop  4289  pwundifss  4321  onunisuci  4468  zfun  4470  op1stb  4514  op1stbg  4515  ordtriexmidlem  4556  ordtriexmid  4558  ordtri2orexmid  4560  2ordpr  4561  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  dtruex  4596  ordsoexmid  4599  0elsucexmid  4602  ordtri2or2exmid  4608  dcextest  4618  tfi  4619  relop  4817  dmxpid  4888  rn0  4923  dmresi  5002  issref  5053  cnvcnv  5123  rescnvcnv  5133  cnvcnvres  5134  cnvsn  5153  cocnvcnv2  5182  cores2  5183  co01  5185  relcoi1  5202  cnviinm  5212  fnopab  5385  mpt0  5388  fnmpti  5389  f1cnvcnv  5477  f1ovi  5546  fmpti  5717  fvsnun2  5763  oprabss  6012  2nd0  6212  f1stres  6226  f2ndres  6227  reldmtpos  6320  dftpos4  6330  tpostpos  6331  tpos0  6341  smo0  6365  frecfnom  6468  oasuc  6531  uniixp  6789  ssdomg  6846  xpcomf1o  6893  ssfilem  6945  diffitest  6957  inffiexmid  6976  fiintim  7001  caseinl  7166  caseinr  7167  eninl  7172  eninr  7173  card0  7268  dju1p1e2  7278  pw1on  7311  dmaddpi  7411  dmmulpi  7412  1lt2pi  7426  1lt2nq  7492  suplocsrlempr  7893  gtso  8124  subf  8247  negne0i  8320  negdii  8329  ltapii  8681  sup3exmid  9003  neg1ap0  9118  halflt1  9227  nn0ssz  9363  3halfnz  9442  zeo  9450  numlt  9500  numltc  9501  le9lt10  9502  decle  9509  uzf  9623  indstr  9686  infrenegsupex  9687  xaddf  9938  ixxf  9992  iooval2  10009  ioof  10065  unirnioo  10067  fzval2  10105  fzf  10106  fz10  10140  fzpreddisj  10165  4fvwrd4  10234  fzof  10238  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  xnn0nnen  10548  sqrt2gt1lt2  11233  infxrnegsupex  11447  fclim  11478  fsumrelem  11655  arisum2  11683  geo2sum2  11699  0.999...  11705  ege2le3  11855  sin0  11913  ef01bndlem  11940  cos2bnd  11944  cos01gt0  11947  sincos2sgn  11950  sin4lt0  11951  egt2lt3  11964  n2dvds1  12096  flodddiv4  12120  0bits  12143  gcdf  12166  nninfct  12235  eucalgf  12250  2prm  12322  dfphi2  12415  pockthi  12554  karatsuba  12626  znnen  12642  ennnfonelem1  12651  qnnen  12675  ctiunct  12684  ssnnctlemct  12690  structcnvcnv  12721  structfn  12724  relelbasov  12767  xpsff1o  13053  rmodislmod  13985  cnfld0  14205  cnfld1  14206  eltpsi  14385  unitg  14406  epttop  14434  txuni2  14600  retopon  14870  cnfldtopon  14884  dedekindicclemicc  14976  reldvg  15023  dvrecap  15057  dvef  15071  plyrecj  15107  sinhalfpilem  15135  coseq00topi  15179  coseq0negpitopi  15180  sincos4thpi  15184  sincos6thpi  15186  pigt3  15188  cos02pilt1  15195  logltb  15218  rpabscxpbnd  15284  sgmf  15330  1sgm2ppw  15339  lgsdir2lem2  15378  lgsdir2lem3  15379  ex-fl  15479  ex-exp  15481  bdceqi  15597  bdcriota  15637  bdsepnfALT  15643  bdbm1.3ii  15645  bj-d0clsepcl  15679  nninfsellemeqinf  15771