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  613  pm3.24  694  olc  712  orc  713  dcnn  849  dn1dc  962  3ori  1311  mptxor  1435  mpgbi  1466  dveeq2  1829  dveeq2or  1830  sbequilem  1852  nfsb  1965  sbco  1987  sbcocom  1989  hbsbd  2001  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  hbe1a  2042  elsb1  2174  elsb2  2175  eqcomi  2200  eqtri  2217  eleqtri  2271  neii  2369  neeqtri  2394  nesymi  2413  necomi  2452  nemtbir  2456  neli  2464  nrex  2589  rexlimi  2607  isseti  2771  eueq1  2936  euxfr2dc  2949  cdeqri  2975  sseqtri  3218  3sstr3i  3224  equncomi  3310  unssi  3339  ssini  3387  unabs  3395  inabs  3396  ddifss  3402  inssddif  3405  snid  3654  rabrsndc  3691  rintm  4010  breqtri  4059  bm1.3ii  4155  zfnuleu  4158  zfpow  4209  undifexmid  4227  copsexg  4278  uniop  4289  pwundifss  4321  onunisuci  4468  zfun  4470  op1stb  4514  op1stbg  4515  ordtriexmidlem  4556  ordtriexmid  4558  ordtri2orexmid  4560  2ordpr  4561  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  dtruex  4596  ordsoexmid  4599  0elsucexmid  4602  ordtri2or2exmid  4608  dcextest  4618  tfi  4619  relop  4817  dmxpid  4888  rn0  4923  dmresi  5002  issref  5053  cnvcnv  5123  rescnvcnv  5133  cnvcnvres  5134  cnvsn  5153  cocnvcnv2  5182  cores2  5183  co01  5185  relcoi1  5202  cnviinm  5212  fnopab  5385  mpt0  5388  fnmpti  5389  f1cnvcnv  5477  f1ovi  5546  fmpti  5717  fvsnun2  5763  oprabss  6012  2nd0  6212  f1stres  6226  f2ndres  6227  reldmtpos  6320  dftpos4  6330  tpostpos  6331  tpos0  6341  smo0  6365  frecfnom  6468  oasuc  6531  uniixp  6789  ssdomg  6846  xpcomf1o  6893  ssfilem  6945  diffitest  6957  inffiexmid  6976  fiintim  7001  caseinl  7166  caseinr  7167  eninl  7172  eninr  7173  card0  7266  dju1p1e2  7276  pw1on  7309  dmaddpi  7409  dmmulpi  7410  1lt2pi  7424  1lt2nq  7490  suplocsrlempr  7891  gtso  8122  subf  8245  negne0i  8318  negdii  8327  ltapii  8679  sup3exmid  9001  neg1ap0  9116  halflt1  9225  nn0ssz  9361  3halfnz  9440  zeo  9448  numlt  9498  numltc  9499  le9lt10  9500  decle  9507  uzf  9621  indstr  9684  infrenegsupex  9685  xaddf  9936  ixxf  9990  iooval2  10007  ioof  10063  unirnioo  10065  fzval2  10103  fzf  10104  fz10  10138  fzpreddisj  10163  4fvwrd4  10232  fzof  10236  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  xnn0nnen  10546  sqrt2gt1lt2  11231  infxrnegsupex  11445  fclim  11476  fsumrelem  11653  arisum2  11681  geo2sum2  11697  0.999...  11703  ege2le3  11853  sin0  11911  ef01bndlem  11938  cos2bnd  11942  cos01gt0  11945  sincos2sgn  11948  sin4lt0  11949  egt2lt3  11962  n2dvds1  12094  flodddiv4  12118  0bits  12141  gcdf  12164  nninfct  12233  eucalgf  12248  2prm  12320  dfphi2  12413  pockthi  12552  karatsuba  12624  znnen  12640  ennnfonelem1  12649  qnnen  12673  ctiunct  12682  ssnnctlemct  12688  structcnvcnv  12719  structfn  12722  relelbasov  12765  xpsff1o  13051  rmodislmod  13983  cnfld0  14203  cnfld1  14204  eltpsi  14361  unitg  14382  epttop  14410  txuni2  14576  retopon  14846  cnfldtopon  14860  dedekindicclemicc  14952  reldvg  14999  dvrecap  15033  dvef  15047  plyrecj  15083  sinhalfpilem  15111  coseq00topi  15155  coseq0negpitopi  15156  sincos4thpi  15160  sincos6thpi  15162  pigt3  15164  cos02pilt1  15171  logltb  15194  rpabscxpbnd  15260  sgmf  15306  1sgm2ppw  15315  lgsdir2lem2  15354  lgsdir2lem3  15355  ex-fl  15455  ex-exp  15457  bdceqi  15573  bdcriota  15613  bdsepnfALT  15619  bdbm1.3ii  15621  bj-d0clsepcl  15655  nninfsellemeqinf  15747