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

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.74i  180  pm4.71i  395  pm4.71ri  396  pm5.32i  458  biadanii  621  pm3.24  705  olc  723  orc  724  dcnn  860  dn1dc  973  3ori  1341  mptxor  1473  mpgbi  1505  dveeq2  1868  dveeq2or  1869  sbequilem  1891  nfsb  2006  sbco  2028  sbcocom  2030  hbsbd  2042  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  hbe1a  2083  elsb1  2216  elsb2  2217  eqcomi  2242  eqtri  2259  eleqtri  2313  neii  2422  neeqtri  2447  nesymi  2466  necomi  2505  nemtbir  2509  neli  2517  nrex  2642  rexlimi  2661  isseti  2830  eueq1  2998  euxfr2dc  3011  cdeqri  3037  sseqtri  3282  3sstr3i  3288  equncomi  3375  unssi  3404  ssini  3454  unabs  3462  inabs  3463  ddifss  3469  inssddif  3472  snid  3740  rabrsndc  3779  rintm  4105  breqtri  4156  bm1.3ii  4256  zfnuleu  4259  zfpow  4314  undifexmid  4332  copsexg  4386  uniop  4398  pwundifss  4432  onunisuci  4579  zfun  4581  op1stb  4626  op1stbg  4627  ordtriexmidlem  4668  ordtriexmid  4670  ordtri2orexmid  4672  2ordpr  4673  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  dtruex  4708  ordsoexmid  4711  0elsucexmid  4714  ordtri2or2exmid  4720  dcextest  4730  tfi  4731  relop  4932  dmxpid  5005  rn0  5040  dmresi  5121  issref  5173  cnvcnv  5243  rescnvcnv  5253  cnvcnvres  5254  cnvsn  5273  cocnvcnv2  5302  cores2  5303  co01  5305  relcoi1  5322  cnviinm  5332  fnopab  5511  mpt0  5514  fnmpti  5515  f1cnvcnv  5612  f1ovi  5683  fmpti  5863  fvsnun2  5916  rinvf1o  6038  oprabss  6177  relmptopab  6294  2nd0  6383  f1stres  6397  f2ndres  6398  reldmtpos  6529  dftpos4  6539  tpostpos  6540  tpos0  6550  smo0  6574  frecfnom  6677  oasuc  6742  uniixp  7009  ssdomg  7071  xpcomf1o  7129  ssfilem  7183  diffitest  7197  inffiexmid  7219  fiintim  7244  caseinl  7437  caseinr  7438  eninl  7443  eninr  7444  card0  7539  dju1p1e2  7555  pw1on  7591  dmaddpi  7698  dmmulpi  7699  1lt2pi  7713  1lt2nq  7779  suplocsrlempr  8180  gtso  8410  subf  8535  negne0i  8608  negdii  8617  ltapii  8971  sup3exmid  9295  neg1ap0  9422  halflt1  9533  nn0ssz  9671  3halfnz  9753  zeo  9761  numlt  9816  numltc  9817  le9lt10  9818  decle  9825  uzf  9939  indstr  10008  infrenegsupex  10009  xaddf  10262  ixxf  10316  iooval2  10333  ioof  10389  unirnioo  10391  fzval2  10430  fzf  10431  fz10  10466  fz00m1  10467  fzpreddisj  10494  4fvwrd4  10563  fzof  10567  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  xnn0nnen  10894  hashfibc  11304  sqrt2gt1lt2  11836  infxrnegsupex  12053  fclim  12084  fsumrelem  12262  arisum2  12290  geo2sum2  12306  0.999...  12312  ege2le3  12462  sin0  12520  ef01bndlem  12547  cos2bnd  12551  cos01gt0  12554  sincos2sgn  12557  sin4lt0  12558  egt2lt3  12571  n2dvds1  12703  flodddiv4  12727  0bits  12750  gcdf  12773  nninfct  12842  eucalgf  12857  2prm  12929  dfphi2  13026  pockthi  13165  karatsuba  13238  1259lem5  13274  ballotfilem2  13285  ballotfilem4  13298  ballotfilem5  13299  ballotfilemi1  13302  ballotfilem7  13336  ballotfilemth  13338  znnen  13346  ennnfonelem1  13355  qnnen  13379  ctiunct  13388  ssnnctlemct  13394  structcnvcnv  13425  structfn  13428  relelbasov  13473  xpsff1o  13728  rmodislmod  14796  cnfld0  15016  cnfld1  15017  eltpsi  15284  unitg  15305  epttop  15333  txuni2  15499  retopon  15769  cnfldtopon  15783  dedekindicclemicc  15875  reldvg  15922  dvrecap  15956  dvef  15970  plyrecj  16006  sinhalfpilem  16035  coseq00topi  16079  coseq0negpitopi  16080  sincos4thpi  16084  sincos6thpi  16086  pigt3  16088  cos02pilt1  16096  logltb  16121  rpabscxpbnd  16192  log2ublog2  16241  birthdaylog2  16245  sgmf  16272  ppi1  16287  cht1  16288  1sgm2ppw  16306  ppiublem1  16308  ppiublem2  16309  ppiqub  16310  chtqub  16313  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsdir2lem2  16370  lgsdir2lem3  16371  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem4  16954  konigsberglem5  16955  konigsberg  16956  ex-fl  16961  ex-exp  16963  bdceqi  17091  bdcriota  17131  bdsepnfALT  17137  bdbm1.3ii  17139  bj-d0clsepcl  17173  nninfsellemeqinf  17282