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

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used 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  3740  rabrsndc  3779  rintm  4105  breqtri  4155  bm1.3ii  4254  zfnuleu  4257  zfpow  4312  undifexmid  4330  copsexg  4384  uniop  4396  pwundifss  4430  onunisuci  4577  zfun  4579  op1stb  4624  op1stbg  4625  ordtriexmidlem  4666  ordtriexmid  4668  ordtri2orexmid  4670  2ordpr  4671  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  dtruex  4706  ordsoexmid  4709  0elsucexmid  4712  ordtri2or2exmid  4718  dcextest  4728  tfi  4729  relop  4930  dmxpid  5003  rn0  5038  dmresi  5118  issref  5170  cnvcnv  5240  rescnvcnv  5250  cnvcnvres  5251  cnvsn  5270  cocnvcnv2  5299  cores2  5300  co01  5302  relcoi1  5319  cnviinm  5329  fnopab  5508  mpt0  5511  fnmpti  5512  f1cnvcnv  5609  f1ovi  5680  fmpti  5860  fvsnun2  5913  rinvf1o  6035  oprabss  6174  relmptopab  6291  2nd0  6379  f1stres  6393  f2ndres  6394  reldmtpos  6524  dftpos4  6534  tpostpos  6535  tpos0  6545  smo0  6569  frecfnom  6672  oasuc  6737  uniixp  7003  ssdomg  7065  xpcomf1o  7123  ssfilem  7177  diffitest  7191  inffiexmid  7213  fiintim  7238  caseinl  7432  caseinr  7433  eninl  7438  eninr  7439  card0  7534  dju1p1e2  7550  pw1on  7586  dmaddpi  7693  dmmulpi  7694  1lt2pi  7708  1lt2nq  7774  suplocsrlempr  8175  gtso  8405  subf  8530  negne0i  8603  negdii  8612  ltapii  8966  sup3exmid  9290  neg1ap0  9416  halflt1  9527  nn0ssz  9667  3halfnz  9748  zeo  9756  numlt  9811  numltc  9812  le9lt10  9813  decle  9820  uzf  9934  indstr  10003  infrenegsupex  10004  xaddf  10257  ixxf  10311  iooval2  10328  ioof  10384  unirnioo  10386  fzval2  10425  fzf  10426  fz10  10461  fz00m1  10462  fzpreddisj  10489  4fvwrd4  10558  fzof  10562  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  xnn0nnen  10889  hashfibc  11299  sqrt2gt1lt2  11831  infxrnegsupex  12048  fclim  12079  fsumrelem  12257  arisum2  12285  geo2sum2  12301  0.999...  12307  ege2le3  12457  sin0  12515  ef01bndlem  12542  cos2bnd  12546  cos01gt0  12549  sincos2sgn  12552  sin4lt0  12553  egt2lt3  12566  n2dvds1  12698  flodddiv4  12722  0bits  12745  gcdf  12768  nninfct  12837  eucalgf  12852  2prm  12924  dfphi2  13021  pockthi  13160  karatsuba  13233  1259lem5  13269  ballotfilem2  13280  ballotfilem4  13293  ballotfilem5  13294  ballotfilemi1  13297  ballotfilem7  13331  ballotfilemth  13333  znnen  13341  ennnfonelem1  13350  qnnen  13374  ctiunct  13383  ssnnctlemct  13389  structcnvcnv  13420  structfn  13423  relelbasov  13468  xpsff1o  13723  rmodislmod  14772  cnfld0  14992  cnfld1  14993  eltpsi  15233  unitg  15254  epttop  15282  txuni2  15448  retopon  15718  cnfldtopon  15732  dedekindicclemicc  15824  reldvg  15871  dvrecap  15905  dvef  15919  plyrecj  15955  sinhalfpilem  15984  coseq00topi  16028  coseq0negpitopi  16029  sincos4thpi  16033  sincos6thpi  16035  pigt3  16037  cos02pilt1  16044  logltb  16068  rpabscxpbnd  16137  log2ublog2  16185  birthdaylog2  16189  sgmf  16216  ppi1  16231  cht1  16232  1sgm2ppw  16250  ppiublem1  16252  ppiublem2  16253  ppiqub  16254  chtqub  16257  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsdir2lem2  16314  lgsdir2lem3  16315  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem4  16898  konigsberglem5  16899  konigsberg  16900  ex-fl  16905  ex-exp  16907  bdceqi  17035  bdcriota  17075  bdsepnfALT  17081  bdbm1.3ii  17083  bj-d0clsepcl  17117  nninfsellemeqinf  17225