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  615  pm3.24  698  olc  716  orc  717  dcnn  853  dn1dc  966  3ori  1334  mptxor  1466  mpgbi  1498  dveeq2  1861  dveeq2or  1862  sbequilem  1884  nfsb  1997  sbco  2019  sbcocom  2021  hbsbd  2033  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  hbe1a  2074  elsb1  2207  elsb2  2208  eqcomi  2233  eqtri  2250  eleqtri  2304  neii  2402  neeqtri  2427  nesymi  2446  necomi  2485  nemtbir  2489  neli  2497  nrex  2622  rexlimi  2641  isseti  2808  eueq1  2975  euxfr2dc  2988  cdeqri  3014  sseqtri  3258  3sstr3i  3264  equncomi  3350  unssi  3379  ssini  3427  unabs  3435  inabs  3436  ddifss  3442  inssddif  3445  snid  3697  rabrsndc  3734  rintm  4058  breqtri  4108  bm1.3ii  4205  zfnuleu  4208  zfpow  4259  undifexmid  4277  copsexg  4330  uniop  4342  pwundifss  4376  onunisuci  4523  zfun  4525  op1stb  4569  op1stbg  4570  ordtriexmidlem  4611  ordtriexmid  4613  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  dtruex  4651  ordsoexmid  4654  0elsucexmid  4657  ordtri2or2exmid  4663  dcextest  4673  tfi  4674  relop  4872  dmxpid  4945  rn0  4980  dmresi  5060  issref  5111  cnvcnv  5181  rescnvcnv  5191  cnvcnvres  5192  cnvsn  5211  cocnvcnv2  5240  cores2  5241  co01  5243  relcoi1  5260  cnviinm  5270  fnopab  5448  mpt0  5451  fnmpti  5452  f1cnvcnv  5544  f1ovi  5614  fmpti  5789  fvsnun2  5841  oprabss  6096  relmptopab  6213  2nd0  6297  f1stres  6311  f2ndres  6312  reldmtpos  6405  dftpos4  6415  tpostpos  6416  tpos0  6426  smo0  6450  frecfnom  6553  oasuc  6618  uniixp  6876  ssdomg  6938  xpcomf1o  6992  ssfilem  7045  diffitest  7057  inffiexmid  7079  fiintim  7104  caseinl  7269  caseinr  7270  eninl  7275  eninr  7276  card0  7371  dju1p1e2  7386  pw1on  7422  dmaddpi  7523  dmmulpi  7524  1lt2pi  7538  1lt2nq  7604  suplocsrlempr  8005  gtso  8236  subf  8359  negne0i  8432  negdii  8441  ltapii  8793  sup3exmid  9115  neg1ap0  9230  halflt1  9339  nn0ssz  9475  3halfnz  9555  zeo  9563  numlt  9613  numltc  9614  le9lt10  9615  decle  9622  uzf  9736  indstr  9800  infrenegsupex  9801  xaddf  10052  ixxf  10106  iooval2  10123  ioof  10179  unirnioo  10181  fzval2  10219  fzf  10220  fz10  10254  fzpreddisj  10279  4fvwrd4  10348  fzof  10352  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  xnn0nnen  10671  sqrt2gt1lt2  11575  infxrnegsupex  11789  fclim  11820  fsumrelem  11997  arisum2  12025  geo2sum2  12041  0.999...  12047  ege2le3  12197  sin0  12255  ef01bndlem  12282  cos2bnd  12286  cos01gt0  12289  sincos2sgn  12292  sin4lt0  12293  egt2lt3  12306  n2dvds1  12438  flodddiv4  12462  0bits  12485  gcdf  12508  nninfct  12577  eucalgf  12592  2prm  12664  dfphi2  12757  pockthi  12896  karatsuba  12968  znnen  12984  ennnfonelem1  12993  qnnen  13017  ctiunct  13026  ssnnctlemct  13032  structcnvcnv  13063  structfn  13066  relelbasov  13110  xpsff1o  13397  rmodislmod  14330  cnfld0  14550  cnfld1  14551  eltpsi  14730  unitg  14751  epttop  14779  txuni2  14945  retopon  15215  cnfldtopon  15229  dedekindicclemicc  15321  reldvg  15368  dvrecap  15402  dvef  15416  plyrecj  15452  sinhalfpilem  15480  coseq00topi  15524  coseq0negpitopi  15525  sincos4thpi  15529  sincos6thpi  15531  pigt3  15533  cos02pilt1  15540  logltb  15563  rpabscxpbnd  15629  sgmf  15675  1sgm2ppw  15684  lgsdir2lem2  15723  lgsdir2lem3  15724  ex-fl  16144  ex-exp  16146  bdceqi  16261  bdcriota  16301  bdsepnfALT  16307  bdbm1.3ii  16309  bj-d0clsepcl  16343  nninfsellemeqinf  16442