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  695  olc  713  orc  714  dcnn  850  dn1dc  963  3ori  1313  mptxor  1444  mpgbi  1476  dveeq2  1839  dveeq2or  1840  sbequilem  1862  nfsb  1975  sbco  1997  sbcocom  1999  hbsbd  2011  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  hbe1a  2052  elsb1  2184  elsb2  2185  eqcomi  2210  eqtri  2227  eleqtri  2281  neii  2379  neeqtri  2404  nesymi  2423  necomi  2462  nemtbir  2466  neli  2474  nrex  2599  rexlimi  2617  isseti  2781  eueq1  2946  euxfr2dc  2959  cdeqri  2985  sseqtri  3228  3sstr3i  3234  equncomi  3320  unssi  3349  ssini  3397  unabs  3405  inabs  3406  ddifss  3412  inssddif  3415  snid  3665  rabrsndc  3702  rintm  4022  breqtri  4072  bm1.3ii  4169  zfnuleu  4172  zfpow  4223  undifexmid  4241  copsexg  4292  uniop  4304  pwundifss  4336  onunisuci  4483  zfun  4485  op1stb  4529  op1stbg  4530  ordtriexmidlem  4571  ordtriexmid  4573  ordtri2orexmid  4575  2ordpr  4576  ontr2exmid  4577  onsucsssucexmid  4579  onsucelsucexmid  4582  dtruex  4611  ordsoexmid  4614  0elsucexmid  4617  ordtri2or2exmid  4623  dcextest  4633  tfi  4634  relop  4832  dmxpid  4904  rn0  4939  dmresi  5019  issref  5070  cnvcnv  5140  rescnvcnv  5150  cnvcnvres  5151  cnvsn  5170  cocnvcnv2  5199  cores2  5200  co01  5202  relcoi1  5219  cnviinm  5229  fnopab  5406  mpt0  5409  fnmpti  5410  f1cnvcnv  5499  f1ovi  5568  fmpti  5739  fvsnun2  5789  oprabss  6038  2nd0  6238  f1stres  6252  f2ndres  6253  reldmtpos  6346  dftpos4  6356  tpostpos  6357  tpos0  6367  smo0  6391  frecfnom  6494  oasuc  6557  uniixp  6815  ssdomg  6877  xpcomf1o  6927  ssfilem  6979  diffitest  6991  inffiexmid  7010  fiintim  7035  caseinl  7200  caseinr  7201  eninl  7206  eninr  7207  card0  7302  dju1p1e2  7312  pw1on  7345  dmaddpi  7445  dmmulpi  7446  1lt2pi  7460  1lt2nq  7526  suplocsrlempr  7927  gtso  8158  subf  8281  negne0i  8354  negdii  8363  ltapii  8715  sup3exmid  9037  neg1ap0  9152  halflt1  9261  nn0ssz  9397  3halfnz  9477  zeo  9485  numlt  9535  numltc  9536  le9lt10  9537  decle  9544  uzf  9658  indstr  9721  infrenegsupex  9722  xaddf  9973  ixxf  10027  iooval2  10044  ioof  10100  unirnioo  10102  fzval2  10140  fzf  10141  fz10  10175  fzpreddisj  10200  4fvwrd4  10269  fzof  10273  fldiv4p1lem1div2  10455  fldiv4lem1div2  10457  xnn0nnen  10589  sqrt2gt1lt2  11404  infxrnegsupex  11618  fclim  11649  fsumrelem  11826  arisum2  11854  geo2sum2  11870  0.999...  11876  ege2le3  12026  sin0  12084  ef01bndlem  12111  cos2bnd  12115  cos01gt0  12118  sincos2sgn  12121  sin4lt0  12122  egt2lt3  12135  n2dvds1  12267  flodddiv4  12291  0bits  12314  gcdf  12337  nninfct  12406  eucalgf  12421  2prm  12493  dfphi2  12586  pockthi  12725  karatsuba  12797  znnen  12813  ennnfonelem1  12822  qnnen  12846  ctiunct  12855  ssnnctlemct  12861  structcnvcnv  12892  structfn  12895  relelbasov  12938  xpsff1o  13225  rmodislmod  14157  cnfld0  14377  cnfld1  14378  eltpsi  14557  unitg  14578  epttop  14606  txuni2  14772  retopon  15042  cnfldtopon  15056  dedekindicclemicc  15148  reldvg  15195  dvrecap  15229  dvef  15243  plyrecj  15279  sinhalfpilem  15307  coseq00topi  15351  coseq0negpitopi  15352  sincos4thpi  15356  sincos6thpi  15358  pigt3  15360  cos02pilt1  15367  logltb  15390  rpabscxpbnd  15456  sgmf  15502  1sgm2ppw  15511  lgsdir2lem2  15550  lgsdir2lem3  15551  ex-fl  15735  ex-exp  15737  bdceqi  15853  bdcriota  15893  bdsepnfALT  15899  bdbm1.3ii  15901  bj-d0clsepcl  15935  nninfsellemeqinf  16027