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  6528  dftpos4  6538  tpostpos  6539  tpos0  6549  smo0  6573  frecfnom  6676  oasuc  6741  uniixp  7007  ssdomg  7069  xpcomf1o  7127  ssfilem  7181  diffitest  7195  inffiexmid  7217  fiintim  7242  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  9673  3halfnz  9754  zeo  9762  numlt  9817  numltc  9818  le9lt10  9819  decle  9826  uzf  9940  indstr  10009  infrenegsupex  10010  xaddf  10263  ixxf  10317  iooval2  10334  ioof  10390  unirnioo  10392  fzval2  10431  fzf  10432  fz10  10467  fz00m1  10468  fzpreddisj  10495  4fvwrd4  10564  fzof  10568  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  xnn0nnen  10895  hashfibc  11305  sqrt2gt1lt2  11837  infxrnegsupex  12054  fclim  12085  fsumrelem  12263  arisum2  12291  geo2sum2  12307  0.999...  12313  ege2le3  12463  sin0  12521  ef01bndlem  12548  cos2bnd  12552  cos01gt0  12555  sincos2sgn  12558  sin4lt0  12559  egt2lt3  12572  n2dvds1  12704  flodddiv4  12728  0bits  12751  gcdf  12774  nninfct  12843  eucalgf  12858  2prm  12930  dfphi2  13027  pockthi  13166  karatsuba  13239  1259lem5  13275  ballotfilem2  13286  ballotfilem4  13299  ballotfilem5  13300  ballotfilemi1  13303  ballotfilem7  13337  ballotfilemth  13339  znnen  13347  ennnfonelem1  13356  qnnen  13380  ctiunct  13389  ssnnctlemct  13395  structcnvcnv  13426  structfn  13429  relelbasov  13474  xpsff1o  13729  rmodislmod  14797  cnfld0  15017  cnfld1  15018  eltpsi  15267  unitg  15288  epttop  15316  txuni2  15482  retopon  15752  cnfldtopon  15766  dedekindicclemicc  15858  reldvg  15905  dvrecap  15939  dvef  15953  plyrecj  15989  sinhalfpilem  16018  coseq00topi  16062  coseq0negpitopi  16063  sincos4thpi  16067  sincos6thpi  16069  pigt3  16071  cos02pilt1  16079  logltb  16104  rpabscxpbnd  16175  log2ublog2  16224  birthdaylog2  16228  sgmf  16255  ppi1  16270  cht1  16271  1sgm2ppw  16289  ppiublem1  16291  ppiublem2  16292  ppiqub  16293  chtqub  16296  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsdir2lem2  16353  lgsdir2lem3  16354  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem4  16937  konigsberglem5  16938  konigsberg  16939  ex-fl  16944  ex-exp  16946  bdceqi  17074  bdcriota  17114  bdsepnfALT  17120  bdbm1.3ii  17122  bj-d0clsepcl  17156  nninfsellemeqinf  17265