Theorem mpbi 144

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 119	. 2 |- ( ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.74i  179  pm4.71i  389  pm4.71ri  390  pm5.32i  451  biadanii  608  pm3.24  688  olc  706  orc  707  dcnn  843  dn1dc  955  3ori  1295  mptxor  1419  mpgbi  1445  dveeq2  1808  dveeq2or  1809  sbequilem  1831  nfsb  1939  sbco  1961  sbcocom  1963  hbsbd  1975  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  hbe1a  2016  elsb1  2148  elsb2  2149  eqcomi  2174  eqtri  2191  eleqtri  2245  neii  2342  neeqtri  2367  nesymi  2386  necomi  2425  nemtbir  2429  neli  2437  nrex  2562  rexlimi  2580  isseti  2738  eueq1  2902  euxfr2dc  2915  cdeqri  2941  sseqtri  3181  3sstr3i  3187  equncomi  3273  unssi  3302  ssini  3350  unabs  3358  inabs  3359  ddifss  3365  inssddif  3368  rgenm  3517  snid  3614  rabrsndc  3651  rintm  3965  breqtri  4014  bm1.3ii  4110  zfnuleu  4113  zfpow  4161  undifexmid  4179  copsexg  4229  uniop  4240  pwundifss  4270  onunisuci  4417  zfun  4419  op1stb  4463  op1stbg  4464  ordtriexmidlem  4503  ordtriexmid  4505  ordtri2orexmid  4507  2ordpr  4508  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmid  4514  dtruex  4543  ordsoexmid  4546  0elsucexmid  4549  ordtri2or2exmid  4555  dcextest  4565  tfi  4566  relop  4761  dmxpid  4832  rn0  4867  dmresi  4946  issref  4993  cnvcnv  5063  rescnvcnv  5073  cnvcnvres  5074  cnvsn  5093  cocnvcnv2  5122  cores2  5123  co01  5125  relcoi1  5142  cnviinm  5152  fnopab  5322  mpt0  5325  fnmpti  5326  f1cnvcnv  5414  f1ovi  5481  fmpti  5648  fvsnun2  5694  oprabss  5939  2nd0  6124  f1stres  6138  f2ndres  6139  reldmtpos  6232  dftpos4  6242  tpostpos  6243  tpos0  6253  smo0  6277  frecfnom  6380  oasuc  6443  uniixp  6699  ssdomg  6756  xpcomf1o  6803  ssfilem  6853  diffitest  6865  inffiexmid  6884  fiintim  6906  caseinl  7068  caseinr  7069  eninl  7074  eninr  7075  card0  7165  dju1p1e2  7174  pw1on  7203  dmaddpi  7287  dmmulpi  7288  1lt2pi  7302  1lt2nq  7368  suplocsrlempr  7769  gtso  7998  subf  8121  negne0i  8194  negdii  8203  ltapii  8554  sup3exmid  8873  neg1ap0  8987  halflt1  9095  nn0ssz  9230  3halfnz  9309  zeo  9317  numlt  9367  numltc  9368  le9lt10  9369  decle  9376  uzf  9490  indstr  9552  infrenegsupex  9553  xaddf  9801  ixxf  9855  iooval2  9872  ioof  9928  unirnioo  9930  fzval2  9968  fzf  9969  fz10  10002  fzpreddisj  10027  4fvwrd4  10096  fzof  10100  fldiv4p1lem1div2  10261  sqrt2gt1lt2  11013  infxrnegsupex  11226  fclim  11257  fsumrelem  11434  arisum2  11462  geo2sum2  11478  0.999...  11484  ege2le3  11634  sin0  11692  ef01bndlem  11719  cos2bnd  11723  cos01gt0  11725  sincos2sgn  11728  sin4lt0  11729  egt2lt3  11742  n2dvds1  11871  flodddiv4  11893  gcdf  11927  eucalgf  12009  2prm  12081  dfphi2  12174  pockthi  12310  znnen  12353  ennnfonelem1  12362  qnnen  12386  ctiunct  12395  ssnnctlemct  12401  structcnvcnv  12432  structfn  12435  eltpsi  12833  unitg  12856  epttop  12884  txuni2  13050  retopon  13320  dedekindicclemicc  13404  reldvg  13442  dvrecap  13471  dvef  13482  sinhalfpilem  13506  coseq00topi  13550  coseq0negpitopi  13551  sincos4thpi  13555  sincos6thpi  13557  pigt3  13559  cos02pilt1  13566  logltb  13589  rpabscxpbnd  13653  lgsdir2lem2  13724  lgsdir2lem3  13725  ex-fl  13760  ex-exp  13762  bdceqi  13878  bdcriota  13918  bdsepnfALT  13924  bdbm1.3ii  13926  bj-d0clsepcl  13960  nninfsellemeqinf  14049