Theorem mpbi 143

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 118	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 7	1 ⊢ 𝜓

Syntax hints:   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.74i  178  pm4.71i  383  pm4.71ri  384  pm5.32i  441  pm3.24  659  olc  664  orc  665  dn1dc  901  3ori  1231  mptxor  1355  mpgbi  1381  dveeq2  1736  dveeq2or  1737  sbequilem  1759  nfsb  1863  sbco  1883  sbcocom  1885  elsb3  1893  elsb4  1894  hbsbd  1899  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  eqcomi  2085  eqtri  2101  eleqtri  2153  neii  2247  neeqtri  2272  nesymi  2291  necomi  2330  nemtbir  2334  neli  2341  nrex  2453  rexlimi  2470  isseti  2607  eueq1  2764  euxfr2dc  2777  cdeqri  2801  sseqtri  3031  3sstr3i  3037  equncomi  3118  unssi  3147  ssini  3189  unabs  3196  inabs  3197  ddifss  3202  inssddif  3205  rgenm  3343  snid  3425  rabrsndc  3460  rintm  3765  breqtri  3808  bm1.3ii  3899  zfnuleu  3902  zfpow  3949  copsexg  3999  uniop  4010  pwundifss  4040  onunisuci  4187  zfun  4189  op1stb  4227  op1stbg  4228  ordtriexmidlem  4263  ordtriexmid  4265  ordtri2orexmid  4266  2ordpr  4267  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  dtruex  4302  ordsoexmid  4305  0elsucexmid  4308  ordtri2or2exmid  4314  tfi  4323  relop  4504  rn0  4606  dmresi  4681  issref  4727  cnvcnv  4793  rescnvcnv  4803  cnvcnvres  4804  cnvsn  4823  cocnvcnv2  4852  cores2  4853  co01  4855  relcoi1  4869  cnviinm  4879  fnopab  5043  mpt0  5046  fnmpti  5047  f1cnvcnv  5120  f1ovi  5185  fmpti  5342  fvsnun2  5382  oprabss  5610  2nd0  5792  f1stres  5806  f2ndres  5807  reldmtpos  5891  dftpos4  5901  tpostpos  5902  tpos0  5912  smo0  5936  frecfnom  6009  oasuc  6067  ssdomg  6281  xpcomf1o  6322  ssfilem  6360  diffitest  6371  card0  6457  dmaddpi  6515  dmmulpi  6516  1lt2pi  6530  1lt2nq  6596  gtso  7190  subf  7310  negne0i  7383  negdii  7392  ltapii  7733  neg1ap0  8148  halflt1  8248  nn0ssz  8369  3halfnz  8444  zeo  8452  numlt  8501  numltc  8502  le9lt10  8503  decle  8510  uzf  8622  indstr  8681  infrenegsupex  8682  ixxf  8921  iooval2  8938  ioof  8994  unirnioo  8996  fzval2  9032  fzf  9033  fz10  9065  fzpreddisj  9088  4fvwrd4  9150  fzof  9154  fldiv4p1lem1div2  9307  sqrt2gt1lt2  9935  fclim  10133  n2dvds1  10312  flodddiv4  10334  gcdf  10364  eucalgf  10437  2prm  10509  ex-fl  10563  bdceqi  10634  bdcriota  10674  bdsepnfALT  10680  bdbm1.3ii  10682  bj-d0clsepcl  10720