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  1312  mptxor  1443  mpgbi  1474  dveeq2  1837  dveeq2or  1838  sbequilem  1860  nfsb  1973  sbco  1995  sbcocom  1997  hbsbd  2009  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  hbe1a  2050  elsb1  2182  elsb2  2183  eqcomi  2208  eqtri  2225  eleqtri  2279  neii  2377  neeqtri  2402  nesymi  2421  necomi  2460  nemtbir  2464  neli  2472  nrex  2597  rexlimi  2615  isseti  2779  eueq1  2944  euxfr2dc  2957  cdeqri  2983  sseqtri  3226  3sstr3i  3232  equncomi  3318  unssi  3347  ssini  3395  unabs  3403  inabs  3404  ddifss  3410  inssddif  3413  snid  3663  rabrsndc  3700  rintm  4019  breqtri  4068  bm1.3ii  4164  zfnuleu  4167  zfpow  4218  undifexmid  4236  copsexg  4287  uniop  4299  pwundifss  4331  onunisuci  4478  zfun  4480  op1stb  4524  op1stbg  4525  ordtriexmidlem  4566  ordtriexmid  4568  ordtri2orexmid  4570  2ordpr  4571  ontr2exmid  4572  onsucsssucexmid  4574  onsucelsucexmid  4577  dtruex  4606  ordsoexmid  4609  0elsucexmid  4612  ordtri2or2exmid  4618  dcextest  4628  tfi  4629  relop  4827  dmxpid  4898  rn0  4933  dmresi  5013  issref  5064  cnvcnv  5134  rescnvcnv  5144  cnvcnvres  5145  cnvsn  5164  cocnvcnv2  5193  cores2  5194  co01  5196  relcoi1  5213  cnviinm  5223  fnopab  5399  mpt0  5402  fnmpti  5403  f1cnvcnv  5491  f1ovi  5560  fmpti  5731  fvsnun2  5781  oprabss  6030  2nd0  6230  f1stres  6244  f2ndres  6245  reldmtpos  6338  dftpos4  6348  tpostpos  6349  tpos0  6359  smo0  6383  frecfnom  6486  oasuc  6549  uniixp  6807  ssdomg  6869  xpcomf1o  6919  ssfilem  6971  diffitest  6983  inffiexmid  7002  fiintim  7027  caseinl  7192  caseinr  7193  eninl  7198  eninr  7199  card0  7294  dju1p1e2  7304  pw1on  7337  dmaddpi  7437  dmmulpi  7438  1lt2pi  7452  1lt2nq  7518  suplocsrlempr  7919  gtso  8150  subf  8273  negne0i  8346  negdii  8355  ltapii  8707  sup3exmid  9029  neg1ap0  9144  halflt1  9253  nn0ssz  9389  3halfnz  9469  zeo  9477  numlt  9527  numltc  9528  le9lt10  9529  decle  9536  uzf  9650  indstr  9713  infrenegsupex  9714  xaddf  9965  ixxf  10019  iooval2  10036  ioof  10092  unirnioo  10094  fzval2  10132  fzf  10133  fz10  10167  fzpreddisj  10192  4fvwrd4  10261  fzof  10265  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  xnn0nnen  10580  sqrt2gt1lt2  11331  infxrnegsupex  11545  fclim  11576  fsumrelem  11753  arisum2  11781  geo2sum2  11797  0.999...  11803  ege2le3  11953  sin0  12011  ef01bndlem  12038  cos2bnd  12042  cos01gt0  12045  sincos2sgn  12048  sin4lt0  12049  egt2lt3  12062  n2dvds1  12194  flodddiv4  12218  0bits  12241  gcdf  12264  nninfct  12333  eucalgf  12348  2prm  12420  dfphi2  12513  pockthi  12652  karatsuba  12724  znnen  12740  ennnfonelem1  12749  qnnen  12773  ctiunct  12782  ssnnctlemct  12788  structcnvcnv  12819  structfn  12822  relelbasov  12865  xpsff1o  13152  rmodislmod  14084  cnfld0  14304  cnfld1  14305  eltpsi  14484  unitg  14505  epttop  14533  txuni2  14699  retopon  14969  cnfldtopon  14983  dedekindicclemicc  15075  reldvg  15122  dvrecap  15156  dvef  15170  plyrecj  15206  sinhalfpilem  15234  coseq00topi  15278  coseq0negpitopi  15279  sincos4thpi  15283  sincos6thpi  15285  pigt3  15287  cos02pilt1  15294  logltb  15317  rpabscxpbnd  15383  sgmf  15429  1sgm2ppw  15438  lgsdir2lem2  15477  lgsdir2lem3  15478  ex-fl  15623  ex-exp  15625  bdceqi  15741  bdcriota  15781  bdsepnfALT  15787  bdbm1.3ii  15789  bj-d0clsepcl  15823  nninfsellemeqinf  15915