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  442  pm3.24  660  olc  665  orc  666  dn1dc  902  3ori  1232  mptxor  1356  mpgbi  1382  dveeq2  1738  dveeq2or  1739  sbequilem  1761  nfsb  1865  sbco  1885  sbcocom  1887  elsb3  1895  elsb4  1896  hbsbd  1901  dvelimALT  1929  dvelimfv  1930  dvelimor  1937  eqcomi  2087  eqtri  2103  eleqtri  2157  neii  2251  neeqtri  2276  nesymi  2295  necomi  2334  nemtbir  2338  neli  2346  nrex  2458  rexlimi  2475  isseti  2616  eueq1  2774  euxfr2dc  2787  cdeqri  2811  sseqtri  3041  3sstr3i  3047  equncomi  3129  unssi  3158  ssini  3206  unabs  3213  inabs  3214  ddifss  3219  inssddif  3222  rgenm  3361  snid  3444  rabrsndc  3479  rintm  3786  breqtri  3829  bm1.3ii  3920  zfnuleu  3923  zfpow  3970  undifexmid  3985  copsexg  4028  uniop  4039  pwundifss  4069  onunisuci  4216  zfun  4218  op1stb  4256  op1stbg  4257  ordtriexmidlem  4292  ordtriexmid  4294  ordtri2orexmid  4295  2ordpr  4296  ontr2exmid  4297  onsucsssucexmid  4299  onsucelsucexmid  4302  dtruex  4331  ordsoexmid  4334  0elsucexmid  4337  ordtri2or2exmid  4343  tfi  4352  relop  4535  rn0  4637  dmresi  4712  issref  4758  cnvcnv  4824  rescnvcnv  4834  cnvcnvres  4835  cnvsn  4854  cocnvcnv2  4883  cores2  4884  co01  4886  relcoi1  4900  cnviinm  4910  fnopab  5075  mpt0  5078  fnmpti  5079  f1cnvcnv  5152  f1ovi  5217  fmpti  5374  fvsnun2  5414  oprabss  5642  2nd0  5824  f1stres  5838  f2ndres  5839  reldmtpos  5923  dftpos4  5933  tpostpos  5934  tpos0  5944  smo0  5968  frecfnom  6071  oasuc  6129  ssdomg  6347  xpcomf1o  6391  ssfilem  6432  diffitest  6444  inffiexmid  6458  card0  6552  dmaddpi  6613  dmmulpi  6614  1lt2pi  6628  1lt2nq  6694  gtso  7293  subf  7413  negne0i  7486  negdii  7495  ltapii  7836  neg1ap0  8251  halflt1  8351  nn0ssz  8486  3halfnz  8561  zeo  8569  numlt  8618  numltc  8619  le9lt10  8620  decle  8627  uzf  8739  indstr  8798  infrenegsupex  8799  ixxf  9033  iooval2  9050  ioof  9106  unirnioo  9108  fzval2  9144  fzf  9145  fz10  9177  fzpreddisj  9200  4fvwrd4  9263  fzof  9267  fldiv4p1lem1div2  9423  sqrt2gt1lt2  10120  fclim  10318  n2dvds1  10503  flodddiv4  10525  gcdf  10555  eucalgf  10628  2prm  10700  dfphi2  10787  znnen  10802  ex-fl  10807  bdceqi  10885  bdcriota  10925  bdsepnfALT  10931  bdbm1.3ii  10933  bj-d0clsepcl  10971