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  615  pm3.24  698  olc  716  orc  717  dcnn  853  dn1dc  966  3ori  1334  mptxor  1466  mpgbi  1498  dveeq2  1861  dveeq2or  1862  sbequilem  1884  nfsb  1997  sbco  2019  sbcocom  2021  hbsbd  2033  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  hbe1a  2074  elsb1  2207  elsb2  2208  eqcomi  2233  eqtri  2250  eleqtri  2304  neii  2402  neeqtri  2427  nesymi  2446  necomi  2485  nemtbir  2489  neli  2497  nrex  2622  rexlimi  2641  isseti  2808  eueq1  2975  euxfr2dc  2988  cdeqri  3014  sseqtri  3258  3sstr3i  3264  equncomi  3350  unssi  3379  ssini  3427  unabs  3435  inabs  3436  ddifss  3442  inssddif  3445  snid  3697  rabrsndc  3734  rintm  4058  breqtri  4108  bm1.3ii  4205  zfnuleu  4208  zfpow  4259  undifexmid  4277  copsexg  4330  uniop  4342  pwundifss  4376  onunisuci  4523  zfun  4525  op1stb  4569  op1stbg  4570  ordtriexmidlem  4611  ordtriexmid  4613  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  dtruex  4651  ordsoexmid  4654  0elsucexmid  4657  ordtri2or2exmid  4663  dcextest  4673  tfi  4674  relop  4872  dmxpid  4945  rn0  4980  dmresi  5060  issref  5111  cnvcnv  5181  rescnvcnv  5191  cnvcnvres  5192  cnvsn  5211  cocnvcnv2  5240  cores2  5241  co01  5243  relcoi1  5260  cnviinm  5270  fnopab  5448  mpt0  5451  fnmpti  5452  f1cnvcnv  5542  f1ovi  5612  fmpti  5787  fvsnun2  5837  oprabss  6090  relmptopab  6207  2nd0  6291  f1stres  6305  f2ndres  6306  reldmtpos  6399  dftpos4  6409  tpostpos  6410  tpos0  6420  smo0  6444  frecfnom  6547  oasuc  6610  uniixp  6868  ssdomg  6930  xpcomf1o  6984  ssfilem  7037  diffitest  7049  inffiexmid  7068  fiintim  7093  caseinl  7258  caseinr  7259  eninl  7264  eninr  7265  card0  7360  dju1p1e2  7375  pw1on  7411  dmaddpi  7512  dmmulpi  7513  1lt2pi  7527  1lt2nq  7593  suplocsrlempr  7994  gtso  8225  subf  8348  negne0i  8421  negdii  8430  ltapii  8782  sup3exmid  9104  neg1ap0  9219  halflt1  9328  nn0ssz  9464  3halfnz  9544  zeo  9552  numlt  9602  numltc  9603  le9lt10  9604  decle  9611  uzf  9725  indstr  9788  infrenegsupex  9789  xaddf  10040  ixxf  10094  iooval2  10111  ioof  10167  unirnioo  10169  fzval2  10207  fzf  10208  fz10  10242  fzpreddisj  10267  4fvwrd4  10336  fzof  10340  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  xnn0nnen  10659  sqrt2gt1lt2  11560  infxrnegsupex  11774  fclim  11805  fsumrelem  11982  arisum2  12010  geo2sum2  12026  0.999...  12032  ege2le3  12182  sin0  12240  ef01bndlem  12267  cos2bnd  12271  cos01gt0  12274  sincos2sgn  12277  sin4lt0  12278  egt2lt3  12291  n2dvds1  12423  flodddiv4  12447  0bits  12470  gcdf  12493  nninfct  12562  eucalgf  12577  2prm  12649  dfphi2  12742  pockthi  12881  karatsuba  12953  znnen  12969  ennnfonelem1  12978  qnnen  13002  ctiunct  13011  ssnnctlemct  13017  structcnvcnv  13048  structfn  13051  relelbasov  13095  xpsff1o  13382  rmodislmod  14315  cnfld0  14535  cnfld1  14536  eltpsi  14715  unitg  14736  epttop  14764  txuni2  14930  retopon  15200  cnfldtopon  15214  dedekindicclemicc  15306  reldvg  15353  dvrecap  15387  dvef  15401  plyrecj  15437  sinhalfpilem  15465  coseq00topi  15509  coseq0negpitopi  15510  sincos4thpi  15514  sincos6thpi  15516  pigt3  15518  cos02pilt1  15525  logltb  15548  rpabscxpbnd  15614  sgmf  15660  1sgm2ppw  15669  lgsdir2lem2  15708  lgsdir2lem3  15709  ex-fl  16089  ex-exp  16091  bdceqi  16206  bdcriota  16246  bdsepnfALT  16252  bdbm1.3ii  16254  bj-d0clsepcl  16288  nninfsellemeqinf  16382