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  6894  subf  7010  negne0i  7082  negdii  7091  neg1ap0  7804  halflt1  7919  nn0ssz  8039  zeo  8119  numlt  8162  numltc  8163  uzf  8252  indstr  8312  ixxf  8537  iooval2  8554  ioof  8610  unirnioo  8612  fzval2  8647  fzf  8648  fz10  8680  fzpreddisj  8703  4fvwrd4  8767  fzof  8771  bdceqi  9298  bdcriota  9338  bdsepnfALT  9344  bdbm1.3ii  9346  bj-d0clsepcl  9384