Theorem mpbi 145

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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.74i  180  pm4.71i  395  pm4.71ri  396  pm5.32i  458  biadanii  621  pm3.24  705  olc  723  orc  724  dcnn  860  dn1dc  973  3ori  1341  mptxor  1473  mpgbi  1505  dveeq2  1868  dveeq2or  1869  sbequilem  1891  nfsb  2006  sbco  2028  sbcocom  2030  hbsbd  2042  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  hbe1a  2083  elsb1  2216  elsb2  2217  eqcomi  2242  eqtri  2259  eleqtri  2313  neii  2422  neeqtri  2447  nesymi  2466  necomi  2505  nemtbir  2509  neli  2517  nrex  2642  rexlimi  2661  isseti  2830  eueq1  2998  euxfr2dc  3011  cdeqri  3037  sseqtri  3282  3sstr3i  3288  equncomi  3375  unssi  3404  ssini  3454  unabs  3462  inabs  3463  ddifss  3469  inssddif  3472  snid  3739  rabrsndc  3778  rintm  4103  breqtri  4153  bm1.3ii  4252  zfnuleu  4255  zfpow  4310  undifexmid  4328  copsexg  4382  uniop  4394  pwundifss  4428  onunisuci  4575  zfun  4577  op1stb  4622  op1stbg  4623  ordtriexmidlem  4664  ordtriexmid  4666  ordtri2orexmid  4668  2ordpr  4669  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  dtruex  4704  ordsoexmid  4707  0elsucexmid  4710  ordtri2or2exmid  4716  dcextest  4726  tfi  4727  relop  4928  dmxpid  5001  rn0  5036  dmresi  5116  issref  5168  cnvcnv  5238  rescnvcnv  5248  cnvcnvres  5249  cnvsn  5268  cocnvcnv2  5297  cores2  5298  co01  5300  relcoi1  5317  cnviinm  5327  fnopab  5506  mpt0  5509  fnmpti  5510  f1cnvcnv  5607  f1ovi  5678  fmpti  5854  fvsnun2  5907  rinvf1o  6029  oprabss  6168  relmptopab  6285  2nd0  6373  f1stres  6387  f2ndres  6388  reldmtpos  6518  dftpos4  6528  tpostpos  6529  tpos0  6539  smo0  6563  frecfnom  6666  oasuc  6731  uniixp  6997  ssdomg  7059  xpcomf1o  7117  ssfilem  7171  diffitest  7185  inffiexmid  7207  fiintim  7232  caseinl  7425  caseinr  7426  eninl  7431  eninr  7432  card0  7527  dju1p1e2  7543  pw1on  7579  dmaddpi  7686  dmmulpi  7687  1lt2pi  7701  1lt2nq  7767  suplocsrlempr  8168  gtso  8398  subf  8522  negne0i  8595  negdii  8604  ltapii  8957  sup3exmid  9281  neg1ap0  9396  halflt1  9505  nn0ssz  9645  3halfnz  9726  zeo  9734  numlt  9784  numltc  9785  le9lt10  9786  decle  9793  uzf  9907  indstr  9976  infrenegsupex  9977  xaddf  10229  ixxf  10283  iooval2  10300  ioof  10356  unirnioo  10358  fzval2  10397  fzf  10398  fz10  10433  fz00m1  10434  fzpreddisj  10461  4fvwrd4  10530  fzof  10534  fldiv4p1lem1div2  10723  fldiv4lem1div2  10725  xnn0nnen  10857  hashfibc  11266  sqrt2gt1lt2  11798  infxrnegsupex  12012  fclim  12043  fsumrelem  12221  arisum2  12249  geo2sum2  12265  0.999...  12271  ege2le3  12421  sin0  12479  ef01bndlem  12506  cos2bnd  12510  cos01gt0  12513  sincos2sgn  12516  sin4lt0  12517  egt2lt3  12530  n2dvds1  12662  flodddiv4  12686  0bits  12709  gcdf  12732  nninfct  12801  eucalgf  12816  2prm  12888  dfphi2  12981  pockthi  13120  karatsuba  13192  ballotfilem2  13211  ballotfilem4  13224  ballotfilem5  13225  ballotfilemi1  13228  ballotfilem7  13262  ballotfilemth  13264  znnen  13272  ennnfonelem1  13281  qnnen  13305  ctiunct  13314  ssnnctlemct  13320  structcnvcnv  13351  structfn  13354  relelbasov  13399  xpsff1o  13653  rmodislmod  14671  cnfld0  14891  cnfld1  14892  eltpsi  15125  unitg  15146  epttop  15174  txuni2  15340  retopon  15610  cnfldtopon  15624  dedekindicclemicc  15716  reldvg  15763  dvrecap  15797  dvef  15811  plyrecj  15847  sinhalfpilem  15875  coseq00topi  15919  coseq0negpitopi  15920  sincos4thpi  15924  sincos6thpi  15926  pigt3  15928  cos02pilt1  15935  logltb  15958  rpabscxpbnd  16025  log2ublog2  16069  birthdaylog2  16073  sgmf  16083  1sgm2ppw  16092  lgsdir2lem2  16131  lgsdir2lem3  16132  konigsbergiedgwen  16708  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem4  16715  konigsberglem5  16716  konigsberg  16717  ex-fl  16722  ex-exp  16724  bdceqi  16852  bdcriota  16892  bdsepnfALT  16898  bdbm1.3ii  16900  bj-d0clsepcl  16934  nninfsellemeqinf  17033