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  4057  breqtri  4107  bm1.3ii  4204  zfnuleu  4207  zfpow  4258  undifexmid  4276  copsexg  4329  uniop  4341  pwundifss  4375  onunisuci  4522  zfun  4524  op1stb  4568  op1stbg  4569  ordtriexmidlem  4610  ordtriexmid  4612  ordtri2orexmid  4614  2ordpr  4615  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmid  4621  dtruex  4650  ordsoexmid  4653  0elsucexmid  4656  ordtri2or2exmid  4662  dcextest  4672  tfi  4673  relop  4871  dmxpid  4944  rn0  4979  dmresi  5059  issref  5110  cnvcnv  5180  rescnvcnv  5190  cnvcnvres  5191  cnvsn  5210  cocnvcnv2  5239  cores2  5240  co01  5242  relcoi1  5259  cnviinm  5269  fnopab  5447  mpt0  5450  fnmpti  5451  f1cnvcnv  5541  f1ovi  5611  fmpti  5786  fvsnun2  5836  oprabss  6089  2nd0  6289  f1stres  6303  f2ndres  6304  reldmtpos  6397  dftpos4  6407  tpostpos  6408  tpos0  6418  smo0  6442  frecfnom  6545  oasuc  6608  uniixp  6866  ssdomg  6928  xpcomf1o  6980  ssfilem  7033  diffitest  7045  inffiexmid  7064  fiintim  7089  caseinl  7254  caseinr  7255  eninl  7260  eninr  7261  card0  7356  dju1p1e2  7371  pw1on  7407  dmaddpi  7508  dmmulpi  7509  1lt2pi  7523  1lt2nq  7589  suplocsrlempr  7990  gtso  8221  subf  8344  negne0i  8417  negdii  8426  ltapii  8778  sup3exmid  9100  neg1ap0  9215  halflt1  9324  nn0ssz  9460  3halfnz  9540  zeo  9548  numlt  9598  numltc  9599  le9lt10  9600  decle  9607  uzf  9721  indstr  9784  infrenegsupex  9785  xaddf  10036  ixxf  10090  iooval2  10107  ioof  10163  unirnioo  10165  fzval2  10203  fzf  10204  fz10  10238  fzpreddisj  10263  4fvwrd4  10332  fzof  10336  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  xnn0nnen  10654  sqrt2gt1lt2  11555  infxrnegsupex  11769  fclim  11800  fsumrelem  11977  arisum2  12005  geo2sum2  12021  0.999...  12027  ege2le3  12177  sin0  12235  ef01bndlem  12262  cos2bnd  12266  cos01gt0  12269  sincos2sgn  12272  sin4lt0  12273  egt2lt3  12286  n2dvds1  12418  flodddiv4  12442  0bits  12465  gcdf  12488  nninfct  12557  eucalgf  12572  2prm  12644  dfphi2  12737  pockthi  12876  karatsuba  12948  znnen  12964  ennnfonelem1  12973  qnnen  12997  ctiunct  13006  ssnnctlemct  13012  structcnvcnv  13043  structfn  13046  relelbasov  13090  xpsff1o  13377  rmodislmod  14309  cnfld0  14529  cnfld1  14530  eltpsi  14709  unitg  14730  epttop  14758  txuni2  14924  retopon  15194  cnfldtopon  15208  dedekindicclemicc  15300  reldvg  15347  dvrecap  15381  dvef  15395  plyrecj  15431  sinhalfpilem  15459  coseq00topi  15503  coseq0negpitopi  15504  sincos4thpi  15508  sincos6thpi  15510  pigt3  15512  cos02pilt1  15519  logltb  15542  rpabscxpbnd  15608  sgmf  15654  1sgm2ppw  15663  lgsdir2lem2  15702  lgsdir2lem3  15703  ex-fl  16047  ex-exp  16049  bdceqi  16164  bdcriota  16204  bdsepnfALT  16210  bdbm1.3ii  16212  bj-d0clsepcl  16246  nninfsellemeqinf  16341