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  617  pm3.24  700  olc  718  orc  719  dcnn  855  dn1dc  968  3ori  1336  mptxor  1468  mpgbi  1500  dveeq2  1863  dveeq2or  1864  sbequilem  1886  nfsb  1999  sbco  2021  sbcocom  2023  hbsbd  2035  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  hbe1a  2076  elsb1  2209  elsb2  2210  eqcomi  2235  eqtri  2252  eleqtri  2306  neii  2404  neeqtri  2429  nesymi  2448  necomi  2487  nemtbir  2491  neli  2499  nrex  2624  rexlimi  2643  isseti  2811  eueq1  2978  euxfr2dc  2991  cdeqri  3017  sseqtri  3261  3sstr3i  3267  equncomi  3353  unssi  3382  ssini  3430  unabs  3438  inabs  3439  ddifss  3445  inssddif  3448  snid  3700  rabrsndc  3739  rintm  4063  breqtri  4113  bm1.3ii  4210  zfnuleu  4213  zfpow  4265  undifexmid  4283  copsexg  4336  uniop  4348  pwundifss  4382  onunisuci  4529  zfun  4531  op1stb  4575  op1stbg  4576  ordtriexmidlem  4617  ordtriexmid  4619  ordtri2orexmid  4621  2ordpr  4622  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  dtruex  4657  ordsoexmid  4660  0elsucexmid  4663  ordtri2or2exmid  4669  dcextest  4679  tfi  4680  relop  4880  dmxpid  4953  rn0  4988  dmresi  5068  issref  5119  cnvcnv  5189  rescnvcnv  5199  cnvcnvres  5200  cnvsn  5219  cocnvcnv2  5248  cores2  5249  co01  5251  relcoi1  5268  cnviinm  5278  fnopab  5457  mpt0  5460  fnmpti  5461  f1cnvcnv  5553  f1ovi  5624  fmpti  5799  fvsnun2  5852  oprabss  6107  relmptopab  6224  2nd0  6308  f1stres  6322  f2ndres  6323  reldmtpos  6419  dftpos4  6429  tpostpos  6430  tpos0  6440  smo0  6464  frecfnom  6567  oasuc  6632  uniixp  6890  ssdomg  6952  xpcomf1o  7009  ssfilem  7062  diffitest  7076  inffiexmid  7098  fiintim  7123  caseinl  7290  caseinr  7291  eninl  7296  eninr  7297  card0  7392  dju1p1e2  7408  pw1on  7444  dmaddpi  7545  dmmulpi  7546  1lt2pi  7560  1lt2nq  7626  suplocsrlempr  8027  gtso  8258  subf  8381  negne0i  8454  negdii  8463  ltapii  8815  sup3exmid  9137  neg1ap0  9252  halflt1  9361  nn0ssz  9497  3halfnz  9577  zeo  9585  numlt  9635  numltc  9636  le9lt10  9637  decle  9644  uzf  9758  indstr  9827  infrenegsupex  9828  xaddf  10079  ixxf  10133  iooval2  10150  ioof  10206  unirnioo  10208  fzval2  10246  fzf  10247  fz10  10281  fzpreddisj  10306  4fvwrd4  10375  fzof  10379  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  xnn0nnen  10700  sqrt2gt1lt2  11611  infxrnegsupex  11825  fclim  11856  fsumrelem  12034  arisum2  12062  geo2sum2  12078  0.999...  12084  ege2le3  12234  sin0  12292  ef01bndlem  12319  cos2bnd  12323  cos01gt0  12326  sincos2sgn  12329  sin4lt0  12330  egt2lt3  12343  n2dvds1  12475  flodddiv4  12499  0bits  12522  gcdf  12545  nninfct  12614  eucalgf  12629  2prm  12701  dfphi2  12794  pockthi  12933  karatsuba  13005  znnen  13021  ennnfonelem1  13030  qnnen  13054  ctiunct  13063  ssnnctlemct  13069  structcnvcnv  13100  structfn  13103  relelbasov  13147  xpsff1o  13434  rmodislmod  14368  cnfld0  14588  cnfld1  14589  eltpsi  14768  unitg  14789  epttop  14817  txuni2  14983  retopon  15253  cnfldtopon  15267  dedekindicclemicc  15359  reldvg  15406  dvrecap  15440  dvef  15454  plyrecj  15490  sinhalfpilem  15518  coseq00topi  15562  coseq0negpitopi  15563  sincos4thpi  15567  sincos6thpi  15569  pigt3  15571  cos02pilt1  15578  logltb  15601  rpabscxpbnd  15667  sgmf  15713  1sgm2ppw  15722  lgsdir2lem2  15761  lgsdir2lem3  15762  ex-fl  16338  ex-exp  16340  bdceqi  16459  bdcriota  16499  bdsepnfALT  16505  bdbm1.3ii  16507  bj-d0clsepcl  16541  nninfsellemeqinf  16639