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  700  olc  718  orc  719  dcnn  855  dn1dc  968  3ori  1336  mptxor  1468  mpgbi  1500  dveeq2  1862  dveeq2or  1863  sbequilem  1885  nfsb  1998  sbco  2020  sbcocom  2022  hbsbd  2034  dvelimALT  2062  dvelimfv  2063  dvelimor  2070  hbe1a  2075  elsb1  2208  elsb2  2209  eqcomi  2234  eqtri  2251  eleqtri  2305  neii  2403  neeqtri  2428  nesymi  2447  necomi  2486  nemtbir  2490  neli  2498  nrex  2623  rexlimi  2642  isseti  2810  eueq1  2977  euxfr2dc  2990  cdeqri  3016  sseqtri  3260  3sstr3i  3266  equncomi  3352  unssi  3381  ssini  3429  unabs  3437  inabs  3438  ddifss  3444  inssddif  3447  snid  3701  rabrsndc  3740  rintm  4064  breqtri  4114  bm1.3ii  4211  zfnuleu  4214  zfpow  4267  undifexmid  4285  copsexg  4338  uniop  4350  pwundifss  4384  onunisuci  4531  zfun  4533  op1stb  4577  op1stbg  4578  ordtriexmidlem  4619  ordtriexmid  4621  ordtri2orexmid  4623  2ordpr  4624  ontr2exmid  4625  onsucsssucexmid  4627  onsucelsucexmid  4630  dtruex  4659  ordsoexmid  4662  0elsucexmid  4665  ordtri2or2exmid  4671  dcextest  4681  tfi  4682  relop  4882  dmxpid  4955  rn0  4990  dmresi  5070  issref  5121  cnvcnv  5191  rescnvcnv  5201  cnvcnvres  5202  cnvsn  5221  cocnvcnv2  5250  cores2  5251  co01  5253  relcoi1  5270  cnviinm  5280  fnopab  5459  mpt0  5462  fnmpti  5463  f1cnvcnv  5556  f1ovi  5627  fmpti  5802  fvsnun2  5855  oprabss  6112  relmptopab  6229  2nd0  6313  f1stres  6327  f2ndres  6328  reldmtpos  6424  dftpos4  6434  tpostpos  6435  tpos0  6445  smo0  6469  frecfnom  6572  oasuc  6637  uniixp  6895  ssdomg  6957  xpcomf1o  7014  ssfilem  7067  diffitest  7081  inffiexmid  7103  fiintim  7128  caseinl  7295  caseinr  7296  eninl  7301  eninr  7302  card0  7397  dju1p1e2  7413  pw1on  7449  dmaddpi  7550  dmmulpi  7551  1lt2pi  7565  1lt2nq  7631  suplocsrlempr  8032  gtso  8263  subf  8386  negne0i  8459  negdii  8468  ltapii  8820  sup3exmid  9142  neg1ap0  9257  halflt1  9366  nn0ssz  9502  3halfnz  9582  zeo  9590  numlt  9640  numltc  9641  le9lt10  9642  decle  9649  uzf  9763  indstr  9832  infrenegsupex  9833  xaddf  10084  ixxf  10138  iooval2  10155  ioof  10211  unirnioo  10213  fzval2  10251  fzf  10252  fz10  10286  fzpreddisj  10311  4fvwrd4  10380  fzof  10384  fldiv4p1lem1div2  10571  fldiv4lem1div2  10573  xnn0nnen  10705  sqrt2gt1lt2  11632  infxrnegsupex  11846  fclim  11877  fsumrelem  12055  arisum2  12083  geo2sum2  12099  0.999...  12105  ege2le3  12255  sin0  12313  ef01bndlem  12340  cos2bnd  12344  cos01gt0  12347  sincos2sgn  12350  sin4lt0  12351  egt2lt3  12364  n2dvds1  12496  flodddiv4  12520  0bits  12543  gcdf  12566  nninfct  12635  eucalgf  12650  2prm  12722  dfphi2  12815  pockthi  12954  karatsuba  13026  znnen  13042  ennnfonelem1  13051  qnnen  13075  ctiunct  13084  ssnnctlemct  13090  structcnvcnv  13121  structfn  13124  relelbasov  13168  xpsff1o  13455  rmodislmod  14389  cnfld0  14609  cnfld1  14610  eltpsi  14794  unitg  14815  epttop  14843  txuni2  15009  retopon  15279  cnfldtopon  15293  dedekindicclemicc  15385  reldvg  15432  dvrecap  15466  dvef  15480  plyrecj  15516  sinhalfpilem  15544  coseq00topi  15588  coseq0negpitopi  15589  sincos4thpi  15593  sincos6thpi  15595  pigt3  15597  cos02pilt1  15604  logltb  15627  rpabscxpbnd  15693  sgmf  15739  1sgm2ppw  15748  lgsdir2lem2  15787  lgsdir2lem3  15788  konigsbergiedgwen  16364  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  konigsberglem4  16371  konigsberglem5  16372  konigsberg  16373  ex-fl  16378  ex-exp  16380  bdceqi  16498  bdcriota  16538  bdsepnfALT  16544  bdbm1.3ii  16546  bj-d0clsepcl  16580  nninfsellemeqinf  16681