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  3217  3sstr3i  3223  equncomi  3309  unssi  3338  ssini  3386  unabs  3394  inabs  3395  ddifss  3401  inssddif  3404  snid  3653  rabrsndc  3690  rintm  4009  breqtri  4058  bm1.3ii  4154  zfnuleu  4157  zfpow  4208  undifexmid  4226  copsexg  4277  uniop  4288  pwundifss  4320  onunisuci  4467  zfun  4469  op1stb  4513  op1stbg  4514  ordtriexmidlem  4555  ordtriexmid  4557  ordtri2orexmid  4559  2ordpr  4560  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmid  4566  dtruex  4595  ordsoexmid  4598  0elsucexmid  4601  ordtri2or2exmid  4607  dcextest  4617  tfi  4618  relop  4816  dmxpid  4887  rn0  4922  dmresi  5001  issref  5052  cnvcnv  5122  rescnvcnv  5132  cnvcnvres  5133  cnvsn  5152  cocnvcnv2  5181  cores2  5182  co01  5184  relcoi1  5201  cnviinm  5211  fnopab  5382  mpt0  5385  fnmpti  5386  f1cnvcnv  5474  f1ovi  5543  fmpti  5714  fvsnun2  5760  oprabss  6008  2nd0  6203  f1stres  6217  f2ndres  6218  reldmtpos  6311  dftpos4  6321  tpostpos  6322  tpos0  6332  smo0  6356  frecfnom  6459  oasuc  6522  uniixp  6780  ssdomg  6837  xpcomf1o  6884  ssfilem  6936  diffitest  6948  inffiexmid  6967  fiintim  6992  caseinl  7157  caseinr  7158  eninl  7163  eninr  7164  card0  7255  dju1p1e2  7264  pw1on  7293  dmaddpi  7392  dmmulpi  7393  1lt2pi  7407  1lt2nq  7473  suplocsrlempr  7874  gtso  8105  subf  8228  negne0i  8301  negdii  8310  ltapii  8662  sup3exmid  8984  neg1ap0  9099  halflt1  9208  nn0ssz  9344  3halfnz  9423  zeo  9431  numlt  9481  numltc  9482  le9lt10  9483  decle  9490  uzf  9604  indstr  9667  infrenegsupex  9668  xaddf  9919  ixxf  9973  iooval2  9990  ioof  10046  unirnioo  10048  fzval2  10086  fzf  10087  fz10  10121  fzpreddisj  10146  4fvwrd4  10215  fzof  10219  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  xnn0nnen  10529  sqrt2gt1lt2  11214  infxrnegsupex  11428  fclim  11459  fsumrelem  11636  arisum2  11664  geo2sum2  11680  0.999...  11686  ege2le3  11836  sin0  11894  ef01bndlem  11921  cos2bnd  11925  cos01gt0  11928  sincos2sgn  11931  sin4lt0  11932  egt2lt3  11945  n2dvds1  12077  flodddiv4  12101  gcdf  12139  nninfct  12208  eucalgf  12223  2prm  12295  dfphi2  12388  pockthi  12527  karatsuba  12599  znnen  12615  ennnfonelem1  12624  qnnen  12648  ctiunct  12657  ssnnctlemct  12663  structcnvcnv  12694  structfn  12697  relelbasov  12740  xpsff1o  12992  rmodislmod  13907  cnfld0  14127  cnfld1  14128  eltpsi  14277  unitg  14298  epttop  14326  txuni2  14492  retopon  14762  cnfldtopon  14776  dedekindicclemicc  14868  reldvg  14915  dvrecap  14949  dvef  14963  plyrecj  14999  sinhalfpilem  15027  coseq00topi  15071  coseq0negpitopi  15072  sincos4thpi  15076  sincos6thpi  15078  pigt3  15080  cos02pilt1  15087  logltb  15110  rpabscxpbnd  15176  sgmf  15222  1sgm2ppw  15231  lgsdir2lem2  15270  lgsdir2lem3  15271  ex-fl  15371  ex-exp  15373  bdceqi  15489  bdcriota  15529  bdsepnfALT  15535  bdbm1.3ii  15537  bj-d0clsepcl  15571  nninfsellemeqinf  15660