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  4156  bm1.3ii  4256  zfnuleu  4259  zfpow  4314  undifexmid  4332  copsexg  4386  uniop  4398  pwundifss  4432  onunisuci  4579  zfun  4581  op1stb  4626  op1stbg  4627  ordtriexmidlem  4668  ordtriexmid  4670  ordtri2orexmid  4672  2ordpr  4673  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  dtruex  4708  ordsoexmid  4711  0elsucexmid  4714  ordtri2or2exmid  4720  dcextest  4730  tfi  4731  relop  4932  dmxpid  5005  rn0  5040  dmresi  5121  issref  5173  cnvcnv  5243  rescnvcnv  5253  cnvcnvres  5254  cnvsn  5273  cocnvcnv2  5302  cores2  5303  co01  5305  relcoi1  5322  cnviinm  5332  fnopab  5511  mpt0  5514  fnmpti  5515  f1cnvcnv  5612  f1ovi  5683  fmpti  5863  fvsnun2  5916  rinvf1o  6038  oprabss  6177  relmptopab  6294  2nd0  6383  f1stres  6397  f2ndres  6398  reldmtpos  6528  dftpos4  6538  tpostpos  6539  tpos0  6549  smo0  6573  frecfnom  6676  oasuc  6741  uniixp  7008  ssdomg  7070  xpcomf1o  7128  ssfilem  7182  diffitest  7196  inffiexmid  7218  fiintim  7243  caseinl  7438  caseinr  7439  eninl  7444  eninr  7445  card0  7540  dju1p1e2  7556  pw1on  7592  dmaddpi  7699  dmmulpi  7700  1lt2pi  7714  1lt2nq  7780  suplocsrlempr  8181  gtso  8411  subf  8536  negne0i  8609  negdii  8618  ltapii  8972  sup3exmid  9296  neg1ap0  9423  halflt1  9534  nn0ssz  9674  3halfnz  9755  zeo  9763  numlt  9818  numltc  9819  le9lt10  9820  decle  9827  uzf  9941  indstr  10010  infrenegsupex  10011  xaddf  10264  ixxf  10318  iooval2  10335  ioof  10391  unirnioo  10393  fzval2  10432  fzf  10433  fz10  10468  fz00m1  10469  fzpreddisj  10496  4fvwrd4  10565  fzof  10569  fldiv4p1lem1div2  10762  fldiv4lem1div2  10764  xnn0nnen  10896  hashfibc  11306  sqrt2gt1lt2  11838  infxrnegsupex  12055  fclim  12086  fsumrelem  12264  arisum2  12292  geo2sum2  12308  0.999...  12314  ege2le3  12464  sin0  12522  ef01bndlem  12549  cos2bnd  12553  cos01gt0  12556  sincos2sgn  12559  sin4lt0  12560  egt2lt3  12573  n2dvds1  12705  flodddiv4  12729  0bits  12752  gcdf  12775  nninfct  12844  eucalgf  12859  2prm  12931  dfphi2  13028  pockthi  13167  karatsuba  13240  1259lem5  13276  ballotfilem2  13287  ballotfilem4  13300  ballotfilem5  13301  ballotfilemi1  13304  ballotfilem7  13338  ballotfilemth  13340  znnen  13348  ennnfonelem1  13357  qnnen  13381  ctiunct  13390  ssnnctlemct  13396  structcnvcnv  13427  structfn  13430  relelbasov  13475  xpsff1o  13730  rmodislmod  14798  cnfld0  15018  cnfld1  15019  eltpsi  15279  unitg  15300  epttop  15328  txuni2  15494  retopon  15764  cnfldtopon  15778  dedekindicclemicc  15870  reldvg  15917  dvrecap  15951  dvef  15965  plyrecj  16001  sinhalfpilem  16030  coseq00topi  16074  coseq0negpitopi  16075  sincos4thpi  16079  sincos6thpi  16081  pigt3  16083  cos02pilt1  16091  logltb  16116  rpabscxpbnd  16187  log2ublog2  16236  birthdaylog2  16240  sgmf  16267  ppi1  16282  cht1  16283  1sgm2ppw  16301  ppiublem1  16303  ppiublem2  16304  ppiqub  16305  chtqub  16308  bposlem7  16329  bposlem8  16330  bposlem9  16331  lgsdir2lem2  16365  lgsdir2lem3  16366  konigsbergiedgwen  16942  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem4  16949  konigsberglem5  16950  konigsberg  16951  ex-fl  16956  ex-exp  16958  bdceqi  17086  bdcriota  17126  bdsepnfALT  17132  bdbm1.3ii  17134  bj-d0clsepcl  17168  nninfsellemeqinf  17277