Theorem mpbi 137

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 117	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 7	1 ⊢ 𝜓

Syntax hints:   ↔ wb 102

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

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  pm5.74i  173  pm4.71i  377  pm4.71ri  378  pm5.32i  435  pm3.24  637  olc  642  orc  643  dn1dc  878  3ori  1206  mptxor  1331  mpgbi  1357  dveeq2  1712  dveeq2or  1713  sbequilem  1735  nfsb  1838  sbco  1858  sbcocom  1860  elsb3  1868  elsb4  1869  hbsbd  1874  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  eqcomi  2060  eqtri  2076  eleqtri  2128  neii  2222  neeqtri  2247  nesymi  2266  necomi  2305  nemtbir  2309  neli  2316  nrex  2428  rexlimi  2443  isseti  2580  eueq1  2735  euxfr2dc  2748  cdeqri  2772  sseqtri  3004  3sstr3i  3010  pssn2lp  3072  equncomi  3116  unssi  3145  ssini  3187  unabs  3194  inabs  3195  ddifss  3202  inssddif  3205  rgenm  3350  snid  3429  rabrsndc  3465  rintm  3771  breqtri  3814  bm1.3ii  3905  zfnuleu  3908  zfpow  3955  copsexg  4008  uniop  4019  pwundifss  4049  onunisuci  4196  zfun  4198  op1stb  4236  op1stbg  4237  ordtriexmidlem  4272  ordtriexmid  4274  ordtri2orexmid  4275  2ordpr  4276  ontr2exmid  4277  onsucsssucexmid  4279  onsucelsucexmid  4282  dtruex  4310  ordsoexmid  4313  0elsucexmid  4316  ordtri2or2exmid  4323  tfi  4332  relop  4513  rn0  4615  dmresi  4688  issref  4734  cnvcnv  4800  rescnvcnv  4810  cnvcnvres  4811  cnvsn  4830  cocnvcnv2  4859  cores2  4860  co01  4862  relcoi1  4876  cnviinm  4886  fnopab  5050  mpt0  5053  fnmpti  5054  f1cnvcnv  5127  f1ovi  5192  fmpti  5348  fvsnun2  5388  oprabss  5617  2nd0  5799  f1stres  5813  f2ndres  5814  reldmtpos  5898  dftpos4  5908  tpostpos  5909  tpos0  5919  smo0  5943  frecfnom  6016  oasuc  6074  ssdomg  6288  xpcomf1o  6329  ssfiexmid  6366  diffitest  6374  card0  6425  dmaddpi  6480  dmmulpi  6481  1lt2pi  6495  1lt2nq  6561  gtso  7155  subf  7275  negne0i  7348  negdii  7357  ltapii  7697  neg1ap0  8098  halflt1  8198  nn0ssz  8319  3halfnz  8394  zeo  8401  numlt  8450  numltc  8451  le9lt10  8452  decle  8459  uzf  8571  indstr  8631  ixxf  8867  iooval2  8884  ioof  8940  unirnioo  8942  fzval2  8978  fzf  8979  fz10  9011  fzpreddisj  9034  4fvwrd4  9098  fzof  9102  fldiv4p1lem1div2  9249  sqrt2gt1lt2  9868  fclim  10038  n2dvds1  10216  ex-fl  10251  bdceqi  10322  bdcriota  10362  bdsepnfALT  10368  bdbm1.3ii  10370  bj-d0clsepcl  10408