Theorem mpbi 145

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbi.min	|- ph
mpbi.maj	|- ( ph <-> ps )

Assertion

Ref	Expression
mpbi	|- ps

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 |- ph
2		mpbi.maj	. . 3 |- ( ph <-> ps )
3	2	biimpi 120	. 2 |- ( ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

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  1863  dveeq2or  1864  sbequilem  1886  nfsb  1999  sbco  2021  sbcocom  2023  hbsbd  2035  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  hbe1a  2076  elsb1  2209  elsb2  2210  eqcomi  2235  eqtri  2252  eleqtri  2306  neii  2404  neeqtri  2429  nesymi  2448  necomi  2487  nemtbir  2491  neli  2499  nrex  2624  rexlimi  2643  isseti  2811  eueq1  2978  euxfr2dc  2991  cdeqri  3017  sseqtri  3261  3sstr3i  3267  equncomi  3353  unssi  3382  ssini  3430  unabs  3438  inabs  3439  ddifss  3445  inssddif  3448  snid  3700  rabrsndc  3739  rintm  4063  breqtri  4113  bm1.3ii  4210  zfnuleu  4213  zfpow  4265  undifexmid  4283  copsexg  4336  uniop  4348  pwundifss  4382  onunisuci  4529  zfun  4531  op1stb  4575  op1stbg  4576  ordtriexmidlem  4617  ordtriexmid  4619  ordtri2orexmid  4621  2ordpr  4622  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  dtruex  4657  ordsoexmid  4660  0elsucexmid  4663  ordtri2or2exmid  4669  dcextest  4679  tfi  4680  relop  4880  dmxpid  4953  rn0  4988  dmresi  5068  issref  5119  cnvcnv  5189  rescnvcnv  5199  cnvcnvres  5200  cnvsn  5219  cocnvcnv2  5248  cores2  5249  co01  5251  relcoi1  5268  cnviinm  5278  fnopab  5457  mpt0  5460  fnmpti  5461  f1cnvcnv  5553  f1ovi  5624  fmpti  5799  fvsnun2  5852  oprabss  6107  relmptopab  6224  2nd0  6308  f1stres  6322  f2ndres  6323  reldmtpos  6419  dftpos4  6429  tpostpos  6430  tpos0  6440  smo0  6464  frecfnom  6567  oasuc  6632  uniixp  6890  ssdomg  6952  xpcomf1o  7009  ssfilem  7062  diffitest  7076  inffiexmid  7098  fiintim  7123  caseinl  7290  caseinr  7291  eninl  7296  eninr  7297  card0  7392  dju1p1e2  7408  pw1on  7444  dmaddpi  7545  dmmulpi  7546  1lt2pi  7560  1lt2nq  7626  suplocsrlempr  8027  gtso  8258  subf  8381  negne0i  8454  negdii  8463  ltapii  8815  sup3exmid  9137  neg1ap0  9252  halflt1  9361  nn0ssz  9497  3halfnz  9577  zeo  9585  numlt  9635  numltc  9636  le9lt10  9637  decle  9644  uzf  9758  indstr  9827  infrenegsupex  9828  xaddf  10079  ixxf  10133  iooval2  10150  ioof  10206  unirnioo  10208  fzval2  10246  fzf  10247  fz10  10281  fzpreddisj  10306  4fvwrd4  10375  fzof  10379  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  xnn0nnen  10700  sqrt2gt1lt2  11627  infxrnegsupex  11841  fclim  11872  fsumrelem  12050  arisum2  12078  geo2sum2  12094  0.999...  12100  ege2le3  12250  sin0  12308  ef01bndlem  12335  cos2bnd  12339  cos01gt0  12342  sincos2sgn  12345  sin4lt0  12346  egt2lt3  12359  n2dvds1  12491  flodddiv4  12515  0bits  12538  gcdf  12561  nninfct  12630  eucalgf  12645  2prm  12717  dfphi2  12810  pockthi  12949  karatsuba  13021  znnen  13037  ennnfonelem1  13046  qnnen  13070  ctiunct  13079  ssnnctlemct  13085  structcnvcnv  13116  structfn  13119  relelbasov  13163  xpsff1o  13450  rmodislmod  14384  cnfld0  14604  cnfld1  14605  eltpsi  14784  unitg  14805  epttop  14833  txuni2  14999  retopon  15269  cnfldtopon  15283  dedekindicclemicc  15375  reldvg  15422  dvrecap  15456  dvef  15470  plyrecj  15506  sinhalfpilem  15534  coseq00topi  15578  coseq0negpitopi  15579  sincos4thpi  15583  sincos6thpi  15585  pigt3  15587  cos02pilt1  15594  logltb  15617  rpabscxpbnd  15683  sgmf  15729  1sgm2ppw  15738  lgsdir2lem2  15777  lgsdir2lem3  15778  konigsbergiedgwen  16354  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem4  16361  konigsberglem5  16362  konigsberg  16363  ex-fl  16368  ex-exp  16370  bdceqi  16489  bdcriota  16529  bdsepnfALT  16535  bdbm1.3ii  16537  bj-d0clsepcl  16571  nninfsellemeqinf  16669