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  2809  eueq1  2976  euxfr2dc  2989  cdeqri  3015  sseqtri  3259  3sstr3i  3265  equncomi  3351  unssi  3380  ssini  3428  unabs  3436  inabs  3437  ddifss  3443  inssddif  3446  snid  3698  rabrsndc  3737  rintm  4061  breqtri  4111  bm1.3ii  4208  zfnuleu  4211  zfpow  4263  undifexmid  4281  copsexg  4334  uniop  4346  pwundifss  4380  onunisuci  4527  zfun  4529  op1stb  4573  op1stbg  4574  ordtriexmidlem  4615  ordtriexmid  4617  ordtri2orexmid  4619  2ordpr  4620  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  dtruex  4655  ordsoexmid  4658  0elsucexmid  4661  ordtri2or2exmid  4667  dcextest  4677  tfi  4678  relop  4878  dmxpid  4951  rn0  4986  dmresi  5066  issref  5117  cnvcnv  5187  rescnvcnv  5197  cnvcnvres  5198  cnvsn  5217  cocnvcnv2  5246  cores2  5247  co01  5249  relcoi1  5266  cnviinm  5276  fnopab  5454  mpt0  5457  fnmpti  5458  f1cnvcnv  5550  f1ovi  5620  fmpti  5795  fvsnun2  5847  oprabss  6102  relmptopab  6219  2nd0  6303  f1stres  6317  f2ndres  6318  reldmtpos  6414  dftpos4  6424  tpostpos  6425  tpos0  6435  smo0  6459  frecfnom  6562  oasuc  6627  uniixp  6885  ssdomg  6947  xpcomf1o  7004  ssfilem  7057  diffitest  7071  inffiexmid  7093  fiintim  7118  caseinl  7284  caseinr  7285  eninl  7290  eninr  7291  card0  7386  dju1p1e2  7401  pw1on  7437  dmaddpi  7538  dmmulpi  7539  1lt2pi  7553  1lt2nq  7619  suplocsrlempr  8020  gtso  8251  subf  8374  negne0i  8447  negdii  8456  ltapii  8808  sup3exmid  9130  neg1ap0  9245  halflt1  9354  nn0ssz  9490  3halfnz  9570  zeo  9578  numlt  9628  numltc  9629  le9lt10  9630  decle  9637  uzf  9751  indstr  9820  infrenegsupex  9821  xaddf  10072  ixxf  10126  iooval2  10143  ioof  10199  unirnioo  10201  fzval2  10239  fzf  10240  fz10  10274  fzpreddisj  10299  4fvwrd4  10368  fzof  10372  fldiv4p1lem1div2  10558  fldiv4lem1div2  10560  xnn0nnen  10692  sqrt2gt1lt2  11603  infxrnegsupex  11817  fclim  11848  fsumrelem  12025  arisum2  12053  geo2sum2  12069  0.999...  12075  ege2le3  12225  sin0  12283  ef01bndlem  12310  cos2bnd  12314  cos01gt0  12317  sincos2sgn  12320  sin4lt0  12321  egt2lt3  12334  n2dvds1  12466  flodddiv4  12490  0bits  12513  gcdf  12536  nninfct  12605  eucalgf  12620  2prm  12692  dfphi2  12785  pockthi  12924  karatsuba  12996  znnen  13012  ennnfonelem1  13021  qnnen  13045  ctiunct  13054  ssnnctlemct  13060  structcnvcnv  13091  structfn  13094  relelbasov  13138  xpsff1o  13425  rmodislmod  14358  cnfld0  14578  cnfld1  14579  eltpsi  14758  unitg  14779  epttop  14807  txuni2  14973  retopon  15243  cnfldtopon  15257  dedekindicclemicc  15349  reldvg  15396  dvrecap  15430  dvef  15444  plyrecj  15480  sinhalfpilem  15508  coseq00topi  15552  coseq0negpitopi  15553  sincos4thpi  15557  sincos6thpi  15559  pigt3  15561  cos02pilt1  15568  logltb  15591  rpabscxpbnd  15657  sgmf  15703  1sgm2ppw  15712  lgsdir2lem2  15751  lgsdir2lem3  15752  ex-fl  16271  ex-exp  16273  bdceqi  16388  bdcriota  16428  bdsepnfALT  16434  bdbm1.3ii  16436  bj-d0clsepcl  16470  nninfsellemeqinf  16568