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  627  olc  632  orc  633  dn1dc  867  3ori  1195  mptxor  1315  mpgbi  1341  dveeq2  1696  dveeq2or  1697  sbequilem  1719  nfsb  1822  sbco  1842  sbcocom  1844  elsb3  1852  elsb4  1853  hbsbd  1858  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  eqcomi  2044  eqtri  2060  eleqtri  2112  neii  2208  neeqtri  2232  nesymi  2251  necomi  2290  nemtbir  2294  neli  2299  nrex  2411  rexlimi  2426  isseti  2563  eueq1  2713  euxfr2dc  2726  cdeqri  2750  sseqtri  2977  3sstr3i  2983  pssn2lp  3045  equncomi  3089  unssi  3118  ssini  3160  unabs  3167  inabs  3168  ddifss  3175  inssddif  3178  rgenm  3323  snid  3402  rabrsndc  3438  rintm  3744  breqtri  3787  bm1.3ii  3878  zfnuleu  3881  zfpow  3928  copsexg  3981  uniop  3992  pwundifss  4022  onunisuci  4169  zfun  4171  op1stb  4209  op1stbg  4210  ordtriexmidlem  4245  ordtriexmid  4247  ordtri2orexmid  4248  2ordpr  4249  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  dtruex  4283  ordsoexmid  4286  0elsucexmid  4289  ordtri2or2exmid  4296  tfi  4305  relop  4486  rn0  4588  dmresi  4661  issref  4707  cnvcnv  4773  rescnvcnv  4783  cnvcnvres  4784  cnvsn  4803  cocnvcnv2  4832  cores2  4833  co01  4835  relcoi1  4849  cnviinm  4859  fnopab  5023  mpt0  5026  fnmpti  5027  f1cnvcnv  5100  f1ovi  5165  fmpti  5321  fvsnun2  5361  oprabss  5590  2nd0  5772  f1stres  5786  f2ndres  5787  reldmtpos  5868  dftpos4  5878  tpostpos  5879  tpos0  5889  smo0  5913  frecfnom  5986  oasuc  6044  ssdomg  6258  xpcomf1o  6299  ssfiexmid  6336  diffitest  6344  card0  6368  dmaddpi  6423  dmmulpi  6424  1lt2pi  6438  1lt2nq  6504  gtso  7097  subf  7213  negne0i  7286  negdii  7295  ltapii  7624  neg1ap0  8026  halflt1  8142  nn0ssz  8263  zeo  8343  numlt  8386  numltc  8387  uzf  8476  indstr  8536  ixxf  8767  iooval2  8784  ioof  8840  unirnioo  8842  fzval2  8877  fzf  8878  fz10  8910  fzpreddisj  8933  4fvwrd4  8997  fzof  9001  fldiv4p1lem1div2  9147  sqrt2gt1lt2  9647  fclim  9815  ex-fl  9895  bdceqi  9963  bdcriota  10003  bdsepnfALT  10009  bdbm1.3ii  10011  bj-d0clsepcl  10049