Theorem mpbi 222

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 208	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  pm5.74i  263  notbii  312  biluk  378  pm5.19  379  pm3.24  394  pm4.71i  552  pm4.71ri  553  pm5.32i  567  biadanOLD  807  biadani  808  biadanii  810  imori  840  ori  847  pm5.16  996  dn1  1038  3ori  1404  cadan  1572  nic-dfim  1632  nic-dfneg  1633  nic-mp  1634  nic-mpALT  1635  tbw-negdf  1662  rb-imdf  1713  nfri  1752  mpgbi  1761  19.35i  1841  nfim1  2128  19.36i  2163  sbievOLD  2254  ax6  2314  sbie  2468  sbieALT  2540  datisi  2714  disamis  2715  dimatis  2722  fresison  2723  bamalip  2726  axi12  2740  axi12OLD  2741  nulmoOLD  2751  eqcomi  2781  eqtri  2796  eleqtri  2858  neii  2963  necomi  3015  neeqtri  3033  neli  3069  nrex  3208  rexlimiv  3219  rexlimi  3252  issetiOLD  3424  vtocl2OLD  3475  eueqi  3608  euxfr2  3619  reuxfr3d  3645  cdeqri  3660  sseqtri  3887  3sstr3i  3893  pssn2lp  3962  equncomi  4014  unssi  4043  ssini  4089  unabs  4112  inabs  4113  dfin4  4125  difid  4210  ab0orv  4215  disjdif  4298  difin0  4299  snid  4467  rabrsn  4528  iinrab2  4852  symdifv  4868  rintn0  4890  breqtri  4948  axsep  5053  bm1.3ii  5057  ax6vsep  5058  notzfaus  5110  zfpow  5114  dtru  5118  dtruALT  5135  reusv2lem4  5149  dtruALT2  5186  op1stb  5214  copsexg  5232  uniop  5255  pwundif  5303  rn0  5670  dmresi  5757  somincom  5828  cnvcnv  5883  elid  5889  rescnvcnv  5894  cnvcnvres  5895  cocnvcnv2  5944  cores2  5945  co01  5947  cnviin  5969  onunisuci  6136  iota4an  6165  fnopab  6310  mpt0  6314  fnmpti  6315  f1cnvcnv  6407  f1ovi  6476  eliman0  6529  fvco4i  6583  fmpti  6693  fvsnun2OLD  6766  funiunfv  6826  oprabss  7070  relmptopab  7207  zfun  7274  tfinds2  7388  omon  7401  2nd0  7502  f1stres  7519  f2ndres  7520  cnvoprab  7560  relmpoopab  7591  df1st2  7595  df2nd2  7596  fsplit  7614  reldmtpos  7697  dftpos4  7708  tpostpos  7709  tpos0  7719  wfrlem4  7755  wfrlem4OLD  7756  smo0  7793  tfrlem14  7825  tfrlem16  7827  rdgsucg  7857  rdglimg  7859  frfnom  7868  oawordeulem  7975  uniixp  8276  dfdom2  8326  ssdomg  8346  xpcomf1o  8396  sbthlem5  8421  pwdom  8459  limensuci  8483  fiint  8584  fidomdm  8590  residfi  8594  pwfilem  8607  mptfi  8612  fisn  8680  dffi3  8684  ordtypelem6  8776  ordtypelem7  8777  wemaplem2  8800  wdompwdom  8831  harwdom  8843  suc11reg  8870  zfinf  8890  axinf2  8891  noinfep  8911  cantnfvalf  8916  cantnflt  8923  cantnf0  8926  cantnf  8944  tz9.1c  8960  tc2  8972  r111  8992  r1tr2  8994  r1ordg  8995  r1sssuc  9000  r1val1  9003  tz9.13  9008  r1elssi  9022  pwwf  9024  rankopb  9069  rankeq0b  9077  ranksuc  9082  rankmapu  9095  rankxplim  9096  rankxplim3  9098  rankxpsuc  9099  cp  9108  karden  9112  card0  9175  cardlim  9189  cardom  9203  infxpenlem  9227  alephsuc2  9294  alephgeom  9296  unialeph  9315  dfac4  9336  dfacacn  9355  dju1dif  9390  dju1p1e2  9391  infdju1  9407  ackbij1lem13  9446  ackbij2  9457  cf0  9465  cfsuc  9471  cfom  9478  cfslb2n  9482  ominf4  9526  fin23lem17  9552  fin23lem28  9554  fin23lem30  9556  fin23lem31  9557  fin23lem40  9565  isfin1-3  9600  dfacfin7  9613  fin1a2lem6  9619  itunitc1  9634  axcc3  9652  dcomex  9661  axdc2lem  9662  axcclem  9671  zfac  9674  ac3  9676  ackm  9679  axac2  9680  axac  9681  axaci  9682  cardeqv  9683  numth2  9685  numth  9686  dmct  9738  brdom3  9742  fin71ac  9747  cardf  9764  aleph1  9785  cfpwsdom  9798  smobeth  9800  zfcndrep  9828  zfcndpow  9830  zfcndac  9833  gch2  9889  wunex3  9955  tskpr  9984  inar1  9989  rankcf  9991  tskcard  9995  tskuni  9997  grothpw  10040  axgroth4  10046  grothprim  10048  inaprc  10050  dmaddpi  10104  dmmulpi  10105  1lt2pi  10119  addpqf  10158  mulpqf  10160  1lt2nq  10187  supsrlem  10325  ssxr  10504  gtso  10516  subf  10682  negne0i  10756  mulnzcnopr  11081  infrenegsup  11419  nnne0  11468  halflt1  11659  nn0ssz  11810  3halfnz  11868  zeo  11875  numlt  11931  numltc  11932  le9lt10  11933  decle  11940  uzf  12055  xaddf  12428  xsubge0  12464  xmulf  12475  ixxf  12558  ixxssxr  12560  iooval2  12581  ioof  12645  unirnioo  12647  dfioo2  12648  fzval2  12705  fzf  12706  0nelfz1  12736  fz10  12738  fzpreddisj  12766  4fvwrd4  12837  fzof  12845  fzo0  12870  fldiv4p1lem1div2  13014  fldiv4lem1div2  13016  om2uzoi  13132  faclbnd4lem1  13462  hashkf  13501  hashgval  13502  hashinf  13504  hashresfn  13509  hashnn0n0nn  13559  hashbclem  13617  hashge3el3dif  13649  wrdexgOLD  13677  rev0  13977  s2dm  14108  f1oun2prg  14135  trclublem  14210  sqrt2gt1lt2  14489  limsupgord  14684  fclim  14765  fsumrelem  15016  ackbijnn  15037  incexclem  15045  incexc  15046  arisum2  15070  georeclim  15082  geoisumr  15088  0.999...  15091  risefall0lem  15234  ege2le3  15297  sin0  15356  ef01bndlem  15391  cos2bnd  15395  cos01gt0  15398  sincos2sgn  15401  sin4lt0  15402  rpnnen2lem3  15423  rpnnen2lem9  15429  rexpen  15435  cnso  15454  dvdslelem  15513  n2dvds1OLD  15572  divalglem1  15599  divalglem5  15602  divalglem6  15603  divalglem10  15607  flodddiv4  15618  0bits  15642  sadcf  15656  sadcadd  15661  bitsshft  15678  smupf  15681  gcdf  15715  eucalgf  15777  2prm  15886  dfphi2  15961  pockthi  16093  prmrec  16108  vdwapf  16158  vdwlem6  16172  karatsuba  16270  1259lem5  16318  2503lem3  16322  4001lem4  16327  structcnvcnv  16347  structfn  16350  strleun  16441  prdsval  16578  prdsds  16587  imasvscafn  16660  xpsc0  16683  xpsc1  16684  xpsff1o  16691  sscpwex  16937  wunfunc  17021  wunnat  17078  eldmcoa  17177  coapm  17183  catcfuccl  17221  catcxpccl  17309  yonedainv  17383  plusffval  17709  grpinvfvi  17927  mulgfvi  18011  symgsssg  18350  symgfisg  18351  psgnunilem5  18377  psgnunilem5OLD  18378  sylow3lem2  18508  oppglsm  18522  efgmf  18591  efgval  18595  efgsf  18607  0frgp  18659  dmdprd  18864  dprdval  18869  invrfval  19140  drngui  19225  scaffval  19368  rmodislmod  19418  lssintcl  19452  mplsubrglem  19927  opsrtoslem2  19972  cnfldfun  20253  cnfld0  20265  cnfld1  20266  cnfldsub  20269  xrsds  20284  psgnghm  20420  zrhpsgnmhm  20424  recrng  20461  ipffval  20488  ocv1  20519  dsmmbas2  20577  mdetralt  20915  maducoeval2  20947  eltpsi  21250  unitg  21273  fctop  21310  cctop  21312  ppttop  21313  epttop  21315  leordtvallem1  21516  leordtvallem2  21517  iccordt  21520  iscnp2  21545  discmp  21704  conncompcld  21740  1stcrestlem  21758  2ndcdisj  21762  topnlly  21797  disllycmp  21804  dis1stc  21805  txuni2  21871  xkotf  21891  dfac14lem  21923  prdstps  21935  txindis  21940  tx1stc  21956  xkohaus  21959  xkoptsub  21960  cnmpt1st  21974  cnmpt2nd  21975  ptcmpfi  22119  trfil1  22192  fin1aufil  22238  tgpconncompeqg  22417  tgpconncomp  22418  tsmsres  22449  trust  22535  met1stc  22828  dscmet  22879  retopon  23069  cnfldtopon  23088  xrsxmet  23114  xrsmopn  23117  iimulcn  23239  icopnfhmeo  23244  iccpnfhmeo  23246  xrhmeo  23247  cnheiborlem  23255  lebnumii  23267  ishtpy  23273  htpycc  23281  pco1  23316  pcohtpylem  23320  pcopt  23323  pcopt2  23324  pcoass  23325  pcorevlem  23327  cfilresi  23595  rrxcph  23692  rrx0el  23698  ovoliunlem3  23802  ovolicc1  23814  ovolicc2  23820  volf  23827  ioorf  23871  dyadf  23889  dyadmbl  23898  vitalilem5  23910  vitali  23911  mbfimaopnlem  23953  mbflimsup  23964  0plef  23970  i1fima  23976  i1fima2  23977  i1fd  23979  itg1ge0  23984  itg10  23986  i1f1lem  23987  i1fadd  23993  i1fmul  23994  i1fmulc  24001  mbfi1fseqlem5  24017  itg2addlem  24056  reldv  24165  dvbsss  24197  dvef  24274  lhop1lem  24307  deg1fvi  24376  plypf1  24499  coeeulem  24511  coeeu  24512  vieta1lem2  24597  aannenlem3  24616  aalioulem3  24620  dvradcnv  24706  pserulm  24707  pserdvlem2  24713  sinhalfpilem  24746  sincos4thpi  24796  tan4thpi  24797  sincos6thpi  24798  pige3ALT  24802  resinf1o  24815  tanord1  24816  tanregt0  24818  efabl  24829  relogrn  24840  dfrelog  24844  logneg  24866  logltb  24878  logcn  24925  logf1o2  24928  dvlog  24929  efopnlem2  24935  efopn  24936  logccv  24941  dvsqrt  25018  dvcnsqrt  25020  cxpcn3  25024  logblog  25065  angpined  25103  1cubr  25115  asinsin  25165  asin1  25167  reasinsin  25169  atan0  25181  atanbnd  25199  atan1  25201  log2cnv  25218  log2ub  25223  log2le1  25224  birthday  25228  amgmlem  25263  emcllem5  25273  emgt0  25280  harmonicbnd3  25281  ftalem3  25348  basellem4  25357  sgmf  25418  ppi1  25437  cht1  25438  vma1  25439  ppiltx  25450  sqff1o  25455  ppiublem1  25474  ppiublem2  25475  ppiub  25476  chtub  25484  dchreq  25530  bposlem7  25562  bposlem8  25563  bposlem9  25564  lgsdir2lem2  25598  lgsdir2lem3  25599  chebbnd1  25744  chto1ub  25748  chpo1ubb  25753  pntibndlem1  25861  tgldimor  25984  tglnfn  26029  axlowdimlem4  26428  axlowdimlem16  26440  axlowdim  26444  upgrfi  26573  lfgrnloop  26607  lfuhgr1v0e  26733  usgrexmplef  26738  usgrres  26787  vdegp1bi  27016  vtxdginducedm1lem2  27019  pthdlem2  27251  wpthswwlks2on  27461  0ewlk  27637  0pth  27648  konigsbergiedgw  27774  konigsberglem1  27778  konigsberglem2  27779  konigsberglem3  27780  konigsberglem4  27781  konigsberglem5  27782  ex-dif  27974  ex-un  27975  ex-in  27976  ex-fl  27998  avril1  28013  9p10ne21fool  28021  n0lplig  28031  cnidOLD  28130  cnnvm  28230  ipasslem8  28385  ipasslem10  28387  hvsubf  28565  normlem1  28660  normlem6  28665  normlem7  28666  norm-ii-i  28687  norm3adifii  28698  hilid  28711  hlimf  28787  hhssabloi  28812  hhssnv  28814  hhshsslem1  28817  shincli  28914  shsval2i  28939  shs0i  29001  chj0i  29007  chm1i  29008  chincli  29012  chdmm1i  29029  shjshsi  29044  chsup0  29100  h1de2bi  29106  spansnpji  29130  cmcmlem  29143  cmcmii  29149  cmcm2ii  29150  cmcm3ii  29151  pjidmi  29225  pjssmii  29233  pj0i  29245  pjocini  29250  mayetes3i  29281  df0op2  29304  hoaddcomi  29324  hoaddassi  29328  hocadddiri  29331  hocsubdiri  29332  hoaddid1i  29338  ho0coi  29340  hoid1i  29341  hoid1ri  29342  hodseqi  29346  honegsubi  29348  adj1o  29446  hoddii  29541  lnopunilem1  29562  lnopunilem2  29563  nmcopexi  29579  nmcopex  29581  nmcoplb  29582  nmcfnexi  29603  nmcfnex  29605  nmcfnlb  29606  adjbd1o  29637  adjcoi  29652  nmopcoadji  29653  opsqrlem6  29697  pjsdii  29707  pjddii  29708  pjidmcoi  29729  pjtoi  29731  pjin1i  29744  pjclem1  29747  stji1i  29794  inindif  30048  iuninc  30075  fnresin  30129  rinvf1o  30132  suppss2f  30140  xppreima  30150  ofoprabco  30165  gtiso  30189  df1stres  30192  df2ndres  30193  snct  30202  padct  30208  fsuppcurry1  30214  fsuppcurry2  30215  ffsrn  30218  fpwrelmapffs  30223  nnindf  30282  nn0min  30284  dp2lt  30308  dp2ltsuc  30309  dp2ltc  30310  dplti  30328  dpmul  30336  dpmul4  30337  ressplusf  30369  xrsclat  30399  xrge0base  30404  xrge00  30405  xrnarchi  30479  xrge0slmod  30596  ccfldsrarelvec  30685  ccfldextdgrr  30686  locfinreflem  30748  locfinref  30749  unicls  30790  sqsscirc1  30795  mhmhmeotmd  30814  rmulccn  30815  raddcn  30816  xrge0iifiso  30822  xrge0iifhmeo  30823  lmxrge0  30839  cnzh  30855  rezh  30856  qqh0  30869  qqh1  30870  qqhre  30905  rrhre  30906  esumnul  30951  esum0  30952  esumsnf  30967  esumpfinvallem  30977  esumpfinvalf  30979  esumpcvgval  30981  esumcvgsum  30991  esumsup  30992  esumcvgre  30994  sigaclfu2  31025  dmsigagen  31048  ldgenpisyslem1  31067  ddemeas  31140  imambfm  31165  mbfmvolf  31169  br2base  31172  omssubadd  31203  sibfof  31243  sitg0  31249  eulerpartlemt  31274  eulerpartgbij  31275  0rrv  31355  coinfliplem  31382  coinflipprob  31383  coinfliprv  31386  ballotlem2  31392  ballotlem4  31402  ballotlem5  31403  ballotlemi1  31406  ballotlem7  31439  ballotth  31441  signsplypnf  31466  signsply0  31467  signsw0g  31472  signswch  31477  signsvf0  31498  hashreprin  31539  reprfz1  31543  chtvalz  31548  hgt750lemd  31567  hgt750lem  31570  hgt750lem2  31571  bnj521  31655  bnj1098  31703  bnj1109  31706  bnj1131  31707  bnj1533  31771  bnj151  31796  bnj580  31832  bnj852  31840  bnj864  31841  bnj865  31842  bnj978  31868  bnj1021  31883  bnj907  31884  bnj1093  31897  bnj1145  31910  bnj1172  31918  bnj1174  31920  bnj1176  31922  bnj1186  31924  subfacf  32007  subfacp1lem1  32011  subfacp1lem5  32016  subfacp1lem6  32017  subfacval3  32021  erdszelem2  32024  kur14lem4  32041  ioosconn  32079  iccllysconn  32082  msrfo  32313  mthmpps  32349  problem5  32432  quad3  32433  circum  32437  axextprim  32447  axrepprim  32448  axunprim  32449  axinfprim  32452  axacprim  32453  logi  32486  bcneg1  32488  setinds  32543  dfon2lem2  32549  dfon2lem4  32551  axextdfeq  32563  poseq  32616  frrlem4  32647  nosgnn0  32686  sltsolem1  32701  bdayfo  32703  nolt02o  32720  noetalem3  32740  fobigcup  32882  snelsingles  32904  fullfunfnv  32928  fullfunfv  32929  rankaltopb  32961  rank0  33152  rankeq1o  33153  hfuni  33166  fneer  33222  neibastop1  33228  nabi1i  33263  nabi2i  33264  limsucncmpi  33313  knoppcnlem8  33359  knoppcnlem11  33362  cnndvlem1  33396  bj-consensusALT  33429  bj-axsep  33623  bj-dtru  33625  bj-sbidmOLD  33665  bj-n0i  33757  bj-snsetex  33793  bj-tagss  33810  bj-2upln0  33853  bj-2upln1upl  33854  bj-nuliota  33861  bj-0int  33903  bj-elid  33938  bj-inftyexpitaufo  33953  bj-pinftyccb  33972  bj-minftyccb  33976  bj-pinftynminfty  33978  f1omptsnlem  34059  mptsnunlem  34061  topdifinffinlem  34070  relowlpssretop  34087  1oequni2o  34091  pibt2  34139  imadifss  34308  tan2h  34325  poimirlem3  34336  poimirlem9  34342  poimirlem16  34349  poimirlem17  34350  poimirlem18  34351  poimirlem19  34352  poimirlem20  34353  poimirlem22  34355  poimirlem30  34363  mblfinlem1  34370  mblfinlem2  34371  ovoliunnfl  34375  voliunnfl  34377  itg2addnclem  34384  itg2addnclem2  34385  asindmre  34418  areacirclem1  34423  fdc  34462  cntotbnd  34516  heiborlem6  34536  rrnval  34547  reheibor  34559  rngosn3  34644  ineqcomi  34949  brcnvrabga  35045  cnvresrn  35051  moantr  35062  inxp2  35064  dfxrn2  35073  cnvcosseq  35127  refrelcosslem  35147  1cosscnvxrn  35160  redundss3  35308  refrelsredund3  35314  refrelredund3  35317  prter2  35462  renegclALT  35544  mapdunirnN  38231  sn-dtru  38556  sqdeccom12  38607  resubf  38644  dffltz  38678  rntrclfvOAI  38683  diophrw  38751  rabren3dioph  38808  pellexlem6  38827  pellex  38828  frmx  38906  frmy  38907  jm2.23  38989  jm2.27dlem3  39004  axac10  39026  pw2f1ocnv  39030  kelac2lem  39060  lmhmlnmsplit  39083  pwfi2f1o  39092  frlmpwfi  39094  ifpbiidcor  39236  cnvnonrel  39310  rnnonrel  39313  resnonrel  39314  cononrel1  39316  cononrel2  39317  fvnonrel  39319  cnvcnvintabd  39322  cnvintabd  39325  rclexi  39338  rtrclex  39340  clcnvlem  39346  cnvrcl0  39348  dmtrcl  39350  rntrcl  39351  dfrtrcl5  39352  iunrelexp0  39410  dmtrclfvRP  39438  rntrclfv  39440  corcltrcl  39447  cotrclrcl  39450  0heALT  39492  frege54cor1a  39573  dssmapnvod  39729  uneqsn  39736  clsk3nimkb  39753  gneispace  39847  int-sqdefd  39899  int-sqgeq0d  39904  rr-groth  40010  rr-grothprim  40011  seff  40057  expgrowthi  40081  expgrowth  40083  binomcxplemnotnn0  40104  ee233  40272  ax6e2nd  40311  in1  40324  dfvd2ani  40336  dfvd2i  40338  dfvd3i  40345  dfvd3ani  40348  e0bi  40529  uun2221  40566  uun2221p1  40567  uun2221p2  40568  en3lpVD  40598  relopabVD  40654  ax6e2ndVD  40661  ax6e2ndALT  40683  pssnssi  40790  nnf1oxpnn  40882  icof  40907  negpilt0  40975  xrgtso  41042  supxrleubrnmptf  41158  xrpnf  41193  ioontr  41218  iccdifioo  41222  iccdifprioo  41223  uzinico2  41269  fsummulc1f  41282  fsumiunss  41287  fnlimfvre2  41389  limsupreuz  41449  limsupvaluz2  41450  limsup10ex  41485  icccncfext  41600  dvcosre  41626  dvsinax  41627  ioodvbdlimc1lem2  41647  ioodvbdlimc2lem  41649  dvmptmulf  41652  dvnmul  41658  dvmptfprodlem  41659  dvnprodlem2  41662  stoweidlem1  41717  stoweidlem26  41742  stoweidlem34  41750  stoweidlem44  41760  stoweid  41779  stirlinglem5  41794  dirkercncflem1  41819  fourierdlem44  41867  fourierdlem56  41878  fourierdlem62  41884  fourierdlem89  41911  fourierdlem91  41913  fourierdlem100  41922  fourierdlem102  41924  fourierdlem103  41925  fourierdlem104  41926  fourierdlem108  41930  fourierdlem112  41934  fourierdlem114  41936  fouriersw  41947  rrndistlt  42006  gsumge0cl  42084  sge0tsms  42093  sge0ltfirpmpt2  42139  ovn0  42279  hoidmv1le  42307  hoidmvle  42313  ovnsubadd2lem  42358  ovolval4lem1  42362  vonioolem2  42394  smflimlem3  42480  nsssmfmbf  42486  axorbtnotaiffb  42569  axorbciffatcxorb  42571  abnotbtaxb  42581  euabsneu  42668  sprval  43009  fmtnoinf  43066  1nevenALTV  43224  nfermltl8rev  43275  nfermltl2rev  43276  nnsum3primes4  43321  tgblthelfgott  43348  tgoldbachlt  43349  ldepslinc  43931  rrx2plordso  44079  alimp-no-surprise  44249  aacllem  44269  amgmwlem  44270  amgmlemALT  44271