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  391  pm4.71ri  392  pm5.32i  454  biadanii  617  pm3.24  701  olc  719  orc  720  dcnn  856  dn1dc  969  3ori  1337  mptxor  1469  mpgbi  1501  dveeq2  1864  dveeq2or  1865  sbequilem  1887  nfsb  2002  sbco  2024  sbcocom  2026  hbsbd  2038  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  hbe1a  2079  elsb1  2212  elsb2  2213  eqcomi  2238  eqtri  2255  eleqtri  2309  neii  2416  neeqtri  2441  nesymi  2460  necomi  2499  nemtbir  2503  neli  2511  nrex  2636  rexlimi  2655  isseti  2824  eueq1  2992  euxfr2dc  3005  cdeqri  3031  sseqtri  3276  3sstr3i  3282  equncomi  3369  unssi  3398  ssini  3448  unabs  3456  inabs  3457  ddifss  3463  inssddif  3466  snid  3725  rabrsndc  3764  rintm  4089  breqtri  4139  bm1.3ii  4236  zfnuleu  4239  zfpow  4293  undifexmid  4311  copsexg  4365  uniop  4377  pwundifss  4411  onunisuci  4558  zfun  4560  op1stb  4604  op1stbg  4605  ordtriexmidlem  4646  ordtriexmid  4648  ordtri2orexmid  4650  2ordpr  4651  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  dtruex  4686  ordsoexmid  4689  0elsucexmid  4692  ordtri2or2exmid  4698  dcextest  4708  tfi  4709  relop  4910  dmxpid  4983  rn0  5018  dmresi  5098  issref  5150  cnvcnv  5220  rescnvcnv  5230  cnvcnvres  5231  cnvsn  5250  cocnvcnv2  5279  cores2  5280  co01  5282  relcoi1  5299  cnviinm  5309  fnopab  5488  mpt0  5491  fnmpti  5492  f1cnvcnv  5589  f1ovi  5660  fmpti  5834  fvsnun2  5887  rinvf1o  6008  oprabss  6147  relmptopab  6264  2nd0  6352  f1stres  6366  f2ndres  6367  reldmtpos  6497  dftpos4  6507  tpostpos  6508  tpos0  6518  smo0  6542  frecfnom  6645  oasuc  6710  uniixp  6969  ssdomg  7031  xpcomf1o  7089  ssfilem  7143  diffitest  7157  inffiexmid  7179  fiintim  7204  caseinl  7395  caseinr  7396  eninl  7401  eninr  7402  card0  7497  dju1p1e2  7513  pw1on  7549  dmaddpi  7656  dmmulpi  7657  1lt2pi  7671  1lt2nq  7737  suplocsrlempr  8138  gtso  8368  subf  8492  negne0i  8565  negdii  8574  ltapii  8927  sup3exmid  9251  neg1ap0  9366  halflt1  9475  nn0ssz  9615  3halfnz  9696  zeo  9704  numlt  9754  numltc  9755  le9lt10  9756  decle  9763  uzf  9877  indstr  9946  infrenegsupex  9947  xaddf  10199  ixxf  10253  iooval2  10270  ioof  10326  unirnioo  10328  fzval2  10367  fzf  10368  fz10  10403  fzpreddisj  10430  4fvwrd4  10499  fzof  10503  fldiv4p1lem1div2  10692  fldiv4lem1div2  10694  xnn0nnen  10826  hashfibc  11235  sqrt2gt1lt2  11762  infxrnegsupex  11976  fclim  12007  fsumrelem  12185  arisum2  12213  geo2sum2  12229  0.999...  12235  ege2le3  12385  sin0  12443  ef01bndlem  12470  cos2bnd  12474  cos01gt0  12477  sincos2sgn  12480  sin4lt0  12481  egt2lt3  12494  n2dvds1  12626  flodddiv4  12650  0bits  12673  gcdf  12696  nninfct  12765  eucalgf  12780  2prm  12852  dfphi2  12945  pockthi  13084  karatsuba  13156  ballotfilem2  13175  ballotfilem4  13188  ballotfilem5  13189  ballotfilemi1  13192  ballotfilem7  13226  ballotfilemth  13228  znnen  13236  ennnfonelem1  13245  qnnen  13269  ctiunct  13278  ssnnctlemct  13284  structcnvcnv  13315  structfn  13318  relelbasov  13362  xpsff1o  13616  rmodislmod  14628  cnfld0  14848  cnfld1  14849  eltpsi  15035  unitg  15056  epttop  15084  txuni2  15250  retopon  15520  cnfldtopon  15534  dedekindicclemicc  15626  reldvg  15673  dvrecap  15707  dvef  15721  plyrecj  15757  sinhalfpilem  15785  coseq00topi  15829  coseq0negpitopi  15830  sincos4thpi  15834  sincos6thpi  15836  pigt3  15838  cos02pilt1  15845  logltb  15868  rpabscxpbnd  15934  sgmf  15983  1sgm2ppw  15992  lgsdir2lem2  16031  lgsdir2lem3  16032  konigsbergiedgwen  16608  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  konigsberglem4  16615  konigsberglem5  16616  konigsberg  16617  ex-fl  16622  ex-exp  16624  bdceqi  16752  bdcriota  16792  bdsepnfALT  16798  bdbm1.3ii  16800  bj-d0clsepcl  16834  nninfsellemeqinf  16933