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  4155  bm1.3ii  4254  zfnuleu  4257  zfpow  4312  undifexmid  4330  copsexg  4384  uniop  4396  pwundifss  4430  onunisuci  4577  zfun  4579  op1stb  4624  op1stbg  4625  ordtriexmidlem  4666  ordtriexmid  4668  ordtri2orexmid  4670  2ordpr  4671  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  dtruex  4706  ordsoexmid  4709  0elsucexmid  4712  ordtri2or2exmid  4718  dcextest  4728  tfi  4729  relop  4930  dmxpid  5003  rn0  5038  dmresi  5118  issref  5170  cnvcnv  5240  rescnvcnv  5250  cnvcnvres  5251  cnvsn  5270  cocnvcnv2  5299  cores2  5300  co01  5302  relcoi1  5319  cnviinm  5329  fnopab  5508  mpt0  5511  fnmpti  5512  f1cnvcnv  5609  f1ovi  5680  fmpti  5860  fvsnun2  5913  rinvf1o  6035  oprabss  6174  relmptopab  6291  2nd0  6379  f1stres  6393  f2ndres  6394  reldmtpos  6524  dftpos4  6534  tpostpos  6535  tpos0  6545  smo0  6569  frecfnom  6672  oasuc  6737  uniixp  7003  ssdomg  7065  xpcomf1o  7123  ssfilem  7177  diffitest  7191  inffiexmid  7213  fiintim  7238  caseinl  7431  caseinr  7432  eninl  7437  eninr  7438  card0  7533  dju1p1e2  7549  pw1on  7585  dmaddpi  7692  dmmulpi  7693  1lt2pi  7707  1lt2nq  7773  suplocsrlempr  8174  gtso  8404  subf  8528  negne0i  8601  negdii  8610  ltapii  8963  sup3exmid  9287  neg1ap0  9413  halflt1  9522  nn0ssz  9662  3halfnz  9743  zeo  9751  numlt  9801  numltc  9802  le9lt10  9803  decle  9810  uzf  9924  indstr  9993  infrenegsupex  9994  xaddf  10246  ixxf  10300  iooval2  10317  ioof  10373  unirnioo  10375  fzval2  10414  fzf  10415  fz10  10450  fz00m1  10451  fzpreddisj  10478  4fvwrd4  10547  fzof  10551  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  xnn0nnen  10874  hashfibc  11283  sqrt2gt1lt2  11815  infxrnegsupex  12029  fclim  12060  fsumrelem  12238  arisum2  12266  geo2sum2  12282  0.999...  12288  ege2le3  12438  sin0  12496  ef01bndlem  12523  cos2bnd  12527  cos01gt0  12530  sincos2sgn  12533  sin4lt0  12534  egt2lt3  12547  n2dvds1  12679  flodddiv4  12703  0bits  12726  gcdf  12749  nninfct  12818  eucalgf  12833  2prm  12905  dfphi2  12998  pockthi  13137  karatsuba  13209  ballotfilem2  13228  ballotfilem4  13241  ballotfilem5  13242  ballotfilemi1  13245  ballotfilem7  13279  ballotfilemth  13281  znnen  13289  ennnfonelem1  13298  qnnen  13322  ctiunct  13331  ssnnctlemct  13337  structcnvcnv  13368  structfn  13371  relelbasov  13416  xpsff1o  13670  rmodislmod  14688  cnfld0  14908  cnfld1  14909  eltpsi  15142  unitg  15163  epttop  15191  txuni2  15357  retopon  15627  cnfldtopon  15641  dedekindicclemicc  15733  reldvg  15780  dvrecap  15814  dvef  15828  plyrecj  15864  sinhalfpilem  15892  coseq00topi  15936  coseq0negpitopi  15937  sincos4thpi  15941  sincos6thpi  15943  pigt3  15945  cos02pilt1  15952  logltb  15975  rpabscxpbnd  16042  log2ublog2  16086  birthdaylog2  16090  sgmf  16100  1sgm2ppw  16109  lgsdir2lem2  16148  lgsdir2lem3  16149  konigsbergiedgwen  16725  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem4  16732  konigsberglem5  16733  konigsberg  16734  ex-fl  16739  ex-exp  16741  bdceqi  16869  bdcriota  16909  bdsepnfALT  16915  bdbm1.3ii  16917  bj-d0clsepcl  16951  nninfsellemeqinf  17059