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  6874  subf  6990  negne0i  7062  negdii  7071  neg1ap0  7784  halflt1  7899  nn0ssz  8019  zeo  8099  numlt  8142  numltc  8143  uzf  8232  indstr  8292  ixxf  8517  iooval2  8534  ioof  8590  unirnioo  8592  fzval2  8627  fzf  8628  fz10  8660  fzpreddisj  8683  4fvwrd4  8747  fzof  8751  bdceqi  9278  bdcriota  9318  bdsepnfALT  9323  bdbm1.3ii  9325  bj-d0clsepcl  9360