Theorem mpbi 133

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 113	. 2 ⊢ (φ → ψ)
4	1, 3	ax-mp 7	1 ⊢ ψ

Syntax hints:   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.74i  169  pm4.71i  371  pm4.71ri  372  pm5.32i  427  pm3.24  626  olc  631  orc  632  dn1dc  866  3ori  1194  mpto2  1312  mtp-xor  1313  mpgbi  1338  dveeq2  1693  dveeq2or  1694  sbequilem  1716  nfsb  1819  sbco  1839  sbcocom  1841  elsb3  1849  elsb4  1850  hbsbd  1855  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  eqcomi  2041  eqtri  2057  eleqtri  2109  neii  2205  neeqtri  2226  nesymi  2245  necomi  2284  nemtbir  2288  neli  2293  nrex  2405  rexlimi  2420  isseti  2557  eueq1  2707  euxfr2dc  2720  cdeqri  2744  sseqtri  2971  3sstr3i  2977  pssn2lp  3039  equncomi  3083  unssi  3112  ssini  3154  unabs  3161  inabs  3162  ddifss  3169  inssddif  3172  rgenm  3317  snid  3394  rabrsndc  3429  rintm  3735  breqtri  3778  bm1.3ii  3869  zfnuleu  3872  zfpow  3919  copsexg  3972  uniop  3983  pwundifss  4013  onunisuci  4135  zfun  4137  op1stb  4175  op1stbg  4176  ordtriexmidlem  4208  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  onsucelsucexmidlem  4214  onsucelsucexmid  4215  dtruex  4237  ordsoexmid  4240  tfi  4248  relop  4429  rn0  4531  dmresi  4604  issref  4650  cnvcnv  4716  rescnvcnv  4726  cnvcnvres  4727  cnvsn  4746  cocnvcnv2  4775  cores2  4776  co01  4778  relcoi1  4792  cnviinm  4802  fnopab  4966  mpt0  4969  fnmpti  4970  f1cnvcnv  5043  f1ovi  5108  fmpti  5264  fvsnun2  5304  oprabss  5532  2nd0  5714  f1stres  5728  f2ndres  5729  reldmtpos  5809  dftpos4  5819  tpostpos  5820  tpos0  5830  smo0  5854  frecfnom  5925  oasuc  5983  ssdomg  6194  xpcomf1o  6235  ssfiexmid  6254  dmaddpi  6309  dmmulpi  6310  1lt2pi  6324  1lt2nq  6389  gtso  6854  subf  6970  negne0i  7042  negdii  7051  neg1ap0  7764  halflt1  7879  nn0ssz  7999  zeo  8079  numlt  8122  numltc  8123  uzf  8212  indstr  8272  ixxf  8497  iooval2  8514  ioof  8570  unirnioo  8572  fzval2  8607  fzf  8608  fz10  8640  fzpreddisj  8663  4fvwrd4  8727  fzof  8731  bdceqi  9232  bdcriota  9272  bdsepnfALT  9277  bdbm1.3ii  9279  bj-d0clsepcl  9314