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  1475  dveeq2  1838  dveeq2or  1839  sbequilem  1861  nfsb  1974  sbco  1996  sbcocom  1998  hbsbd  2010  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  hbe1a  2051  elsb1  2183  elsb2  2184  eqcomi  2209  eqtri  2226  eleqtri  2280  neii  2378  neeqtri  2403  nesymi  2422  necomi  2461  nemtbir  2465  neli  2473  nrex  2598  rexlimi  2616  isseti  2780  eueq1  2945  euxfr2dc  2958  cdeqri  2984  sseqtri  3227  3sstr3i  3233  equncomi  3319  unssi  3348  ssini  3396  unabs  3404  inabs  3405  ddifss  3411  inssddif  3414  snid  3664  rabrsndc  3701  rintm  4020  breqtri  4069  bm1.3ii  4165  zfnuleu  4168  zfpow  4219  undifexmid  4237  copsexg  4288  uniop  4300  pwundifss  4332  onunisuci  4479  zfun  4481  op1stb  4525  op1stbg  4526  ordtriexmidlem  4567  ordtriexmid  4569  ordtri2orexmid  4571  2ordpr  4572  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmid  4578  dtruex  4607  ordsoexmid  4610  0elsucexmid  4613  ordtri2or2exmid  4619  dcextest  4629  tfi  4630  relop  4828  dmxpid  4899  rn0  4934  dmresi  5014  issref  5065  cnvcnv  5135  rescnvcnv  5145  cnvcnvres  5146  cnvsn  5165  cocnvcnv2  5194  cores2  5195  co01  5197  relcoi1  5214  cnviinm  5224  fnopab  5400  mpt0  5403  fnmpti  5404  f1cnvcnv  5492  f1ovi  5561  fmpti  5732  fvsnun2  5782  oprabss  6031  2nd0  6231  f1stres  6245  f2ndres  6246  reldmtpos  6339  dftpos4  6349  tpostpos  6350  tpos0  6360  smo0  6384  frecfnom  6487  oasuc  6550  uniixp  6808  ssdomg  6870  xpcomf1o  6920  ssfilem  6972  diffitest  6984  inffiexmid  7003  fiintim  7028  caseinl  7193  caseinr  7194  eninl  7199  eninr  7200  card0  7295  dju1p1e2  7305  pw1on  7338  dmaddpi  7438  dmmulpi  7439  1lt2pi  7453  1lt2nq  7519  suplocsrlempr  7920  gtso  8151  subf  8274  negne0i  8347  negdii  8356  ltapii  8708  sup3exmid  9030  neg1ap0  9145  halflt1  9254  nn0ssz  9390  3halfnz  9470  zeo  9478  numlt  9528  numltc  9529  le9lt10  9530  decle  9537  uzf  9651  indstr  9714  infrenegsupex  9715  xaddf  9966  ixxf  10020  iooval2  10037  ioof  10093  unirnioo  10095  fzval2  10133  fzf  10134  fz10  10168  fzpreddisj  10193  4fvwrd4  10262  fzof  10266  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  xnn0nnen  10582  sqrt2gt1lt2  11360  infxrnegsupex  11574  fclim  11605  fsumrelem  11782  arisum2  11810  geo2sum2  11826  0.999...  11832  ege2le3  11982  sin0  12040  ef01bndlem  12067  cos2bnd  12071  cos01gt0  12074  sincos2sgn  12077  sin4lt0  12078  egt2lt3  12091  n2dvds1  12223  flodddiv4  12247  0bits  12270  gcdf  12293  nninfct  12362  eucalgf  12377  2prm  12449  dfphi2  12542  pockthi  12681  karatsuba  12753  znnen  12769  ennnfonelem1  12778  qnnen  12802  ctiunct  12811  ssnnctlemct  12817  structcnvcnv  12848  structfn  12851  relelbasov  12894  xpsff1o  13181  rmodislmod  14113  cnfld0  14333  cnfld1  14334  eltpsi  14513  unitg  14534  epttop  14562  txuni2  14728  retopon  14998  cnfldtopon  15012  dedekindicclemicc  15104  reldvg  15151  dvrecap  15185  dvef  15199  plyrecj  15235  sinhalfpilem  15263  coseq00topi  15307  coseq0negpitopi  15308  sincos4thpi  15312  sincos6thpi  15314  pigt3  15316  cos02pilt1  15323  logltb  15346  rpabscxpbnd  15412  sgmf  15458  1sgm2ppw  15467  lgsdir2lem2  15506  lgsdir2lem3  15507  ex-fl  15661  ex-exp  15663  bdceqi  15779  bdcriota  15819  bdsepnfALT  15825  bdbm1.3ii  15827  bj-d0clsepcl  15861  nninfsellemeqinf  15953