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  694  olc  712  orc  713  dcnn  849  dn1dc  962  3ori  1311  mptxor  1435  mpgbi  1463  dveeq2  1826  dveeq2or  1827  sbequilem  1849  nfsb  1962  sbco  1984  sbcocom  1986  hbsbd  1998  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  hbe1a  2039  elsb1  2171  elsb2  2172  eqcomi  2197  eqtri  2214  eleqtri  2268  neii  2366  neeqtri  2391  nesymi  2410  necomi  2449  nemtbir  2453  neli  2461  nrex  2586  rexlimi  2604  isseti  2768  eueq1  2933  euxfr2dc  2946  cdeqri  2972  sseqtri  3214  3sstr3i  3220  equncomi  3306  unssi  3335  ssini  3383  unabs  3391  inabs  3392  ddifss  3398  inssddif  3401  snid  3650  rabrsndc  3687  rintm  4006  breqtri  4055  bm1.3ii  4151  zfnuleu  4154  zfpow  4205  undifexmid  4223  copsexg  4274  uniop  4285  pwundifss  4317  onunisuci  4464  zfun  4466  op1stb  4510  op1stbg  4511  ordtriexmidlem  4552  ordtriexmid  4554  ordtri2orexmid  4556  2ordpr  4557  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  dtruex  4592  ordsoexmid  4595  0elsucexmid  4598  ordtri2or2exmid  4604  dcextest  4614  tfi  4615  relop  4813  dmxpid  4884  rn0  4919  dmresi  4998  issref  5049  cnvcnv  5119  rescnvcnv  5129  cnvcnvres  5130  cnvsn  5149  cocnvcnv2  5178  cores2  5179  co01  5181  relcoi1  5198  cnviinm  5208  fnopab  5379  mpt0  5382  fnmpti  5383  f1cnvcnv  5471  f1ovi  5540  fmpti  5711  fvsnun2  5757  oprabss  6005  2nd0  6200  f1stres  6214  f2ndres  6215  reldmtpos  6308  dftpos4  6318  tpostpos  6319  tpos0  6329  smo0  6353  frecfnom  6456  oasuc  6519  uniixp  6777  ssdomg  6834  xpcomf1o  6881  ssfilem  6933  diffitest  6945  inffiexmid  6964  fiintim  6987  caseinl  7152  caseinr  7153  eninl  7158  eninr  7159  card0  7250  dju1p1e2  7259  pw1on  7288  dmaddpi  7387  dmmulpi  7388  1lt2pi  7402  1lt2nq  7468  suplocsrlempr  7869  gtso  8100  subf  8223  negne0i  8296  negdii  8305  ltapii  8656  sup3exmid  8978  neg1ap0  9093  halflt1  9202  nn0ssz  9338  3halfnz  9417  zeo  9425  numlt  9475  numltc  9476  le9lt10  9477  decle  9484  uzf  9598  indstr  9661  infrenegsupex  9662  xaddf  9913  ixxf  9967  iooval2  9984  ioof  10040  unirnioo  10042  fzval2  10080  fzf  10081  fz10  10115  fzpreddisj  10140  4fvwrd4  10209  fzof  10213  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  xnn0nnen  10511  sqrt2gt1lt2  11196  infxrnegsupex  11409  fclim  11440  fsumrelem  11617  arisum2  11645  geo2sum2  11661  0.999...  11667  ege2le3  11817  sin0  11875  ef01bndlem  11902  cos2bnd  11906  cos01gt0  11909  sincos2sgn  11912  sin4lt0  11913  egt2lt3  11926  n2dvds1  12056  flodddiv4  12078  gcdf  12112  nninfct  12181  eucalgf  12196  2prm  12268  dfphi2  12361  pockthi  12499  znnen  12558  ennnfonelem1  12567  qnnen  12591  ctiunct  12600  ssnnctlemct  12606  structcnvcnv  12637  structfn  12640  relelbasov  12683  xpsff1o  12935  rmodislmod  13850  cnfld0  14070  cnfld1  14071  eltpsi  14220  unitg  14241  epttop  14269  txuni2  14435  retopon  14705  cnfldtopon  14719  dedekindicclemicc  14811  reldvg  14858  dvrecap  14892  dvef  14906  plyrecj  14941  sinhalfpilem  14967  coseq00topi  15011  coseq0negpitopi  15012  sincos4thpi  15016  sincos6thpi  15018  pigt3  15020  cos02pilt1  15027  logltb  15050  rpabscxpbnd  15114  lgsdir2lem2  15186  lgsdir2lem3  15187  ex-fl  15287  ex-exp  15289  bdceqi  15405  bdcriota  15445  bdsepnfALT  15451  bdbm1.3ii  15453  bj-d0clsepcl  15487  nninfsellemeqinf  15576