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  617  pm3.24  701  olc  719  orc  720  dcnn  856  dn1dc  969  3ori  1337  mptxor  1469  mpgbi  1501  dveeq2  1864  dveeq2or  1865  sbequilem  1887  nfsb  2002  sbco  2024  sbcocom  2026  hbsbd  2038  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  hbe1a  2079  elsb1  2212  elsb2  2213  eqcomi  2238  eqtri  2255  eleqtri  2309  neii  2416  neeqtri  2441  nesymi  2460  necomi  2499  nemtbir  2503  neli  2511  nrex  2636  rexlimi  2655  isseti  2824  eueq1  2992  euxfr2dc  3005  cdeqri  3031  sseqtri  3276  3sstr3i  3282  equncomi  3369  unssi  3398  ssini  3448  unabs  3456  inabs  3457  ddifss  3463  inssddif  3466  snid  3725  rabrsndc  3764  rintm  4089  breqtri  4139  bm1.3ii  4236  zfnuleu  4239  zfpow  4293  undifexmid  4311  copsexg  4365  uniop  4377  pwundifss  4411  onunisuci  4558  zfun  4560  op1stb  4604  op1stbg  4605  ordtriexmidlem  4646  ordtriexmid  4648  ordtri2orexmid  4650  2ordpr  4651  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  dtruex  4686  ordsoexmid  4689  0elsucexmid  4692  ordtri2or2exmid  4698  dcextest  4708  tfi  4709  relop  4910  dmxpid  4983  rn0  5018  dmresi  5098  issref  5150  cnvcnv  5220  rescnvcnv  5230  cnvcnvres  5231  cnvsn  5250  cocnvcnv2  5279  cores2  5280  co01  5282  relcoi1  5299  cnviinm  5309  fnopab  5488  mpt0  5491  fnmpti  5492  f1cnvcnv  5589  f1ovi  5660  fmpti  5834  fvsnun2  5887  rinvf1o  6008  oprabss  6147  relmptopab  6264  2nd0  6352  f1stres  6366  f2ndres  6367  reldmtpos  6497  dftpos4  6507  tpostpos  6508  tpos0  6518  smo0  6542  frecfnom  6645  oasuc  6710  uniixp  6969  ssdomg  7031  xpcomf1o  7089  ssfilem  7143  diffitest  7157  inffiexmid  7179  fiintim  7204  caseinl  7395  caseinr  7396  eninl  7401  eninr  7402  card0  7497  dju1p1e2  7513  pw1on  7549  dmaddpi  7656  dmmulpi  7657  1lt2pi  7671  1lt2nq  7737  suplocsrlempr  8138  gtso  8368  subf  8491  negne0i  8564  negdii  8573  ltapii  8926  sup3exmid  9248  neg1ap0  9363  halflt1  9472  nn0ssz  9612  3halfnz  9693  zeo  9701  numlt  9751  numltc  9752  le9lt10  9753  decle  9760  uzf  9874  indstr  9943  infrenegsupex  9944  xaddf  10196  ixxf  10250  iooval2  10267  ioof  10323  unirnioo  10325  fzval2  10364  fzf  10365  fz10  10400  fzpreddisj  10427  4fvwrd4  10496  fzof  10500  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  xnn0nnen  10823  hashfibc  11232  sqrt2gt1lt2  11759  infxrnegsupex  11973  fclim  12004  fsumrelem  12182  arisum2  12210  geo2sum2  12226  0.999...  12232  ege2le3  12382  sin0  12440  ef01bndlem  12467  cos2bnd  12471  cos01gt0  12474  sincos2sgn  12477  sin4lt0  12478  egt2lt3  12491  n2dvds1  12623  flodddiv4  12647  0bits  12670  gcdf  12693  nninfct  12762  eucalgf  12777  2prm  12849  dfphi2  12942  pockthi  13081  karatsuba  13153  ballotfilem2  13172  ballotfilem4  13185  ballotfilem5  13186  ballotfilemi1  13189  ballotfilem7  13223  ballotfilemth  13225  znnen  13233  ennnfonelem1  13242  qnnen  13266  ctiunct  13275  ssnnctlemct  13281  structcnvcnv  13312  structfn  13315  relelbasov  13359  xpsff1o  13613  rmodislmod  14625  cnfld0  14845  cnfld1  14846  eltpsi  15032  unitg  15053  epttop  15081  txuni2  15247  retopon  15517  cnfldtopon  15531  dedekindicclemicc  15623  reldvg  15670  dvrecap  15704  dvef  15718  plyrecj  15754  sinhalfpilem  15782  coseq00topi  15826  coseq0negpitopi  15827  sincos4thpi  15831  sincos6thpi  15833  pigt3  15835  cos02pilt1  15842  logltb  15865  rpabscxpbnd  15931  sgmf  15980  1sgm2ppw  15989  lgsdir2lem2  16028  lgsdir2lem3  16029  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem4  16612  konigsberglem5  16613  konigsberg  16614  ex-fl  16619  ex-exp  16621  bdceqi  16739  bdcriota  16779  bdsepnfALT  16785  bdbm1.3ii  16787  bj-d0clsepcl  16821  nninfsellemeqinf  16920