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  1863  dveeq2or  1864  sbequilem  1886  nfsb  1999  sbco  2021  sbcocom  2023  hbsbd  2035  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  hbe1a  2076  elsb1  2209  elsb2  2210  eqcomi  2235  eqtri  2252  eleqtri  2306  neii  2405  neeqtri  2430  nesymi  2449  necomi  2488  nemtbir  2492  neli  2500  nrex  2625  rexlimi  2644  isseti  2812  eueq1  2979  euxfr2dc  2992  cdeqri  3018  sseqtri  3262  3sstr3i  3268  equncomi  3355  unssi  3384  ssini  3432  unabs  3440  inabs  3441  ddifss  3447  inssddif  3450  snid  3704  rabrsndc  3743  rintm  4068  breqtri  4118  bm1.3ii  4215  zfnuleu  4218  zfpow  4271  undifexmid  4289  copsexg  4342  uniop  4354  pwundifss  4388  onunisuci  4535  zfun  4537  op1stb  4581  op1stbg  4582  ordtriexmidlem  4623  ordtriexmid  4625  ordtri2orexmid  4627  2ordpr  4628  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmid  4634  dtruex  4663  ordsoexmid  4666  0elsucexmid  4669  ordtri2or2exmid  4675  dcextest  4685  tfi  4686  relop  4886  dmxpid  4959  rn0  4994  dmresi  5074  issref  5126  cnvcnv  5196  rescnvcnv  5206  cnvcnvres  5207  cnvsn  5226  cocnvcnv2  5255  cores2  5256  co01  5258  relcoi1  5275  cnviinm  5285  fnopab  5464  mpt0  5467  fnmpti  5468  f1cnvcnv  5562  f1ovi  5633  fmpti  5807  fvsnun2  5860  oprabss  6117  relmptopab  6234  2nd0  6317  f1stres  6331  f2ndres  6332  reldmtpos  6462  dftpos4  6472  tpostpos  6473  tpos0  6483  smo0  6507  frecfnom  6610  oasuc  6675  uniixp  6933  ssdomg  6995  xpcomf1o  7052  ssfilem  7105  diffitest  7119  inffiexmid  7141  fiintim  7166  caseinl  7333  caseinr  7334  eninl  7339  eninr  7340  card0  7435  dju1p1e2  7451  pw1on  7487  dmaddpi  7588  dmmulpi  7589  1lt2pi  7603  1lt2nq  7669  suplocsrlempr  8070  gtso  8300  subf  8423  negne0i  8496  negdii  8505  ltapii  8857  sup3exmid  9179  neg1ap0  9294  halflt1  9403  nn0ssz  9541  3halfnz  9621  zeo  9629  numlt  9679  numltc  9680  le9lt10  9681  decle  9688  uzf  9802  indstr  9871  infrenegsupex  9872  xaddf  10123  ixxf  10177  iooval2  10194  ioof  10250  unirnioo  10252  fzval2  10291  fzf  10292  fz10  10326  fzpreddisj  10351  4fvwrd4  10420  fzof  10424  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  xnn0nnen  10745  sqrt2gt1lt2  11672  infxrnegsupex  11886  fclim  11917  fsumrelem  12095  arisum2  12123  geo2sum2  12139  0.999...  12145  ege2le3  12295  sin0  12353  ef01bndlem  12380  cos2bnd  12384  cos01gt0  12387  sincos2sgn  12390  sin4lt0  12391  egt2lt3  12404  n2dvds1  12536  flodddiv4  12560  0bits  12583  gcdf  12606  nninfct  12675  eucalgf  12690  2prm  12762  dfphi2  12855  pockthi  12994  karatsuba  13066  znnen  13082  ennnfonelem1  13091  qnnen  13115  ctiunct  13124  ssnnctlemct  13130  structcnvcnv  13161  structfn  13164  relelbasov  13208  xpsff1o  13495  rmodislmod  14430  cnfld0  14650  cnfld1  14651  eltpsi  14835  unitg  14856  epttop  14884  txuni2  15050  retopon  15320  cnfldtopon  15334  dedekindicclemicc  15426  reldvg  15473  dvrecap  15507  dvef  15521  plyrecj  15557  sinhalfpilem  15585  coseq00topi  15629  coseq0negpitopi  15630  sincos4thpi  15634  sincos6thpi  15636  pigt3  15638  cos02pilt1  15645  logltb  15668  rpabscxpbnd  15734  sgmf  15783  1sgm2ppw  15792  lgsdir2lem2  15831  lgsdir2lem3  15832  konigsbergiedgwen  16408  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem4  16415  konigsberglem5  16416  konigsberg  16417  ex-fl  16422  ex-exp  16424  bdceqi  16542  bdcriota  16582  bdsepnfALT  16588  bdbm1.3ii  16590  bj-d0clsepcl  16624  nninfsellemeqinf  16725