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  430  pm3.24  614  olc  619  orc  620  dn1dc  853  3ori  1179  mpto2  1296  mtp-xor  1297  mpgbi  1317  dveeq2  1674  dveeq2or  1675  sbequilem  1697  nfsb  1800  sbco  1820  sbcocom  1822  elsb3  1830  elsb4  1831  hbsbd  1836  dvelimALT  1864  dvelimfv  1865  dvelimor  1872  eqcomi  2022  eqtri  2038  eleqtri  2090  neii  2186  neeqtri  2206  nesymi  2225  necomi  2264  nemtbir  2268  neli  2273  nrex  2385  rexlimi  2400  isseti  2537  eueq1  2686  euxfr2dc  2699  cdeqri  2723  sseqtri  2950  3sstr3i  2956  pssn2lp  3018  equncomi  3062  unssi  3091  ssini  3133  unabs  3140  inabs  3141  ddifss  3148  inssddif  3151  rgenm  3298  snid  3373  rabrsndc  3408  rintm  3714  breqtri  3757  bm1.3ii  3848  zfnuleu  3851  zfpow  3898  copsexg  3951  uniop  3962  pwundifss  3992  onunisuci  4115  zfun  4117  op1stb  4155  op1stbg  4156  ordtriexmidlem  4188  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmidlem  4194  onsucelsucexmid  4195  dtruex  4217  ordsoexmid  4220  tfi  4228  relop  4409  rn0  4511  dmresi  4584  issref  4630  cnvcnv  4696  rescnvcnv  4706  cnvcnvres  4707  cnvsn  4726  cocnvcnv2  4755  cores2  4756  co01  4758  relcoi1  4772  cnviinm  4782  fnopab  4945  mpt0  4948  fnmpti  4949  f1cnvcnv  5021  f1ovi  5086  fmpti  5242  fvsnun2  5282  oprabss  5509  2nd0  5691  f1stres  5705  f2ndres  5706  reldmtpos  5786  dftpos4  5796  tpostpos  5797  tpos0  5807  smo0  5831  frecfnom  5897  oasuc  5955  dmaddpi  6179  dmmulpi  6180  1lt2pi  6194  1lt2nq  6258  gtso  6691  subf  6800  negne0i  6872  negdii  6881  bdceqi  7209  bdcriota  7249  bdsepnfALT  7254  bdbm1.3ii  7256  bj-d0clsepcl  7287