Theorem mpbi 233

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-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 219	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  pm5.74i  274  notbii  323  biluk  390  pm5.19  391  pm3.24  406  dfbi  479  pm4.71i  563  pm5.32i  578  biadani  820  biadanii  822  imori  854  ori  861  pm5.16  1014  dn1  1058  3ori  1426  cadan  1616  nic-dfim  1677  nic-dfneg  1678  nic-mp  1679  nic-mpALT  1680  tbw-negdf  1707  rb-imdf  1758  nfri  1797  mpgbi  1806  19.35i  1886  nfim1  2199  19.36i  2231  ax6  2385  sbie  2507  datisi  2682  disamis  2683  dimatis  2690  fresison  2691  bamalip  2694  axi12  2708  eqcomi  2748  eqtri  2767  eleqtri  2838  nfnfc  2919  neii  2945  necomi  2998  neeqtri  3016  neli  3051  nfra2wOLD  3153  nrex  3197  rexlimiv  3209  rexlimi  3244  eueqi  3640  euxfr2w  3651  euxfr2  3653  reuxfrd  3679  cdeqri  3697  sseqtri  3954  3sstr3i  3960  pssn2lp  4033  equncomi  4086  unssi  4116  ssini  4163  unabs  4186  inabs  4187  dfin4  4199  vn0  4270  difidALT  4303  ab0orv  4310  ab0orvALT  4311  disjdif  4403  difin0  4405  pwundif  4556  snid  4594  rabrsn  4657  iinrab2  4995  symdifv  5011  rintn0  5034  breqtri  5095  axsepgfromrep  5214  bm1.3ii  5219  ax6vsep  5220  notzfaus  5278  notzfausOLD  5279  zfpow  5283  dtru  5287  dtruALT  5305  reusv2lem4  5318  dtruALT2  5352  op1stb  5379  copsexgw  5397  copsexg  5398  uniop  5422  pwundifOLD  5476  rn0  5823  dmresi  5949  somincom  6027  cnvimassrndm  6043  cnvcnv  6083  elid  6090  rescnvcnv  6095  cnvcnvres  6096  cocnvcnv2  6150  cores2  6151  co01  6153  cnviin  6177  onunisuci  6362  iota4an  6397  fnopab  6552  mpt0  6556  fnmpti  6557  f1cnvcnv  6661  f1ovi  6735  eliman0  6788  fvco4i  6848  cnvimainrn  6923  fmpti  6965  funiunfv  7100  oprabss  7356  relmptopab  7494  zfun  7564  tfinds2  7682  omon  7696  2nd0  7808  f1stres  7825  f2ndres  7826  cnvoprab  7870  relmpoopab  7902  df1st2  7906  df2nd2  7907  fsplit  7925  fsplitOLD  7926  reldmtpos  8018  dftpos4  8029  tpostpos  8030  tpos0  8040  frrlem4  8072  wfrlem4  8100  smo0  8137  tfrlem14  8169  tfrlem16  8171  rdgsucg  8201  rdglimg  8203  frfnom  8212  oawordeulem  8324  uniixp  8644  dfdom2  8698  ssdomg  8718  xpcomf1o  8778  sbthlem5  8804  limensuci  8866  fiint  8996  fidomdm  9001  residfi  9005  pwfilemOLD  9018  mptfi  9023  fisn  9091  dffi3  9095  ordtypelem6  9187  ordtypelem7  9188  wemaplem2  9211  harwdom  9255  suc11reg  9282  zfinf  9302  axinf2  9303  noinfep  9323  cantnfvalf  9328  cantnflt  9335  cantnf0  9338  cantnf  9356  tz9.1c  9394  tc2  9406  r111  9439  r1tr2  9441  r1ordg  9442  r1sssuc  9447  r1val1  9450  tz9.13  9455  r1elssi  9469  pwwf  9471  rankopb  9516  rankeq0b  9524  ranksuc  9529  rankmapu  9542  rankxplim3  9545  rankxpsuc  9546  cp  9555  karden  9559  card0  9622  cardlim  9636  cardom  9650  infxpenlem  9675  alephsuc2  9742  alephgeom  9744  unialeph  9763  dfac4  9784  dfacacn  9803  dju1dif  9834  dju1p1e2  9835  infdju1  9851  ackbij1lem13  9894  ackbij2  9905  cf0  9913  cfsuc  9919  cfom  9926  cfslb2n  9930  ominf4  9974  fin23lem17  10000  fin23lem28  10002  fin23lem30  10004  fin23lem31  10005  fin23lem40  10013  isfin1-3  10048  dfacfin7  10061  fin1a2lem6  10067  itunitc1  10082  axcc3  10100  dcomex  10109  axdc2lem  10110  axcclem  10119  zfac  10122  ac3  10124  ackm  10127  axac2  10128  axac  10129  axaci  10130  cardeqv  10131  numth2  10133  numth  10134  dmct  10186  brdom3  10190  fin71ac  10195  cardf  10212  aleph1  10233  cfpwsdom  10246  smobeth  10248  zfcndrep  10276  zfcndpow  10278  zfcndac  10281  gch2  10337  wunex3  10403  tskpr  10432  inar1  10437  rankcf  10439  tskcard  10443  tskuni  10445  grothpw  10488  axgroth4  10494  grothprim  10496  inaprc  10498  dmaddpi  10552  dmmulpi  10553  1lt2pi  10567  addpqf  10606  mulpqf  10608  1lt2nq  10635  supsrlem  10773  ssxr  10950  gtso  10962  subf  11128  negne0i  11201  mulnzcnopr  11526  infrenegsup  11863  nnne0  11912  halflt1  12096  nn0ssz  12246  3halfnz  12304  zeo  12311  numlt  12366  numltc  12367  le9lt10  12368  decle  12375  uzf  12489  xaddf  12862  xsubge0  12899  xmulf  12910  ixxf  12993  ixxssxr  12995  iooval2  13016  ioof  13083  unirnioo  13085  dfioo2  13086  fzval2  13146  fzf  13147  0nelfz1  13179  fz10  13181  fzpreddisj  13209  4fvwrd4  13280  fzof  13288  fzo0  13314  fldiv4p1lem1div2  13458  fldiv4lem1div2  13460  om2uzoi  13578  faclbnd4lem1  13910  hashkf  13949  hashgval  13950  hashinf  13952  hashresfn  13957  hashnn0n0nn  14009  hashge3el3dif  14103  rev0  14380  s2dm  14506  f1oun2prg  14533  trclublem  14609  sqrt2gt1lt2  14889  limsupgord  15084  fclim  15165  fsumrelem  15422  ackbijnn  15443  incexclem  15451  incexc  15452  arisum2  15476  georeclim  15487  geoisumr  15493  0.999...  15496  risefall0lem  15639  ege2le3  15702  sin0  15761  ef01bndlem  15796  cos2bnd  15800  cos01gt0  15803  sincos2sgn  15806  sin4lt0  15807  rpnnen2lem3  15828  rpnnen2lem9  15834  rexpen  15840  cnso  15859  dvdslelem  15921  divalglem1  16006  divalglem5  16009  divalglem6  16010  divalglem10  16014  flodddiv4  16025  0bits  16049  sadcf  16063  sadcadd  16068  bitsshft  16085  smupf  16088  gcdf  16122  eucalgf  16191  2prm  16300  dfphi2  16378  pockthi  16511  prmrec  16526  vdwapf  16576  vdwlem6  16590  karatsuba  16688  1259lem5  16739  2503lem3  16743  4001lem4  16748  structcnvcnv  16757  structfn  16760  strleun  16761  imasvscafn  17140  xpsff1o  17170  wunnat  17563  wunnatOLD  17564  dfinito3  17611  dftermo3  17612  eldmcoa  17671  coapm  17677  catcfuccl  17725  catcfucclOLD  17726  catcxpccl  17815  catcxpcclOLD  17816  yonedainv  17890  smndex1bas  18435  smndex1n0mnd  18441  grpinvfvi  18512  mulgfvi  18596  symgsssg  18965  symgfisg  18966  psgnunilem5  18992  sylow3lem2  19123  oppglsm  19137  efgmf  19209  efgval  19213  efgsf  19225  0frgp  19275  dmdprd  19491  dprdval  19496  invrfval  19805  drngui  19887  rmodislmod  20081  rmodislmodOLD  20082  lssintcl  20116  cnfldfun  20497  cnfld0  20509  cnfld1  20510  cnfldsub  20513  xrsds  20528  psgnghm  20672  zrhpsgnmhm  20676  recrng  20713  ocv1  20771  dsmmbas2  20829  mplsubrglem  21095  opsrtoslem2  21148  mdetralt  21640  maducoeval2  21672  eltpsi  21977  unitg  22000  fctop  22037  cctop  22039  ppttop  22040  epttop  22042  leordtvallem1  22244  leordtvallem2  22245  iccordt  22248  iscnp2  22273  discmp  22432  conncompcld  22468  1stcrestlem  22486  2ndcdisj  22490  topnlly  22525  disllycmp  22532  dis1stc  22533  txuni2  22599  xkotf  22619  dfac14lem  22651  prdstps  22663  txindis  22668  tx1stc  22684  xkohaus  22687  xkoptsub  22688  cnmpt1st  22702  cnmpt2nd  22703  ptcmpfi  22847  trfil1  22920  fin1aufil  22966  tgpconncompeqg  23146  tgpconncomp  23147  trust  23264  met1stc  23558  dscmet  23609  retopon  23808  cnfldtopon  23827  xrsxmet  23853  xrsmopn  23856  iimulcn  23982  icopnfhmeo  23987  iccpnfhmeo  23989  xrhmeo  23990  cnheiborlem  23998  lebnumii  24010  ishtpy  24016  htpycc  24024  pco1  24059  pcohtpylem  24063  pcopt  24066  pcopt2  24067  pcoass  24068  pcorevlem  24070  rrxcph  24436  rrx0el  24442  ovoliunlem3  24548  ovolicc1  24560  ovolicc2  24566  volf  24573  ioorf  24617  dyadf  24635  dyadmbl  24644  vitalilem5  24656  vitali  24657  mbfimaopnlem  24699  mbflimsup  24710  0plef  24716  i1fima  24722  i1fima2  24723  i1fd  24725  itg1ge0  24730  itg10  24732  i1f1lem  24733  i1fadd  24739  i1fmul  24740  i1fmulc  24748  mbfi1fseqlem5  24764  itg2addlem  24803  reldv  24914  dvbsss  24946  dvef  25024  lhop1lem  25057  deg1fvi  25130  plypf1  25253  coeeulem  25265  coeeu  25266  vieta1lem2  25351  aannenlem3  25370  aalioulem3  25374  dvradcnv  25460  pserulm  25461  pserdvlem2  25467  sinhalfpilem  25500  sincos4thpi  25550  tan4thpi  25551  sincos6thpi  25552  pige3ALT  25556  resinf1o  25572  tanord1  25573  tanregt0  25575  efabl  25586  relogrn  25597  dfrelog  25601  logneg  25623  logltb  25635  logcn  25682  logf1o2  25685  dvlog  25686  efopnlem2  25692  efopn  25693  logccv  25698  dvsqrt  25775  dvcnsqrt  25777  cxpcn3  25781  logblog  25822  angpined  25860  1cubr  25872  asinsin  25922  asin1  25924  reasinsin  25926  atan0  25938  atanbnd  25956  atan1  25958  log2cnv  25974  log2ub  25979  log2le1  25980  birthday  25984  amgmlem  26019  emcllem5  26029  emgt0  26036  harmonicbnd3  26037  ftalem3  26104  basellem4  26113  sgmf  26174  ppi1  26193  cht1  26194  vma1  26195  ppiltx  26206  sqff1o  26211  ppiublem1  26230  ppiublem2  26231  ppiub  26232  chtub  26240  dchreq  26286  bposlem7  26318  bposlem8  26319  bposlem9  26320  lgsdir2lem2  26354  lgsdir2lem3  26355  chebbnd1  26500  chto1ub  26504  chpo1ubb  26509  pntibndlem1  26617  tgldimor  26742  tglnfn  26787  axlowdimlem4  27191  axlowdimlem16  27203  axlowdim  27207  upgrfi  27339  lfgrnloop  27373  lfuhgr1v0e  27499  usgrexmplef  27504  usgrres  27553  vdegp1bi  27782  vtxdginducedm1lem2  27785  pthdlem2  28012  wpthswwlks2on  28202  0ewlk  28354  0pth  28365  konigsbergiedgw  28488  konigsberglem1  28492  konigsberglem2  28493  konigsberglem3  28494  konigsberglem4  28495  konigsberglem5  28496  ex-dif  28663  ex-un  28664  ex-in  28665  ex-fl  28687  avril1  28703  9p10ne21fool  28711  n0lplig  28721  cnidOLD  28820  cnnvm  28920  ipasslem8  29075  ipasslem10  29077  hvsubf  29253  normlem1  29348  normlem6  29353  normlem7  29354  norm-ii-i  29375  norm3adifii  29386  hilid  29399  hlimf  29475  hhssabloi  29500  hhssnv  29502  hhshsslem1  29505  shincli  29600  shsval2i  29625  shs0i  29687  chj0i  29693  chm1i  29694  chincli  29698  chdmm1i  29715  shjshsi  29730  chsup0  29786  h1de2bi  29792  spansnpji  29816  cmcmlem  29829  cmcmii  29835  cmcm2ii  29836  cmcm3ii  29837  pjidmi  29911  pjssmii  29919  pj0i  29931  pjocini  29936  mayetes3i  29967  df0op2  29990  hoaddcomi  30010  hoaddassi  30014  hocadddiri  30017  hocsubdiri  30018  hoaddid1i  30024  ho0coi  30026  hoid1i  30027  hoid1ri  30028  hodseqi  30032  honegsubi  30034  adj1o  30132  hoddii  30227  lnopunilem1  30248  lnopunilem2  30249  nmcopexi  30265  nmcopex  30267  nmcoplb  30268  nmcfnexi  30289  nmcfnex  30291  nmcfnlb  30292  adjbd1o  30323  adjcoi  30338  nmopcoadji  30339  opsqrlem6  30383  pjsdii  30393  pjddii  30394  pjidmcoi  30415  pjtoi  30417  pjin1i  30430  pjclem1  30433  stji1i  30480  reuxfrdf  30715  inindif  30739  iuninc  30776  fnresin  30837  rinvf1o  30841  suppss2f  30850  xppreima  30859  ofoprabco  30878  fressupp  30899  supppreima  30902  fsupprnfi  30903  gtiso  30910  df1stres  30913  df2ndres  30914  snct  30925  padct  30931  fsuppcurry1  30937  fsuppcurry2  30938  ffsrn  30941  fpwrelmapffs  30946  fzodif1  30991  nnindf  31010  nn0min  31011  dp2lt  31036  dp2ltsuc  31037  dp2ltc  31038  dplti  31056  dpmul  31064  dpmul4  31065  ressplusf  31112  xrsclat  31166  xrge0base  31171  xrge00  31172  xrnarchi  31315  xrge0slmod  31425  ccfldsrarelvec  31618  ccfldextdgrr  31619  locfinreflem  31667  locfinref  31668  unicls  31730  sqsscirc1  31735  mhmhmeotmd  31754  rmulccn  31755  raddcn  31756  xrge0iifiso  31762  xrge0iifhmeo  31763  lmxrge0  31779  cnzh  31795  rezh  31796  qqh0  31809  qqh1  31810  qqhre  31845  rrhre  31846  esumnul  31891  esum0  31892  esumsnf  31907  esumpfinvallem  31917  esumpfinvalf  31919  esumpcvgval  31921  esumcvgsum  31931  esumsup  31932  esumcvgre  31934  sigaclfu2  31964  dmsigagen  31987  ddemeas  32079  mbfmvolf  32108  br2base  32111  omssubadd  32142  sibfof  32182  sitg0  32188  eulerpartlemt  32213  eulerpartgbij  32214  0rrv  32293  coinfliplem  32320  coinflipprob  32321  coinfliprv  32324  ballotlem2  32330  ballotlem4  32340  ballotlem5  32341  ballotlemi1  32344  ballotlem7  32377  ballotth  32379  signsplypnf  32404  signsply0  32405  signsw0g  32410  signswch  32415  signsvf0  32434  hashreprin  32475  reprfz1  32479  chtvalz  32484  hgt750lemd  32503  hgt750lem  32506  hgt750lem2  32507  bnj521  32591  bnj1098  32638  bnj1109  32641  bnj1131  32642  bnj1533  32707  bnj151  32732  bnj580  32768  bnj852  32776  bnj864  32777  bnj865  32778  bnj978  32804  bnj1021  32821  bnj907  32822  bnj1093  32835  bnj1145  32848  bnj1172  32856  bnj1174  32858  bnj1176  32860  bnj1186  32862  fineqvac  32941  subfacf  33012  subfacp1lem1  33016  subfacp1lem5  33021  subfacp1lem6  33022  subfacval3  33026  erdszelem2  33029  kur14lem4  33046  ioosconn  33084  iccllysconn  33087  satfn  33192  fmlaomn0  33227  gonan0  33229  goaln0  33230  elnanelprv  33266  msrfo  33383  mthmpps  33419  problem5  33502  quad3  33503  circum  33507  axextprim  33517  axrepprim  33518  axunprim  33519  axinfprim  33522  axacprim  33523  logi  33581  bcneg1  33583  setinds  33635  dfon2lem2  33641  dfon2lem4  33643  axextdfeq  33654  ttrclco  33679  frpoins3xpg  33689  frpoins3xp3g  33690  poxp2  33692  poseq  33704  nosgnn0  33763  sltsolem1  33780  bdayfo  33782  nolt02o  33800  nogt01o  33801  noetasuplem4  33841  noetainflem4  33845  scutbdaybnd2lim  33913  madeun  33968  fobigcup  34104  snelsingles  34126  fullfunfnv  34150  fullfunfv  34151  rankaltopb  34183  rank0  34374  rankeq1o  34375  hfuni  34388  fneer  34444  neibastop1  34450  nabi1i  34485  nabi2i  34486  limsucncmpi  34536  knoppcnlem8  34582  knoppcnlem11  34585  cnndvlem1  34619  bj-consensusALT  34662  bj-dtru  34901  bj-sbidmOLD  34936  bj-n0i  35042  bj-snsetex  35055  bj-tagss  35072  bj-2upln0  35115  bj-2upln1upl  35116  bj-nuliota  35130  bj-0int  35175  bj-elid5  35243  bj-inftyexpitaufo  35276  bj-pinftyccb  35295  bj-minftyccb  35299  bj-pinftynminfty  35301  bj-isrvec  35368  iccioo01  35401  f1omptsnlem  35413  mptsnunlem  35415  topdifinffinlem  35424  relowlpssretop  35441  1oequni2o  35445  pibt2  35494  imadifss  35658  tan2h  35675  poimirlem3  35686  poimirlem9  35692  poimirlem16  35699  poimirlem17  35700  poimirlem18  35701  poimirlem19  35702  poimirlem20  35703  poimirlem22  35705  poimirlem30  35713  mblfinlem1  35720  mblfinlem2  35721  ovoliunnfl  35725  voliunnfl  35727  itg2addnclem  35734  itg2addnclem2  35735  asindmre  35766  areacirclem1  35771  fdc  35809  cntotbnd  35860  heiborlem6  35880  rrnval  35891  reheibor  35903  rngosn3  35988  brcnvrabga  36383  cnvresrn  36389  moantr  36400  inxp2  36403  dfxrn2  36412  cnvcosseq  36466  refrelcosslem  36486  1cosscnvxrn  36499  redundss3  36647  refrelsredund3  36653  refrelredund3  36656  prter2  36801  renegclALT  36883  mapdunirnN  39570  lcmeprodgcdi  39922  3factsumint2  39937  3factsumint3  39938  3factsumint4  39939  3factsumint  39940  lcmineqlem4  39947  3lexlogpow5ineq1  39969  3lexlogpow2ineq1  39973  dvrelogpow2b  39982  aks4d1p1p4  39985  2ap1caineq  40001  sticksstones1  40002  sticksstones2  40003  metakunt6  40030  metakunt24  40048  sn-dtru  40088  sqdeccom12  40210  resubf  40257  sn-0ne2  40282  sn-subf  40303  sn-0lt1  40325  reneg1lt0  40327  rntrclfvOAI  40401  diophrw  40469  rabren3dioph  40525  pellexlem6  40544  pellex  40545  frmx  40623  frmy  40624  jm2.23  40706  jm2.27dlem3  40721  axac10  40743  pw2f1ocnv  40747  kelac2lem  40777  lmhmlnmsplit  40800  pwfi2f1o  40809  frlmpwfi  40811  ifpbiidcor  40951  alephiso2  41026  alephiso3  41027  cnvnonrel  41057  rnnonrel  41060  resnonrel  41061  cononrel1  41063  cononrel2  41064  fvnonrel  41066  cnvcnvintabd  41069  cnvintabd  41072  rclexi  41084  rtrclex  41086  clcnvlem  41092  cnvrcl0  41094  dmtrcl  41096  rntrcl  41097  dfrtrcl5  41098  iunrelexp0  41172  dmtrclfvRP  41200  rntrclfv  41202  corcltrcl  41209  cotrclrcl  41212  0heALT  41253  frege54cor1a  41334  uneqsn  41495  clsk3nimkb  41512  int-sqdefd  41654  int-sqgeq0d  41659  rr-groth  41779  rr-grothprim  41780  rr-grothshort  41784  seff  41789  expgrowthi  41813  expgrowth  41815  binomcxplemnotnn0  41836  ee233  42001  ax6e2nd  42040  in1  42053  dfvd2ani  42065  dfvd2i  42067  dfvd3i  42074  dfvd3ani  42077  e0bi  42258  uun2221  42295  uun2221p1  42296  uun2221p2  42297  en3lpVD  42327  relopabVD  42383  ax6e2ndVD  42390  ax6e2ndALT  42412  pssnssi  42513  nnf1oxpnn  42596  icof  42621  negpilt0  42681  xrgtso  42747  supxrleubrnmptf  42854  xrpnf  42889  ioontr  42912  iccdifioo  42916  iccdifprioo  42917  uzinico2  42963  fsummulc1f  42975  fsumiunss  42979  fnlimfvre2  43081  limsupreuz  43141  limsupvaluz2  43142  limsup10ex  43177  icccncfext  43291  dvcosre  43316  dvsinax  43317  ioodvbdlimc1lem2  43336  ioodvbdlimc2lem  43338  dvmptmulf  43341  dvnmul  43347  dvmptfprodlem  43348  dvnprodlem2  43351  stoweidlem1  43405  stoweidlem26  43430  stoweidlem34  43438  stoweidlem44  43448  stoweid  43467  stirlinglem5  43482  dirkercncflem1  43507  fourierdlem44  43555  fourierdlem56  43566  fourierdlem62  43572  fourierdlem89  43599  fourierdlem91  43601  fourierdlem100  43610  fourierdlem102  43612  fourierdlem103  43613  fourierdlem104  43614  fourierdlem108  43618  fourierdlem112  43622  fourierdlem114  43624  fouriersw  43635  rrndistlt  43694  gsumge0cl  43772  sge0tsms  43781  sge0ltfirpmpt2  43827  ovn0  43967  hoidmv1le  43995  hoidmvle  44001  ovnsubadd2lem  44046  ovolval4lem1  44050  vonioolem2  44082  smflimlem3  44168  nsssmfmbf  44174  axorbtnotaiffb  44258  axorbciffatcxorb  44260  abnotbtaxb  44270  euabsneu  44382  sprval  44792  fmtnoinf  44849  1nevenALTV  45004  nfermltl8rev  45055  nfermltl2rev  45056  nnsum3primes4  45101  tgblthelfgott  45128  tgoldbachlt  45129  ldepslinc  45711  ackval42  45903  rrx2plordso  45931  vsn  46018  sepfsepc  46082  alimp-no-surprise  46344  aacllem  46364  amgmwlem  46365  amgmlemALT  46366