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  2809  eueq1  2976  euxfr2dc  2989  cdeqri  3015  sseqtri  3259  3sstr3i  3265  equncomi  3351  unssi  3380  ssini  3428  unabs  3436  inabs  3437  ddifss  3443  inssddif  3446  snid  3698  rabrsndc  3737  rintm  4061  breqtri  4111  bm1.3ii  4208  zfnuleu  4211  zfpow  4263  undifexmid  4281  copsexg  4334  uniop  4346  pwundifss  4380  onunisuci  4527  zfun  4529  op1stb  4573  op1stbg  4574  ordtriexmidlem  4615  ordtriexmid  4617  ordtri2orexmid  4619  2ordpr  4620  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmid  4626  dtruex  4655  ordsoexmid  4658  0elsucexmid  4661  ordtri2or2exmid  4667  dcextest  4677  tfi  4678  relop  4878  dmxpid  4951  rn0  4986  dmresi  5066  issref  5117  cnvcnv  5187  rescnvcnv  5197  cnvcnvres  5198  cnvsn  5217  cocnvcnv2  5246  cores2  5247  co01  5249  relcoi1  5266  cnviinm  5276  fnopab  5454  mpt0  5457  fnmpti  5458  f1cnvcnv  5550  f1ovi  5620  fmpti  5795  fvsnun2  5847  oprabss  6102  relmptopab  6219  2nd0  6303  f1stres  6317  f2ndres  6318  reldmtpos  6414  dftpos4  6424  tpostpos  6425  tpos0  6435  smo0  6459  frecfnom  6562  oasuc  6627  uniixp  6885  ssdomg  6947  xpcomf1o  7004  ssfilem  7057  diffitest  7069  inffiexmid  7091  fiintim  7116  caseinl  7281  caseinr  7282  eninl  7287  eninr  7288  card0  7383  dju1p1e2  7398  pw1on  7434  dmaddpi  7535  dmmulpi  7536  1lt2pi  7550  1lt2nq  7616  suplocsrlempr  8017  gtso  8248  subf  8371  negne0i  8444  negdii  8453  ltapii  8805  sup3exmid  9127  neg1ap0  9242  halflt1  9351  nn0ssz  9487  3halfnz  9567  zeo  9575  numlt  9625  numltc  9626  le9lt10  9627  decle  9634  uzf  9748  indstr  9817  infrenegsupex  9818  xaddf  10069  ixxf  10123  iooval2  10140  ioof  10196  unirnioo  10198  fzval2  10236  fzf  10237  fz10  10271  fzpreddisj  10296  4fvwrd4  10365  fzof  10369  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  xnn0nnen  10689  sqrt2gt1lt2  11600  infxrnegsupex  11814  fclim  11845  fsumrelem  12022  arisum2  12050  geo2sum2  12066  0.999...  12072  ege2le3  12222  sin0  12280  ef01bndlem  12307  cos2bnd  12311  cos01gt0  12314  sincos2sgn  12317  sin4lt0  12318  egt2lt3  12331  n2dvds1  12463  flodddiv4  12487  0bits  12510  gcdf  12533  nninfct  12602  eucalgf  12617  2prm  12689  dfphi2  12782  pockthi  12921  karatsuba  12993  znnen  13009  ennnfonelem1  13018  qnnen  13042  ctiunct  13051  ssnnctlemct  13057  structcnvcnv  13088  structfn  13091  relelbasov  13135  xpsff1o  13422  rmodislmod  14355  cnfld0  14575  cnfld1  14576  eltpsi  14755  unitg  14776  epttop  14804  txuni2  14970  retopon  15240  cnfldtopon  15254  dedekindicclemicc  15346  reldvg  15393  dvrecap  15427  dvef  15441  plyrecj  15477  sinhalfpilem  15505  coseq00topi  15549  coseq0negpitopi  15550  sincos4thpi  15554  sincos6thpi  15556  pigt3  15558  cos02pilt1  15565  logltb  15588  rpabscxpbnd  15654  sgmf  15700  1sgm2ppw  15709  lgsdir2lem2  15748  lgsdir2lem3  15749  ex-fl  16257  ex-exp  16259  bdceqi  16374  bdcriota  16414  bdsepnfALT  16420  bdbm1.3ii  16422  bj-d0clsepcl  16456  nninfsellemeqinf  16554