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  697  olc  715  orc  716  dcnn  852  dn1dc  965  3ori  1315  mptxor  1446  mpgbi  1478  dveeq2  1841  dveeq2or  1842  sbequilem  1864  nfsb  1977  sbco  1999  sbcocom  2001  hbsbd  2013  dvelimALT  2041  dvelimfv  2042  dvelimor  2049  hbe1a  2054  elsb1  2187  elsb2  2188  eqcomi  2213  eqtri  2230  eleqtri  2284  neii  2382  neeqtri  2407  nesymi  2426  necomi  2465  nemtbir  2469  neli  2477  nrex  2602  rexlimi  2621  isseti  2788  eueq1  2955  euxfr2dc  2968  cdeqri  2994  sseqtri  3238  3sstr3i  3244  equncomi  3330  unssi  3359  ssini  3407  unabs  3415  inabs  3416  ddifss  3422  inssddif  3425  snid  3677  rabrsndc  3714  rintm  4037  breqtri  4087  bm1.3ii  4184  zfnuleu  4187  zfpow  4238  undifexmid  4256  copsexg  4309  uniop  4321  pwundifss  4353  onunisuci  4500  zfun  4502  op1stb  4546  op1stbg  4547  ordtriexmidlem  4588  ordtriexmid  4590  ordtri2orexmid  4592  2ordpr  4593  ontr2exmid  4594  onsucsssucexmid  4596  onsucelsucexmid  4599  dtruex  4628  ordsoexmid  4631  0elsucexmid  4634  ordtri2or2exmid  4640  dcextest  4650  tfi  4651  relop  4849  dmxpid  4921  rn0  4956  dmresi  5036  issref  5087  cnvcnv  5157  rescnvcnv  5167  cnvcnvres  5168  cnvsn  5187  cocnvcnv2  5216  cores2  5217  co01  5219  relcoi1  5236  cnviinm  5246  fnopab  5424  mpt0  5427  fnmpti  5428  f1cnvcnv  5518  f1ovi  5588  fmpti  5760  fvsnun2  5810  oprabss  6061  2nd0  6261  f1stres  6275  f2ndres  6276  reldmtpos  6369  dftpos4  6379  tpostpos  6380  tpos0  6390  smo0  6414  frecfnom  6517  oasuc  6580  uniixp  6838  ssdomg  6900  xpcomf1o  6952  ssfilem  7005  diffitest  7017  inffiexmid  7036  fiintim  7061  caseinl  7226  caseinr  7227  eninl  7232  eninr  7233  card0  7328  dju1p1e2  7343  pw1on  7379  dmaddpi  7480  dmmulpi  7481  1lt2pi  7495  1lt2nq  7561  suplocsrlempr  7962  gtso  8193  subf  8316  negne0i  8389  negdii  8398  ltapii  8750  sup3exmid  9072  neg1ap0  9187  halflt1  9296  nn0ssz  9432  3halfnz  9512  zeo  9520  numlt  9570  numltc  9571  le9lt10  9572  decle  9579  uzf  9693  indstr  9756  infrenegsupex  9757  xaddf  10008  ixxf  10062  iooval2  10079  ioof  10135  unirnioo  10137  fzval2  10175  fzf  10176  fz10  10210  fzpreddisj  10235  4fvwrd4  10304  fzof  10308  fldiv4p1lem1div2  10492  fldiv4lem1div2  10494  xnn0nnen  10626  sqrt2gt1lt2  11526  infxrnegsupex  11740  fclim  11771  fsumrelem  11948  arisum2  11976  geo2sum2  11992  0.999...  11998  ege2le3  12148  sin0  12206  ef01bndlem  12233  cos2bnd  12237  cos01gt0  12240  sincos2sgn  12243  sin4lt0  12244  egt2lt3  12257  n2dvds1  12389  flodddiv4  12413  0bits  12436  gcdf  12459  nninfct  12528  eucalgf  12543  2prm  12615  dfphi2  12708  pockthi  12847  karatsuba  12919  znnen  12935  ennnfonelem1  12944  qnnen  12968  ctiunct  12977  ssnnctlemct  12983  structcnvcnv  13014  structfn  13017  relelbasov  13061  xpsff1o  13348  rmodislmod  14280  cnfld0  14500  cnfld1  14501  eltpsi  14680  unitg  14701  epttop  14729  txuni2  14895  retopon  15165  cnfldtopon  15179  dedekindicclemicc  15271  reldvg  15318  dvrecap  15352  dvef  15366  plyrecj  15402  sinhalfpilem  15430  coseq00topi  15474  coseq0negpitopi  15475  sincos4thpi  15479  sincos6thpi  15481  pigt3  15483  cos02pilt1  15490  logltb  15513  rpabscxpbnd  15579  sgmf  15625  1sgm2ppw  15634  lgsdir2lem2  15673  lgsdir2lem3  15674  ex-fl  15999  ex-exp  16001  bdceqi  16116  bdcriota  16156  bdsepnfALT  16162  bdbm1.3ii  16164  bj-d0clsepcl  16198  nninfsellemeqinf  16293