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  613  pm3.24  695  olc  713  orc  714  dcnn  850  dn1dc  963  3ori  1313  mptxor  1444  mpgbi  1476  dveeq2  1839  dveeq2or  1840  sbequilem  1862  nfsb  1975  sbco  1997  sbcocom  1999  hbsbd  2011  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  hbe1a  2052  elsb1  2185  elsb2  2186  eqcomi  2211  eqtri  2228  eleqtri  2282  neii  2380  neeqtri  2405  nesymi  2424  necomi  2463  nemtbir  2467  neli  2475  nrex  2600  rexlimi  2618  isseti  2785  eueq1  2952  euxfr2dc  2965  cdeqri  2991  sseqtri  3235  3sstr3i  3241  equncomi  3327  unssi  3356  ssini  3404  unabs  3412  inabs  3413  ddifss  3419  inssddif  3422  snid  3674  rabrsndc  3711  rintm  4034  breqtri  4084  bm1.3ii  4181  zfnuleu  4184  zfpow  4235  undifexmid  4253  copsexg  4306  uniop  4318  pwundifss  4350  onunisuci  4497  zfun  4499  op1stb  4543  op1stbg  4544  ordtriexmidlem  4585  ordtriexmid  4587  ordtri2orexmid  4589  2ordpr  4590  ontr2exmid  4591  onsucsssucexmid  4593  onsucelsucexmid  4596  dtruex  4625  ordsoexmid  4628  0elsucexmid  4631  ordtri2or2exmid  4637  dcextest  4647  tfi  4648  relop  4846  dmxpid  4918  rn0  4953  dmresi  5033  issref  5084  cnvcnv  5154  rescnvcnv  5164  cnvcnvres  5165  cnvsn  5184  cocnvcnv2  5213  cores2  5214  co01  5216  relcoi1  5233  cnviinm  5243  fnopab  5420  mpt0  5423  fnmpti  5424  f1cnvcnv  5514  f1ovi  5584  fmpti  5755  fvsnun2  5805  oprabss  6054  2nd0  6254  f1stres  6268  f2ndres  6269  reldmtpos  6362  dftpos4  6372  tpostpos  6373  tpos0  6383  smo0  6407  frecfnom  6510  oasuc  6573  uniixp  6831  ssdomg  6893  xpcomf1o  6945  ssfilem  6998  diffitest  7010  inffiexmid  7029  fiintim  7054  caseinl  7219  caseinr  7220  eninl  7225  eninr  7226  card0  7321  dju1p1e2  7336  pw1on  7372  dmaddpi  7473  dmmulpi  7474  1lt2pi  7488  1lt2nq  7554  suplocsrlempr  7955  gtso  8186  subf  8309  negne0i  8382  negdii  8391  ltapii  8743  sup3exmid  9065  neg1ap0  9180  halflt1  9289  nn0ssz  9425  3halfnz  9505  zeo  9513  numlt  9563  numltc  9564  le9lt10  9565  decle  9572  uzf  9686  indstr  9749  infrenegsupex  9750  xaddf  10001  ixxf  10055  iooval2  10072  ioof  10128  unirnioo  10130  fzval2  10168  fzf  10169  fz10  10203  fzpreddisj  10228  4fvwrd4  10297  fzof  10301  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  xnn0nnen  10619  sqrt2gt1lt2  11475  infxrnegsupex  11689  fclim  11720  fsumrelem  11897  arisum2  11925  geo2sum2  11941  0.999...  11947  ege2le3  12097  sin0  12155  ef01bndlem  12182  cos2bnd  12186  cos01gt0  12189  sincos2sgn  12192  sin4lt0  12193  egt2lt3  12206  n2dvds1  12338  flodddiv4  12362  0bits  12385  gcdf  12408  nninfct  12477  eucalgf  12492  2prm  12564  dfphi2  12657  pockthi  12796  karatsuba  12868  znnen  12884  ennnfonelem1  12893  qnnen  12917  ctiunct  12926  ssnnctlemct  12932  structcnvcnv  12963  structfn  12966  relelbasov  13009  xpsff1o  13296  rmodislmod  14228  cnfld0  14448  cnfld1  14449  eltpsi  14628  unitg  14649  epttop  14677  txuni2  14843  retopon  15113  cnfldtopon  15127  dedekindicclemicc  15219  reldvg  15266  dvrecap  15300  dvef  15314  plyrecj  15350  sinhalfpilem  15378  coseq00topi  15422  coseq0negpitopi  15423  sincos4thpi  15427  sincos6thpi  15429  pigt3  15431  cos02pilt1  15438  logltb  15461  rpabscxpbnd  15527  sgmf  15573  1sgm2ppw  15582  lgsdir2lem2  15621  lgsdir2lem3  15622  ex-fl  15861  ex-exp  15863  bdceqi  15978  bdcriota  16018  bdsepnfALT  16024  bdbm1.3ii  16026  bj-d0clsepcl  16060  nninfsellemeqinf  16155