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  395  pm4.71ri  396  pm5.32i  458  biadanii  621  pm3.24  705  olc  723  orc  724  dcnn  860  dn1dc  973  3ori  1341  mptxor  1473  mpgbi  1505  dveeq2  1868  dveeq2or  1869  sbequilem  1891  nfsb  2006  sbco  2028  sbcocom  2030  hbsbd  2042  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  hbe1a  2083  elsb1  2216  elsb2  2217  eqcomi  2242  eqtri  2259  eleqtri  2313  neii  2422  neeqtri  2447  nesymi  2466  necomi  2505  nemtbir  2509  neli  2517  nrex  2642  rexlimi  2661  isseti  2830  eueq1  2998  euxfr2dc  3011  cdeqri  3037  sseqtri  3282  3sstr3i  3288  equncomi  3375  unssi  3404  ssini  3454  unabs  3462  inabs  3463  ddifss  3469  inssddif  3472  snid  3736  rabrsndc  3775  rintm  4100  breqtri  4150  bm1.3ii  4249  zfnuleu  4252  zfpow  4307  undifexmid  4325  copsexg  4379  uniop  4391  pwundifss  4425  onunisuci  4572  zfun  4574  op1stb  4619  op1stbg  4620  ordtriexmidlem  4661  ordtriexmid  4663  ordtri2orexmid  4665  2ordpr  4666  ontr2exmid  4667  onsucsssucexmid  4669  onsucelsucexmid  4672  dtruex  4701  ordsoexmid  4704  0elsucexmid  4707  ordtri2or2exmid  4713  dcextest  4723  tfi  4724  relop  4925  dmxpid  4998  rn0  5033  dmresi  5113  issref  5165  cnvcnv  5235  rescnvcnv  5245  cnvcnvres  5246  cnvsn  5265  cocnvcnv2  5294  cores2  5295  co01  5297  relcoi1  5314  cnviinm  5324  fnopab  5503  mpt0  5506  fnmpti  5507  f1cnvcnv  5604  f1ovi  5675  fmpti  5851  fvsnun2  5904  rinvf1o  6025  oprabss  6164  relmptopab  6281  2nd0  6369  f1stres  6383  f2ndres  6384  reldmtpos  6514  dftpos4  6524  tpostpos  6525  tpos0  6535  smo0  6559  frecfnom  6662  oasuc  6727  uniixp  6993  ssdomg  7055  xpcomf1o  7113  ssfilem  7167  diffitest  7181  inffiexmid  7203  fiintim  7228  caseinl  7421  caseinr  7422  eninl  7427  eninr  7428  card0  7523  dju1p1e2  7539  pw1on  7575  dmaddpi  7682  dmmulpi  7683  1lt2pi  7697  1lt2nq  7763  suplocsrlempr  8164  gtso  8394  subf  8518  negne0i  8591  negdii  8600  ltapii  8953  sup3exmid  9277  neg1ap0  9392  halflt1  9501  nn0ssz  9641  3halfnz  9722  zeo  9730  numlt  9780  numltc  9781  le9lt10  9782  decle  9789  uzf  9903  indstr  9972  infrenegsupex  9973  xaddf  10225  ixxf  10279  iooval2  10296  ioof  10352  unirnioo  10354  fzval2  10393  fzf  10394  fz10  10429  fzpreddisj  10456  4fvwrd4  10525  fzof  10529  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  xnn0nnen  10852  hashfibc  11261  sqrt2gt1lt2  11793  infxrnegsupex  12007  fclim  12038  fsumrelem  12216  arisum2  12244  geo2sum2  12260  0.999...  12266  ege2le3  12416  sin0  12474  ef01bndlem  12501  cos2bnd  12505  cos01gt0  12508  sincos2sgn  12511  sin4lt0  12512  egt2lt3  12525  n2dvds1  12657  flodddiv4  12681  0bits  12704  gcdf  12727  nninfct  12796  eucalgf  12811  2prm  12883  dfphi2  12976  pockthi  13115  karatsuba  13187  ballotfilem2  13206  ballotfilem4  13219  ballotfilem5  13220  ballotfilemi1  13223  ballotfilem7  13257  ballotfilemth  13259  znnen  13267  ennnfonelem1  13276  qnnen  13300  ctiunct  13309  ssnnctlemct  13315  structcnvcnv  13346  structfn  13349  relelbasov  13393  xpsff1o  13647  rmodislmod  14660  cnfld0  14880  cnfld1  14881  eltpsi  15065  unitg  15086  epttop  15114  txuni2  15280  retopon  15550  cnfldtopon  15564  dedekindicclemicc  15656  reldvg  15703  dvrecap  15737  dvef  15751  plyrecj  15787  sinhalfpilem  15815  coseq00topi  15859  coseq0negpitopi  15860  sincos4thpi  15864  sincos6thpi  15866  pigt3  15868  cos02pilt1  15875  logltb  15898  rpabscxpbnd  15965  sgmf  16014  1sgm2ppw  16023  lgsdir2lem2  16062  lgsdir2lem3  16063  konigsbergiedgwen  16639  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem4  16646  konigsberglem5  16647  konigsberg  16648  ex-fl  16653  ex-exp  16655  bdceqi  16783  bdcriota  16823  bdsepnfALT  16829  bdbm1.3ii  16831  bj-d0clsepcl  16865  nninfsellemeqinf  16964