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  615  pm3.24  698  olc  716  orc  717  dcnn  853  dn1dc  966  3ori  1334  mptxor  1466  mpgbi  1498  dveeq2  1861  dveeq2or  1862  sbequilem  1884  nfsb  1997  sbco  2019  sbcocom  2021  hbsbd  2033  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  hbe1a  2074  elsb1  2207  elsb2  2208  eqcomi  2233  eqtri  2250  eleqtri  2304  neii  2402  neeqtri  2427  nesymi  2446  necomi  2485  nemtbir  2489  neli  2497  nrex  2622  rexlimi  2641  isseti  2808  eueq1  2975  euxfr2dc  2988  cdeqri  3014  sseqtri  3258  3sstr3i  3264  equncomi  3350  unssi  3379  ssini  3427  unabs  3435  inabs  3436  ddifss  3442  inssddif  3445  snid  3697  rabrsndc  3734  rintm  4058  breqtri  4108  bm1.3ii  4205  zfnuleu  4208  zfpow  4259  undifexmid  4277  copsexg  4330  uniop  4342  pwundifss  4376  onunisuci  4523  zfun  4525  op1stb  4569  op1stbg  4570  ordtriexmidlem  4611  ordtriexmid  4613  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  dtruex  4651  ordsoexmid  4654  0elsucexmid  4657  ordtri2or2exmid  4663  dcextest  4673  tfi  4674  relop  4872  dmxpid  4945  rn0  4980  dmresi  5060  issref  5111  cnvcnv  5181  rescnvcnv  5191  cnvcnvres  5192  cnvsn  5211  cocnvcnv2  5240  cores2  5241  co01  5243  relcoi1  5260  cnviinm  5270  fnopab  5448  mpt0  5451  fnmpti  5452  f1cnvcnv  5544  f1ovi  5614  fmpti  5789  fvsnun2  5841  oprabss  6096  relmptopab  6213  2nd0  6297  f1stres  6311  f2ndres  6312  reldmtpos  6405  dftpos4  6415  tpostpos  6416  tpos0  6426  smo0  6450  frecfnom  6553  oasuc  6618  uniixp  6876  ssdomg  6938  xpcomf1o  6992  ssfilem  7045  diffitest  7057  inffiexmid  7076  fiintim  7101  caseinl  7266  caseinr  7267  eninl  7272  eninr  7273  card0  7368  dju1p1e2  7383  pw1on  7419  dmaddpi  7520  dmmulpi  7521  1lt2pi  7535  1lt2nq  7601  suplocsrlempr  8002  gtso  8233  subf  8356  negne0i  8429  negdii  8438  ltapii  8790  sup3exmid  9112  neg1ap0  9227  halflt1  9336  nn0ssz  9472  3halfnz  9552  zeo  9560  numlt  9610  numltc  9611  le9lt10  9612  decle  9619  uzf  9733  indstr  9796  infrenegsupex  9797  xaddf  10048  ixxf  10102  iooval2  10119  ioof  10175  unirnioo  10177  fzval2  10215  fzf  10216  fz10  10250  fzpreddisj  10275  4fvwrd4  10344  fzof  10348  fldiv4p1lem1div2  10533  fldiv4lem1div2  10535  xnn0nnen  10667  sqrt2gt1lt2  11568  infxrnegsupex  11782  fclim  11813  fsumrelem  11990  arisum2  12018  geo2sum2  12034  0.999...  12040  ege2le3  12190  sin0  12248  ef01bndlem  12275  cos2bnd  12279  cos01gt0  12282  sincos2sgn  12285  sin4lt0  12286  egt2lt3  12299  n2dvds1  12431  flodddiv4  12455  0bits  12478  gcdf  12501  nninfct  12570  eucalgf  12585  2prm  12657  dfphi2  12750  pockthi  12889  karatsuba  12961  znnen  12977  ennnfonelem1  12986  qnnen  13010  ctiunct  13019  ssnnctlemct  13025  structcnvcnv  13056  structfn  13059  relelbasov  13103  xpsff1o  13390  rmodislmod  14323  cnfld0  14543  cnfld1  14544  eltpsi  14723  unitg  14744  epttop  14772  txuni2  14938  retopon  15208  cnfldtopon  15222  dedekindicclemicc  15314  reldvg  15361  dvrecap  15395  dvef  15409  plyrecj  15445  sinhalfpilem  15473  coseq00topi  15517  coseq0negpitopi  15518  sincos4thpi  15522  sincos6thpi  15524  pigt3  15526  cos02pilt1  15533  logltb  15556  rpabscxpbnd  15622  sgmf  15668  1sgm2ppw  15677  lgsdir2lem2  15716  lgsdir2lem3  15717  ex-fl  16113  ex-exp  16115  bdceqi  16230  bdcriota  16270  bdsepnfALT  16276  bdbm1.3ii  16278  bj-d0clsepcl  16312  nninfsellemeqinf  16412