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  2991  euxfr2dc  3004  cdeqri  3030  sseqtri  3274  3sstr3i  3280  equncomi  3367  unssi  3396  ssini  3446  unabs  3454  inabs  3455  ddifss  3461  inssddif  3464  snid  3722  rabrsndc  3761  rintm  4086  breqtri  4136  bm1.3ii  4233  zfnuleu  4236  zfpow  4290  undifexmid  4308  copsexg  4362  uniop  4374  pwundifss  4408  onunisuci  4555  zfun  4557  op1stb  4601  op1stbg  4602  ordtriexmidlem  4643  ordtriexmid  4645  ordtri2orexmid  4647  2ordpr  4648  ontr2exmid  4649  onsucsssucexmid  4651  onsucelsucexmid  4654  dtruex  4683  ordsoexmid  4686  0elsucexmid  4689  ordtri2or2exmid  4695  dcextest  4705  tfi  4706  relop  4907  dmxpid  4980  rn0  5015  dmresi  5095  issref  5147  cnvcnv  5217  rescnvcnv  5227  cnvcnvres  5228  cnvsn  5247  cocnvcnv2  5276  cores2  5277  co01  5279  relcoi1  5296  cnviinm  5306  fnopab  5485  mpt0  5488  fnmpti  5489  f1cnvcnv  5586  f1ovi  5657  fmpti  5831  fvsnun2  5884  oprabss  6141  relmptopab  6258  2nd0  6341  f1stres  6355  f2ndres  6356  reldmtpos  6486  dftpos4  6496  tpostpos  6497  tpos0  6507  smo0  6531  frecfnom  6634  oasuc  6699  uniixp  6958  ssdomg  7020  xpcomf1o  7078  ssfilem  7132  diffitest  7146  inffiexmid  7168  fiintim  7193  caseinl  7384  caseinr  7385  eninl  7390  eninr  7391  card0  7486  dju1p1e2  7502  pw1on  7538  dmaddpi  7645  dmmulpi  7646  1lt2pi  7660  1lt2nq  7726  suplocsrlempr  8127  gtso  8357  subf  8480  negne0i  8553  negdii  8562  ltapii  8914  sup3exmid  9236  neg1ap0  9351  halflt1  9460  nn0ssz  9600  3halfnz  9681  zeo  9689  numlt  9739  numltc  9740  le9lt10  9741  decle  9748  uzf  9862  indstr  9931  infrenegsupex  9932  xaddf  10183  ixxf  10237  iooval2  10254  ioof  10310  unirnioo  10312  fzval2  10351  fzf  10352  fz10  10386  fzpreddisj  10412  4fvwrd4  10481  fzof  10485  fldiv4p1lem1div2  10672  fldiv4lem1div2  10674  xnn0nnen  10806  hashfibc  11215  sqrt2gt1lt2  11742  infxrnegsupex  11956  fclim  11987  fsumrelem  12165  arisum2  12193  geo2sum2  12209  0.999...  12215  ege2le3  12365  sin0  12423  ef01bndlem  12450  cos2bnd  12454  cos01gt0  12457  sincos2sgn  12460  sin4lt0  12461  egt2lt3  12474  n2dvds1  12606  flodddiv4  12630  0bits  12653  gcdf  12676  nninfct  12745  eucalgf  12760  2prm  12832  dfphi2  12925  pockthi  13064  karatsuba  13136  ballotfilem2  13153  ballotfilem4  13163  znnen  13170  ennnfonelem1  13179  qnnen  13203  ctiunct  13212  ssnnctlemct  13218  structcnvcnv  13249  structfn  13252  relelbasov  13296  xpsff1o  13583  rmodislmod  14548  cnfld0  14768  cnfld1  14769  eltpsi  14955  unitg  14976  epttop  15004  txuni2  15170  retopon  15440  cnfldtopon  15454  dedekindicclemicc  15546  reldvg  15593  dvrecap  15627  dvef  15641  plyrecj  15677  sinhalfpilem  15705  coseq00topi  15749  coseq0negpitopi  15750  sincos4thpi  15754  sincos6thpi  15756  pigt3  15758  cos02pilt1  15765  logltb  15788  rpabscxpbnd  15854  sgmf  15903  1sgm2ppw  15912  lgsdir2lem2  15951  lgsdir2lem3  15952  konigsbergiedgwen  16528  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  konigsberglem4  16535  konigsberglem5  16536  konigsberg  16537  ex-fl  16542  ex-exp  16544  bdceqi  16662  bdcriota  16702  bdsepnfALT  16708  bdbm1.3ii  16710  bj-d0clsepcl  16744  nninfsellemeqinf  16843