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  5851  oprabss  6106  relmptopab  6223  2nd0  6307  f1stres  6321  f2ndres  6322  reldmtpos  6418  dftpos4  6428  tpostpos  6429  tpos0  6439  smo0  6463  frecfnom  6566  oasuc  6631  uniixp  6889  ssdomg  6951  xpcomf1o  7008  ssfilem  7061  diffitest  7075  inffiexmid  7097  fiintim  7122  caseinl  7289  caseinr  7290  eninl  7295  eninr  7296  card0  7391  dju1p1e2  7407  pw1on  7443  dmaddpi  7544  dmmulpi  7545  1lt2pi  7559  1lt2nq  7625  suplocsrlempr  8026  gtso  8257  subf  8380  negne0i  8453  negdii  8462  ltapii  8814  sup3exmid  9136  neg1ap0  9251  halflt1  9360  nn0ssz  9496  3halfnz  9576  zeo  9584  numlt  9634  numltc  9635  le9lt10  9636  decle  9643  uzf  9757  indstr  9826  infrenegsupex  9827  xaddf  10078  ixxf  10132  iooval2  10149  ioof  10205  unirnioo  10207  fzval2  10245  fzf  10246  fz10  10280  fzpreddisj  10305  4fvwrd4  10374  fzof  10378  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  xnn0nnen  10698  sqrt2gt1lt2  11609  infxrnegsupex  11823  fclim  11854  fsumrelem  12031  arisum2  12059  geo2sum2  12075  0.999...  12081  ege2le3  12231  sin0  12289  ef01bndlem  12316  cos2bnd  12320  cos01gt0  12323  sincos2sgn  12326  sin4lt0  12327  egt2lt3  12340  n2dvds1  12472  flodddiv4  12496  0bits  12519  gcdf  12542  nninfct  12611  eucalgf  12626  2prm  12698  dfphi2  12791  pockthi  12930  karatsuba  13002  znnen  13018  ennnfonelem1  13027  qnnen  13051  ctiunct  13060  ssnnctlemct  13066  structcnvcnv  13097  structfn  13100  relelbasov  13144  xpsff1o  13431  rmodislmod  14364  cnfld0  14584  cnfld1  14585  eltpsi  14764  unitg  14785  epttop  14813  txuni2  14979  retopon  15249  cnfldtopon  15263  dedekindicclemicc  15355  reldvg  15402  dvrecap  15436  dvef  15450  plyrecj  15486  sinhalfpilem  15514  coseq00topi  15558  coseq0negpitopi  15559  sincos4thpi  15563  sincos6thpi  15565  pigt3  15567  cos02pilt1  15574  logltb  15597  rpabscxpbnd  15663  sgmf  15709  1sgm2ppw  15718  lgsdir2lem2  15757  lgsdir2lem3  15758  ex-fl  16321  ex-exp  16323  bdceqi  16438  bdcriota  16478  bdsepnfALT  16484  bdbm1.3ii  16486  bj-d0clsepcl  16520  nninfsellemeqinf  16618