Theorem mpbi 145

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbi.min	⊢ 𝜑
mpbi.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbi	⊢ 𝜓

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ 𝜑
2		mpbi.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpi 120	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

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  8528  negne0i  8601  negdii  8610  ltapii  8964  sup3exmid  9288  neg1ap0  9414  halflt1  9524  nn0ssz  9664  3halfnz  9745  zeo  9753  numlt  9803  numltc  9804  le9lt10  9805  decle  9812  uzf  9926  indstr  9995  infrenegsupex  9996  xaddf  10248  ixxf  10302  iooval2  10319  ioof  10375  unirnioo  10377  fzval2  10416  fzf  10417  fz10  10452  fz00m1  10453  fzpreddisj  10480  4fvwrd4  10549  fzof  10553  fldiv4p1lem1div2  10742  fldiv4lem1div2  10744  xnn0nnen  10876  hashfibc  11285  sqrt2gt1lt2  11817  infxrnegsupex  12031  fclim  12062  fsumrelem  12240  arisum2  12268  geo2sum2  12284  0.999...  12290  ege2le3  12440  sin0  12498  ef01bndlem  12525  cos2bnd  12529  cos01gt0  12532  sincos2sgn  12535  sin4lt0  12536  egt2lt3  12549  n2dvds1  12681  flodddiv4  12705  0bits  12728  gcdf  12751  nninfct  12820  eucalgf  12835  2prm  12907  dfphi2  13000  pockthi  13139  karatsuba  13211  ballotfilem2  13230  ballotfilem4  13243  ballotfilem5  13244  ballotfilemi1  13247  ballotfilem7  13281  ballotfilemth  13283  znnen  13291  ennnfonelem1  13300  qnnen  13324  ctiunct  13333  ssnnctlemct  13339  structcnvcnv  13370  structfn  13373  relelbasov  13418  xpsff1o  13672  rmodislmod  14690  cnfld0  14910  cnfld1  14911  eltpsi  15144  unitg  15165  epttop  15193  txuni2  15359  retopon  15629  cnfldtopon  15643  dedekindicclemicc  15735  reldvg  15782  dvrecap  15816  dvef  15830  plyrecj  15866  sinhalfpilem  15895  coseq00topi  15939  coseq0negpitopi  15940  sincos4thpi  15944  sincos6thpi  15946  pigt3  15948  cos02pilt1  15955  logltb  15979  rpabscxpbnd  16048  log2ublog2  16092  birthdaylog2  16096  sgmf  16106  1sgm2ppw  16115  lgsdir2lem2  16160  lgsdir2lem3  16161  konigsbergiedgwen  16737  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem4  16744  konigsberglem5  16745  konigsberg  16746  ex-fl  16751  ex-exp  16753  bdceqi  16881  bdcriota  16921  bdsepnfALT  16927  bdbm1.3ii  16929  bj-d0clsepcl  16963  nninfsellemeqinf  17071