Theorem mpbi 229

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  pm5.74i  270  notbii  319  biluk  386  pm5.19  387  pm3.24  402  dfbi  475  pm4.71i  559  pm5.32i  574  biadani  816  biadanii  818  imori  850  ori  857  pm5.16  1010  dn1  1054  3ori  1422  cadan  1614  nic-dfim  1675  nic-dfneg  1676  nic-mp  1677  nic-mpALT  1678  tbw-negdf  1705  rb-imdf  1756  nfri  1795  mpgbi  1804  19.35i  1884  nfim1  2195  19.36i  2227  ax6  2385  sbie  2507  datisi  2682  disamis  2683  dimatis  2690  fresison  2691  bamalip  2694  axi12  2708  eqcomi  2748  eqtri  2767  eleqtri  2838  nfnfc  2920  neii  2946  necomi  2999  neeqtri  3017  neli  3052  nfra2wOLD  3154  nrex  3198  rexlimiv  3210  rexlimi  3245  eueqi  3647  euxfr2w  3658  euxfr2  3660  reuxfrd  3686  cdeqri  3704  sseqtri  3961  3sstr3i  3967  pssn2lp  4040  equncomi  4093  unssi  4123  ssini  4170  unabs  4193  inabs  4194  dfin4  4206  vn0  4277  difidALT  4310  ab0orv  4317  ab0orvALT  4318  disjdif  4410  difin0  4412  pwundif  4564  snid  4602  rabrsn  4665  iinrab2  5003  symdifv  5019  rintn0  5042  breqtri  5103  axsepgfromrep  5224  bm1.3ii  5229  ax6vsep  5230  notzfaus  5288  zfpow  5292  dtru  5296  dtruALT  5314  reusv2lem4  5327  dtruALT2  5361  op1stb  5388  copsexgw  5406  copsexg  5407  uniop  5431  pwundifOLD  5485  rn0  5832  dmresi  5958  somincom  6036  cnvimassrndm  6052  cnvcnv  6092  elid  6099  rescnvcnv  6104  cnvcnvres  6105  cocnvcnv2  6159  cores2  6160  co01  6162  cnviin  6186  predres  6239  onunisuci  6377  iota4an  6412  fnopab  6567  mpt0  6571  fnmpti  6572  f1cnvcnv  6676  f1ovi  6750  eliman0  6803  fvco4i  6863  cnvimainrn  6938  fmpti  6980  funiunfv  7115  oprabss  7372  relmptopab  7510  zfun  7580  tfinds2  7698  omon  7712  2nd0  7824  f1stres  7841  f2ndres  7842  cnvoprab  7886  relmpoopab  7918  df1st2  7922  df2nd2  7923  fsplit  7941  fsplitOLD  7942  reldmtpos  8034  dftpos4  8045  tpostpos  8046  tpos0  8056  frrlem4  8089  wfrlem4OLD  8127  smo0  8173  tfrlem14  8206  tfrlem16  8208  rdgsucg  8238  rdglimg  8240  frfnom  8250  oawordeulem  8361  uniixp  8683  dfdom2  8737  ssdomg  8757  xpcomf1o  8817  sbthlem5  8843  limensuci  8905  fiint  9052  fidomdm  9057  residfi  9061  pwfilemOLD  9074  mptfi  9079  fisn  9147  dffi3  9151  ordtypelem6  9243  ordtypelem7  9244  wemaplem2  9267  harwdom  9311  suc11reg  9338  zfinf  9358  axinf2  9359  noinfep  9379  cantnfvalf  9384  cantnflt  9391  cantnf0  9394  cantnf  9412  ttrclco  9437  tz9.1c  9471  tc2  9483  r111  9517  r1tr2  9519  r1ordg  9520  r1sssuc  9525  r1val1  9528  tz9.13  9533  r1elssi  9547  pwwf  9549  rankopb  9594  rankeq0b  9602  ranksuc  9607  rankmapu  9620  rankxplim3  9623  rankxpsuc  9624  cp  9633  karden  9637  card0  9700  cardlim  9714  cardom  9728  infxpenlem  9753  alephsuc2  9820  alephgeom  9822  unialeph  9841  dfac4  9862  dfacacn  9881  dju1dif  9912  dju1p1e2  9913  infdju1  9929  ackbij1lem13  9972  ackbij2  9983  cf0  9991  cfsuc  9997  cfom  10004  cfslb2n  10008  ominf4  10052  fin23lem17  10078  fin23lem28  10080  fin23lem30  10082  fin23lem31  10083  fin23lem40  10091  isfin1-3  10126  dfacfin7  10139  fin1a2lem6  10145  itunitc1  10160  axcc3  10178  dcomex  10187  axdc2lem  10188  axcclem  10197  zfac  10200  ac3  10202  ackm  10205  axac2  10206  axac  10207  axaci  10208  cardeqv  10209  numth2  10211  numth  10212  dmct  10264  brdom3  10268  fin71ac  10273  cardf  10290  aleph1  10311  cfpwsdom  10324  smobeth  10326  zfcndrep  10354  zfcndpow  10356  zfcndac  10359  gch2  10415  wunex3  10481  tskpr  10510  inar1  10515  rankcf  10517  tskcard  10521  tskuni  10523  grothpw  10566  axgroth4  10572  grothprim  10574  inaprc  10576  dmaddpi  10630  dmmulpi  10631  1lt2pi  10645  addpqf  10684  mulpqf  10686  1lt2nq  10713  supsrlem  10851  ssxr  11028  gtso  11040  subf  11206  negne0i  11279  mulnzcnopr  11604  infrenegsup  11941  nnne0  11990  halflt1  12174  nn0ssz  12324  3halfnz  12382  zeo  12389  numlt  12444  numltc  12445  le9lt10  12446  decle  12453  uzf  12567  xaddf  12940  xsubge0  12977  xmulf  12988  ixxf  13071  ixxssxr  13073  iooval2  13094  ioof  13161  unirnioo  13163  dfioo2  13164  fzval2  13224  fzf  13225  0nelfz1  13257  fz10  13259  fzpreddisj  13287  4fvwrd4  13358  fzof  13366  fzo0  13392  fldiv4p1lem1div2  13536  fldiv4lem1div2  13538  om2uzoi  13656  faclbnd4lem1  13988  hashkf  14027  hashgval  14028  hashinf  14030  hashresfn  14035  hashnn0n0nn  14087  hashge3el3dif  14181  rev0  14458  s2dm  14584  f1oun2prg  14611  trclublem  14687  sqrt2gt1lt2  14967  limsupgord  15162  fclim  15243  fsumrelem  15500  ackbijnn  15521  incexclem  15529  incexc  15530  arisum2  15554  georeclim  15565  geoisumr  15571  0.999...  15574  risefall0lem  15717  ege2le3  15780  sin0  15839  ef01bndlem  15874  cos2bnd  15878  cos01gt0  15881  sincos2sgn  15884  sin4lt0  15885  rpnnen2lem3  15906  rpnnen2lem9  15912  rexpen  15918  cnso  15937  dvdslelem  15999  divalglem1  16084  divalglem5  16087  divalglem6  16088  divalglem10  16092  flodddiv4  16103  0bits  16127  sadcf  16141  sadcadd  16146  bitsshft  16163  smupf  16166  gcdf  16200  eucalgf  16269  2prm  16378  dfphi2  16456  pockthi  16589  prmrec  16604  vdwapf  16654  vdwlem6  16668  karatsuba  16766  1259lem5  16817  2503lem3  16821  4001lem4  16826  structcnvcnv  16835  structfn  16838  strleun  16839  imasvscafn  17229  xpsff1o  17259  wunnat  17653  wunnatOLD  17654  dfinito3  17701  dftermo3  17702  eldmcoa  17761  coapm  17767  catcfuccl  17815  catcfucclOLD  17816  catcxpccl  17905  catcxpcclOLD  17906  yonedainv  17980  smndex1bas  18526  smndex1n0mnd  18532  grpinvfvi  18603  mulgfvi  18687  symgsssg  19056  symgfisg  19057  psgnunilem5  19083  sylow3lem2  19214  oppglsm  19228  efgmf  19300  efgval  19304  efgsf  19316  0frgp  19366  dmdprd  19582  dprdval  19587  invrfval  19896  drngui  19978  rmodislmod  20172  rmodislmodOLD  20173  lssintcl  20207  cnfldfun  20590  cnfldfunOLD  20591  cnfld0  20603  cnfld1  20604  cnfldsub  20607  xrsds  20622  psgnghm  20766  zrhpsgnmhm  20770  recrng  20807  ocv1  20865  dsmmbas2  20925  mplsubrglem  21191  opsrtoslem2  21244  mdetralt  21738  maducoeval2  21770  eltpsi  22075  unitg  22098  fctop  22135  cctop  22137  ppttop  22138  epttop  22140  leordtvallem1  22342  leordtvallem2  22343  iccordt  22346  iscnp2  22371  discmp  22530  conncompcld  22566  1stcrestlem  22584  2ndcdisj  22588  topnlly  22623  disllycmp  22630  dis1stc  22631  txuni2  22697  xkotf  22717  dfac14lem  22749  prdstps  22761  txindis  22766  tx1stc  22782  xkohaus  22785  xkoptsub  22786  cnmpt1st  22800  cnmpt2nd  22801  ptcmpfi  22945  trfil1  23018  fin1aufil  23064  tgpconncompeqg  23244  tgpconncomp  23245  trust  23362  met1stc  23658  dscmet  23709  retopon  23908  cnfldtopon  23927  xrsxmet  23953  xrsmopn  23956  iimulcn  24082  icopnfhmeo  24087  iccpnfhmeo  24089  xrhmeo  24090  cnheiborlem  24098  lebnumii  24110  ishtpy  24116  htpycc  24124  pco1  24159  pcohtpylem  24163  pcopt  24166  pcopt2  24167  pcoass  24168  pcorevlem  24170  rrxcph  24537  rrx0el  24543  ovoliunlem3  24649  ovolicc1  24661  ovolicc2  24667  volf  24674  ioorf  24718  dyadf  24736  dyadmbl  24745  vitalilem5  24757  vitali  24758  mbfimaopnlem  24800  mbflimsup  24811  0plef  24817  i1fima  24823  i1fima2  24824  i1fd  24826  itg1ge0  24831  itg10  24833  i1f1lem  24834  i1fadd  24840  i1fmul  24841  i1fmulc  24849  mbfi1fseqlem5  24865  itg2addlem  24904  reldv  25015  dvbsss  25047  dvef  25125  lhop1lem  25158  deg1fvi  25231  plypf1  25354  coeeulem  25366  coeeu  25367  vieta1lem2  25452  aannenlem3  25471  aalioulem3  25475  dvradcnv  25561  pserulm  25562  pserdvlem2  25568  sinhalfpilem  25601  sincos4thpi  25651  tan4thpi  25652  sincos6thpi  25653  pige3ALT  25657  resinf1o  25673  tanord1  25674  tanregt0  25676  efabl  25687  relogrn  25698  dfrelog  25702  logneg  25724  logltb  25736  logcn  25783  logf1o2  25786  dvlog  25787  efopnlem2  25793  efopn  25794  logccv  25799  dvsqrt  25876  dvcnsqrt  25878  cxpcn3  25882  logblog  25923  angpined  25961  1cubr  25973  asinsin  26023  asin1  26025  reasinsin  26027  atan0  26039  atanbnd  26057  atan1  26059  log2cnv  26075  log2ub  26080  log2le1  26081  birthday  26085  amgmlem  26120  emcllem5  26130  emgt0  26137  harmonicbnd3  26138  ftalem3  26205  basellem4  26214  sgmf  26275  ppi1  26294  cht1  26295  vma1  26296  ppiltx  26307  sqff1o  26312  ppiublem1  26331  ppiublem2  26332  ppiub  26333  chtub  26341  dchreq  26387  bposlem7  26419  bposlem8  26420  bposlem9  26421  lgsdir2lem2  26455  lgsdir2lem3  26456  chebbnd1  26601  chto1ub  26605  chpo1ubb  26610  pntibndlem1  26718  tgldimor  26844  tglnfn  26889  axlowdimlem4  27294  axlowdimlem16  27306  axlowdim  27310  upgrfi  27442  lfgrnloop  27476  lfuhgr1v0e  27602  usgrexmplef  27607  usgrres  27656  vdegp1bi  27885  vtxdginducedm1lem2  27888  pthdlem2  28115  wpthswwlks2on  28305  0ewlk  28457  0pth  28468  konigsbergiedgw  28591  konigsberglem1  28595  konigsberglem2  28596  konigsberglem3  28597  konigsberglem4  28598  konigsberglem5  28599  ex-dif  28766  ex-un  28767  ex-in  28768  ex-fl  28790  avril1  28806  9p10ne21fool  28814  n0lplig  28824  cnidOLD  28923  cnnvm  29023  ipasslem8  29178  ipasslem10  29180  hvsubf  29356  normlem1  29451  normlem6  29456  normlem7  29457  norm-ii-i  29478  norm3adifii  29489  hilid  29502  hlimf  29578  hhssabloi  29603  hhssnv  29605  hhshsslem1  29608  shincli  29703  shsval2i  29728  shs0i  29790  chj0i  29796  chm1i  29797  chincli  29801  chdmm1i  29818  shjshsi  29833  chsup0  29889  h1de2bi  29895  spansnpji  29919  cmcmlem  29932  cmcmii  29938  cmcm2ii  29939  cmcm3ii  29940  pjidmi  30014  pjssmii  30022  pj0i  30034  pjocini  30039  mayetes3i  30070  df0op2  30093  hoaddcomi  30113  hoaddassi  30117  hocadddiri  30120  hocsubdiri  30121  hoaddid1i  30127  ho0coi  30129  hoid1i  30130  hoid1ri  30131  hodseqi  30135  honegsubi  30137  adj1o  30235  hoddii  30330  lnopunilem1  30351  lnopunilem2  30352  nmcopexi  30368  nmcopex  30370  nmcoplb  30371  nmcfnexi  30392  nmcfnex  30394  nmcfnlb  30395  adjbd1o  30426  adjcoi  30441  nmopcoadji  30442  opsqrlem6  30486  pjsdii  30496  pjddii  30497  pjidmcoi  30518  pjtoi  30520  pjin1i  30533  pjclem1  30536  stji1i  30583  reuxfrdf  30818  inindif  30842  iuninc  30879  fnresin  30940  rinvf1o  30944  suppss2f  30953  xppreima  30962  ofoprabco  30980  fressupp  31001  supppreima  31004  fsupprnfi  31005  gtiso  31012  df1stres  31015  df2ndres  31016  snct  31027  padct  31033  fsuppcurry1  31039  fsuppcurry2  31040  ffsrn  31043  fpwrelmapffs  31048  fzodif1  31093  nnindf  31112  nn0min  31113  dp2lt  31138  dp2ltsuc  31139  dp2ltc  31140  dplti  31158  dpmul  31166  dpmul4  31167  ressplusf  31214  xrsclat  31268  xrge0base  31273  xrge00  31274  xrnarchi  31417  xrge0slmod  31527  ccfldsrarelvec  31720  ccfldextdgrr  31721  locfinreflem  31769  locfinref  31770  unicls  31832  sqsscirc1  31837  mhmhmeotmd  31856  rmulccn  31857  raddcn  31858  xrge0iifiso  31864  xrge0iifhmeo  31865  lmxrge0  31881  cnzh  31899  rezh  31900  qqh0  31913  qqh1  31914  qqhre  31949  rrhre  31950  esumnul  31995  esum0  31996  esumsnf  32011  esumpfinvallem  32021  esumpfinvalf  32023  esumpcvgval  32025  esumcvgsum  32035  esumsup  32036  esumcvgre  32038  sigaclfu2  32068  dmsigagen  32091  ddemeas  32183  mbfmvolf  32212  br2base  32215  omssubadd  32246  sibfof  32286  sitg0  32292  eulerpartlemt  32317  eulerpartgbij  32318  0rrv  32397  coinfliplem  32424  coinflipprob  32425  coinfliprv  32428  ballotlem2  32434  ballotlem4  32444  ballotlem5  32445  ballotlemi1  32448  ballotlem7  32481  ballotth  32483  signsplypnf  32508  signsply0  32509  signsw0g  32514  signswch  32519  signsvf0  32538  hashreprin  32579  reprfz1  32583  chtvalz  32588  hgt750lemd  32607  hgt750lem  32610  hgt750lem2  32611  bnj521  32695  bnj1098  32742  bnj1109  32745  bnj1131  32746  bnj1533  32811  bnj151  32836  bnj580  32872  bnj852  32880  bnj864  32881  bnj865  32882  bnj978  32908  bnj1021  32925  bnj907  32926  bnj1093  32939  bnj1145  32952  bnj1172  32960  bnj1174  32962  bnj1176  32964  bnj1186  32966  fineqvac  33045  subfacf  33116  subfacp1lem1  33120  subfacp1lem5  33125  subfacp1lem6  33126  subfacval3  33130  erdszelem2  33133  kur14lem4  33150  ioosconn  33188  iccllysconn  33191  satfn  33296  fmlaomn0  33331  gonan0  33333  goaln0  33334  elnanelprv  33370  msrfo  33487  mthmpps  33523  problem5  33606  quad3  33607  circum  33611  axextprim  33621  axrepprim  33622  axunprim  33623  axinfprim  33626  axacprim  33627  logi  33679  bcneg1  33681  setinds  33733  dfon2lem2  33739  dfon2lem4  33741  axextdfeq  33752  frpoins3xpg  33766  frpoins3xp3g  33767  poxp2  33769  poseq  33781  nosgnn0  33840  sltsolem1  33857  bdayfo  33859  nolt02o  33877  nogt01o  33878  noetasuplem4  33918  noetainflem4  33922  scutbdaybnd2lim  33990  madeun  34045  fobigcup  34181  snelsingles  34203  fullfunfnv  34227  fullfunfv  34228  rankaltopb  34260  rank0  34451  rankeq1o  34452  hfuni  34465  fneer  34521  neibastop1  34527  nabi1i  34562  nabi2i  34563  limsucncmpi  34613  knoppcnlem8  34659  knoppcnlem11  34662  cnndvlem1  34696  bj-consensusALT  34739  bj-dtru  34978  bj-sbidmOLD  35013  bj-n0i  35119  bj-snsetex  35132  bj-tagss  35149  bj-2upln0  35192  bj-2upln1upl  35193  bj-nuliota  35207  bj-0int  35251  bj-elid5  35319  bj-inftyexpitaufo  35352  bj-pinftyccb  35371  bj-minftyccb  35375  bj-pinftynminfty  35377  bj-isrvec  35444  iccioo01  35477  f1omptsnlem  35486  mptsnunlem  35488  topdifinffinlem  35497  relowlpssretop  35514  1oequni2o  35518  pibt2  35567  imadifss  35731  tan2h  35748  poimirlem3  35759  poimirlem9  35765  poimirlem16  35772  poimirlem17  35773  poimirlem18  35774  poimirlem19  35775  poimirlem20  35776  poimirlem22  35778  poimirlem30  35786  mblfinlem1  35793  mblfinlem2  35794  ovoliunnfl  35798  voliunnfl  35800  itg2addnclem  35807  itg2addnclem2  35808  asindmre  35839  areacirclem1  35844  fdc  35882  cntotbnd  35933  heiborlem6  35953  rrnval  35964  reheibor  35976  rngosn3  36061  brcnvrabga  36456  cnvresrn  36462  moantr  36473  inxp2  36476  dfxrn2  36485  cnvcosseq  36539  refrelcosslem  36559  1cosscnvxrn  36572  redundss3  36720  refrelsredund3  36726  refrelredund3  36729  prter2  36874  renegclALT  36956  mapdunirnN  39643  lcmeprodgcdi  39995  3factsumint2  40010  3factsumint3  40011  3factsumint4  40012  3factsumint  40013  lcmineqlem4  40020  3lexlogpow5ineq1  40042  3lexlogpow2ineq1  40046  dvrelogpow2b  40056  aks4d1p1p4  40059  aks4d1p8  40075  2ap1caineq  40081  sticksstones1  40082  sticksstones2  40083  metakunt6  40110  metakunt24  40128  sn-dtru  40168  sqdeccom12  40297  resubf  40344  sn-0ne2  40369  sn-subf  40390  sn-0lt1  40412  reneg1lt0  40414  rntrclfvOAI  40493  diophrw  40561  rabren3dioph  40617  pellexlem6  40636  pellex  40637  frmx  40715  frmy  40716  jm2.23  40798  jm2.27dlem3  40813  axac10  40835  pw2f1ocnv  40839  kelac2lem  40869  lmhmlnmsplit  40892  pwfi2f1o  40901  frlmpwfi  40903  ifpbiidcor  41043  alephiso2  41118  alephiso3  41119  cnvnonrel  41149  rnnonrel  41152  resnonrel  41153  cononrel1  41155  cononrel2  41156  fvnonrel  41158  cnvcnvintabd  41161  cnvintabd  41164  rclexi  41176  rtrclex  41178  clcnvlem  41184  cnvrcl0  41186  dmtrcl  41188  rntrcl  41189  dfrtrcl5  41190  iunrelexp0  41263  dmtrclfvRP  41291  rntrclfv  41293  corcltrcl  41300  cotrclrcl  41303  0heALT  41344  frege54cor1a  41425  uneqsn  41586  clsk3nimkb  41603  int-sqdefd  41745  int-sqgeq0d  41750  rr-groth  41870  rr-grothprim  41871  rr-grothshort  41875  seff  41880  expgrowthi  41904  expgrowth  41906  binomcxplemnotnn0  41927  ee233  42092  ax6e2nd  42131  in1  42144  dfvd2ani  42156  dfvd2i  42158  dfvd3i  42165  dfvd3ani  42168  e0bi  42349  uun2221  42386  uun2221p1  42387  uun2221p2  42388  en3lpVD  42418  relopabVD  42474  ax6e2ndVD  42481  ax6e2ndALT  42503  pssnssi  42604  nnf1oxpnn  42687  icof  42712  negpilt0  42772  xrgtso  42838  supxrleubrnmptf  42945  xrpnf  42980  ioontr  43003  iccdifioo  43007  iccdifprioo  43008  uzinico2  43054  fsummulc1f  43066  fsumiunss  43070  fnlimfvre2  43172  limsupreuz  43232  limsupvaluz2  43233  limsup10ex  43268  icccncfext  43382  dvcosre  43407  dvsinax  43408  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvmptmulf  43432  dvnmul  43438  dvmptfprodlem  43439  dvnprodlem2  43442  stoweidlem1  43496  stoweidlem26  43521  stoweidlem34  43529  stoweidlem44  43539  stoweid  43558  stirlinglem5  43573  dirkercncflem1  43598  fourierdlem44  43646  fourierdlem56  43657  fourierdlem62  43663  fourierdlem89  43690  fourierdlem91  43692  fourierdlem100  43701  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem108  43709  fourierdlem112  43713  fourierdlem114  43715  fouriersw  43726  rrndistlt  43785  gsumge0cl  43863  sge0tsms  43872  sge0ltfirpmpt2  43918  ovn0  44058  hoidmv1le  44086  hoidmvle  44092  ovnsubadd2lem  44137  ovolval4lem1  44141  vonioolem2  44173  smflimlem3  44259  nsssmfmbf  44265  axorbtnotaiffb  44349  axorbciffatcxorb  44351  abnotbtaxb  44361  euabsneu  44473  sprval  44883  fmtnoinf  44940  1nevenALTV  45095  nfermltl8rev  45146  nfermltl2rev  45147  nnsum3primes4  45192  tgblthelfgott  45219  tgoldbachlt  45220  ldepslinc  45802  ackval42  45994  rrx2plordso  46022  vsn  46109  sepfsepc  46173  alimp-no-surprise  46437  aacllem  46457  amgmwlem  46458  amgmlemALT  46459