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  7431  caseinr  7432  eninl  7437  eninr  7438  card0  7533  dju1p1e2  7549  pw1on  7585  dmaddpi  7692  dmmulpi  7693  1lt2pi  7707  1lt2nq  7773  suplocsrlempr  8174  gtso  8404  subf  8529  negne0i  8602  negdii  8611  ltapii  8965  sup3exmid  9289  neg1ap0  9415  halflt1  9526  nn0ssz  9666  3halfnz  9747  zeo  9755  numlt  9810  numltc  9811  le9lt10  9812  decle  9819  uzf  9933  indstr  10002  infrenegsupex  10003  xaddf  10256  ixxf  10310  iooval2  10327  ioof  10383  unirnioo  10385  fzval2  10424  fzf  10425  fz10  10460  fz00m1  10461  fzpreddisj  10488  4fvwrd4  10557  fzof  10561  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  xnn0nnen  10887  hashfibc  11297  sqrt2gt1lt2  11829  infxrnegsupex  12045  fclim  12076  fsumrelem  12254  arisum2  12282  geo2sum2  12298  0.999...  12304  ege2le3  12454  sin0  12512  ef01bndlem  12539  cos2bnd  12543  cos01gt0  12546  sincos2sgn  12549  sin4lt0  12550  egt2lt3  12563  n2dvds1  12695  flodddiv4  12719  0bits  12742  gcdf  12765  nninfct  12834  eucalgf  12849  2prm  12921  dfphi2  13018  pockthi  13157  karatsuba  13230  1259lem5  13266  ballotfilem2  13277  ballotfilem4  13290  ballotfilem5  13291  ballotfilemi1  13294  ballotfilem7  13328  ballotfilemth  13330  znnen  13338  ennnfonelem1  13347  qnnen  13371  ctiunct  13380  ssnnctlemct  13386  structcnvcnv  13417  structfn  13420  relelbasov  13465  xpsff1o  13719  rmodislmod  14737  cnfld0  14957  cnfld1  14958  eltpsi  15191  unitg  15212  epttop  15240  txuni2  15406  retopon  15676  cnfldtopon  15690  dedekindicclemicc  15782  reldvg  15829  dvrecap  15863  dvef  15877  plyrecj  15913  sinhalfpilem  15942  coseq00topi  15986  coseq0negpitopi  15987  sincos4thpi  15991  sincos6thpi  15993  pigt3  15995  cos02pilt1  16002  logltb  16026  rpabscxpbnd  16095  log2ublog2  16143  birthdaylog2  16147  sgmf  16167  ppi1  16176  1sgm2ppw  16190  ppiublem1  16192  ppiublem2  16193  ppiqub  16194  lgsdir2lem2  16246  lgsdir2lem3  16247  konigsbergiedgwen  16823  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem4  16830  konigsberglem5  16831  konigsberg  16832  ex-fl  16837  ex-exp  16839  bdceqi  16967  bdcriota  17007  bdsepnfALT  17013  bdbm1.3ii  17015  bj-d0clsepcl  17049  nninfsellemeqinf  17157