Theorem mpbiri 260

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbiri.min	⊢ 𝜒
mpbiri.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbiri	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbiri

Step	Hyp	Ref	Expression
1		mpbiri.min	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		mpbiri.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbird 259	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  elimh  1091  spei  2419  nfald2  2470  nfabd2  2941  raleleq  3326  raleleqOLD  3327  ceqsexv2d  3497  dedhb  3660  csbie2df  4391  ssdifeq0  4434  dedth  4533  pwidgOLD  4570  snidg  4613  rexreusng  4632  exsnrex  4633  ifpr  4646  rmosn  4672  rabrsn  4677  prid1g  4713  tpid1g  4722  tpid2g  4724  tpid3g  4725  pwpw0  4765  sssn  4778  elpreqpr  4819  unimax  4897  intmin3  4928  eqbrtrdi  5133  al0ssb  5252  vneqv  5260  rabelpw  5286  intabs  5299  difelpw  5304  0inp0  5309  axpr  5378  intidg  5418  copsexgw  5452  copsexgwOLD  5453  copsexg  5454  euotd  5476  elopab  5491  elvvuni  5717  posn  5726  frsn  5728  eqrelriv  5754  relsnb  5768  relopabiALT  5789  opabid2  5794  ididg  5818  iss  6014  dfpo2  6272  ord0eln0  6391  sucidg  6418  nsuceq0  6420  funopg  6544  fn0  6641  f00  6735  f0bi  6736  f10d  6830  f1o00  6831  fo00  6832  brprcneu  6846  brprcneuALT  6847  dffn5  6914  fsn  7106  funop  7121  funsndifnop  7123  fnsnbOLD  7139  eufnfv  7202  f1ounsn  7245  f1eqcocnv  7274  nfriotadw  7350  nfriotad  7353  riotaprop  7369  oprabidw  7416  oprabid  7417  elrnmpo  7521  ov6g  7549  ovelrn  7561  caovmo  7622  offn  7662  caofinvl  7681  fr3nr  7744  onprc  7750  ordeleqon  7754  onint0  7763  0elsuc  7804  onuninsuci  7809  orduninsuc  7812  ordzsl  7814  onzsl  7815  tfinds  7829  limomss  7840  limom  7851  peano5  7863  xpexr  7888  eqop2  8002  opreuopreu  8004  1stconst  8067  2ndconst  8068  frxp2  8112  frxp3  8119  funsssuppss  8158  dftpos3  8212  dftpos4  8213  oawordeulem  8511  omwordi  8528  nnmwordi  8593  riiner  8760  ecopover  8791  map0g  8855  mapsnd  8857  elixpsn  8908  en0  8988  en0ALT  8989  en0r  8990  en1  8994  snfi  9013  fiprc  9014  sbthlem2  9049  sbthlem4  9051  sbthlem5  9052  0domg  9065  findcard  9121  findcard2  9122  nneneq  9163  sdom1  9183  1sdom2dom  9187  fineqvlem  9199  nfielex  9207  enp1i  9212  elfiun  9366  marypha1lem  9369  oicl  9467  oif  9468  oion  9474  hartogslem1  9480  hartogs  9482  wemapso2  9491  card2on  9492  0wdom  9508  brwdom2  9511  elirrv  9535  inf3lem6  9578  cantnflem3  9636  cantnflem4  9637  wemapwe  9642  cnfcom  9645  ssttrcl  9660  ttrclselem2  9671  tctr  9683  r1tr  9724  r1rankidb  9752  r1pw  9793  scottex  9833  scott0  9834  bnd2  9841  eldju2ndl  9872  tskwe  9898  oncard  9908  cardlim  9920  harsdom  9943  en2eleq  9954  dfac8alem  9975  cardaleph  10035  iunfictbso  10060  infmap2  10163  ackbij1lem18  10182  cff  10194  cfsuc  10204  cff1  10205  cflim2  10210  cfss  10212  sdom2en01  10249  infpssrlem4  10253  fin23lem7  10263  fin23lem11  10264  isfin2-2  10266  fin23lem26  10272  fin23lem19  10283  fin23lem17  10285  isf34lem2  10320  isf34lem4  10324  fin1a2lem6  10352  fin1a2lem10  10356  fin1a2lem12  10358  itunifn  10364  hsmexlem1  10373  axcc2lem  10383  dcomex  10394  axdc3lem4  10400  ondomon  10510  konigthlem  10516  pwcfsdom  10531  cfpwsdom  10532  axpowndlem3  10547  canth4  10595  canthnumlem  10596  canthwelem  10598  canthwe  10599  canthp1lem2  10601  pwfseqlem4  10610  pwfseqlem5  10611  gchaleph  10619  gch2  10623  winainflem  10641  0tsk  10703  rankcf  10725  tskcard  10729  gruina  10766  grutsk  10770  tskmid  10788  indpi  10855  nqereu  10877  mulcanenq  10908  recmulnq  10912  archnq  10928  ltsopr  10980  1ne0sr  11044  0idsr  11045  00sr  11047  leid  11269  lelttric  11280  divcan3  11861  divid  11866  div0  11868  lemul1a  12035  nn1suc  12222  nn0n0n1ge2b  12540  xnn0xr  12549  xnn0nemnf  12555  nn0lt10b  12625  nn0ind-raph  12663  elnn1uz2  12916  indstr2  12918  uzsupss  12931  rpnnen1lem4  12971  rpnnen1lem5  12972  xrnemnf  13109  xrnepnf  13110  mnfltxr  13119  xnn0n0n1ge2b  13124  xnn0ge0  13126  xrlttri  13131  xrlttr  13132  xrleid  13143  qbtwnxr  13193  xmullem2  13258  xlemul1a  13281  xrub  13305  reltxrnmnf  13336  ixxun  13355  xnn0xrge0  13500  fztpval  13581  fseq1p1m1  13593  elfznelfzob  13770  ltweuz  13964  fzfi  13975  fsuppmapnn0fiubex  13995  ser0f  14058  0exp  14100  faclbnd4lem1  14296  bcn1  14316  hashnemnf  14347  hashv01gt1  14348  hashsnle1  14420  hashgt12el2  14426  hashpw  14439  hashf1  14460  fz1isolem  14464  hash2prb  14475  hash3tpb  14498  0wrd0  14543  wrdlen1  14557  ccatvalfn  14584  eqs1  14616  wrdl1exs1  14617  swrdlen  14651  swrdwrdsymb  14666  swrdspsleq  14669  cats1un  14724  wrdind  14725  wrd2ind  14726  swrdccatin1  14728  repswsymballbi  14783  cshw1  14825  scshwfzeqfzo  14829  wrdl2exs2  14949  trclfvcotr  15012  relexp1g  15029  relexp0rel  15040  relexprelg  15041  relexpreld  15043  sqrt0  15244  sqrtsq  15272  mptfzshft  15781  prodf1f  15898  egt2lt3  16214  0dvds  16286  nn0onn  16390  nn0o  16393  divalgmod  16416  flodddiv4  16425  bitsp1o  16443  gcddvds  16513  bezout  16553  lcmdvds  16618  rpdvds  16670  1nprm  16689  prmind2  16695  dvdszzq  16732  nnoddn2prmb  16825  pcpre1  16854  vdwapf  16984  vdwapid1  16987  ram0  17034  ramz  17037  prmolefac  17058  cshws0  17113  prmlem0  17117  strle1  17170  restsspw  17436  prdsdsfn  17470  imasdsfn  17520  imasaddfnlem  17534  imasvscafn  17543  xpsfrnel  17568  isacs1i  17665  cidfn  17687  fnhomeqhomf  17699  comffn  17713  isoval  17774  sscres  17832  cofucl  17897  idffth  17944  ressffth  17949  cat1lem  18105  catcoppccl  18126  estrchomfn  18143  funcestrcsetclem4  18151  funcestrcsetclem7  18154  equivestrcsetc  18160  funcsetcestrclem4  18166  funcsetcestrclem7  18169  1stfcl  18205  2ndfcl  18206  prfcl  18211  evlfcl  18230  curf1cl  18236  curfcl  18240  hofcl  18267  yonedainv  18289  pospo  18351  lubfun  18358  glbfun  18371  joindmss  18385  meetdmss  18399  ipopos  18544  acsficl2d  18560  dirref  18609  mgmidcl  18676  mgmlrid  18677  ielefmnd  18897  smndex1basss  18918  smndex1n0mnd  18925  cntzssv  19344  idresperm  19402  symgvalstruct  19413  pmtrfmvdn0  19478  symggen  19486  psgnunilem1  19509  psgnprfval  19537  slwpgp  19629  frgpmhm  19781  frgpuptinv  19787  frgpup3lem  19793  gsumzoppg  19960  gsumcom2  19991  c0snmhm  20484  srhmsubc  20702  rhmsubclem1  20707  rrgsupp  20723  abv0  20845  zrhrhm  21536  psgnodpmr  21615  frlmphllem  21805  ellspd  21827  psrvscafval  21973  psrridm  21987  ltbwe  22070  psrbag0  22088  psrbagsn  22089  subrgascl  22092  psdmul  22204  mattpostpos  22487  mavmul0  22585  mavmul0g  22586  mdet0f1o  22626  m1detdiag  22630  m2detleiblem5  22658  m2detleiblem6  22659  m2detleiblem3  22662  m2detleiblem4  22663  maducoeval2  22673  d1mat2pmat  22772  chpmat1dlem  22868  chpmat1d  22869  baspartn  22987  eltg3  22995  topnex  23029  fctop  23037  cctop  23039  discld  23122  mretopd  23125  neipeltop  23162  neitr  23213  restcls  23214  ordtbaslem  23221  ordtuni  23223  idcn  23290  cnrmi  23393  cmpsublem  23432  cmpsub  23433  tgcmp  23434  uncmp  23436  hauscmplem  23439  cmpfi  23441  bwth  23443  1stcrestlem  23485  disllycmp  23531  dis1stc  23532  refref  23546  kgeni  23570  1stckgenlem  23586  kqffn  23758  snfil  23897  filconn  23916  cfinfil  23926  ufileu  23952  filufint  23953  fixufil  23955  cfinufil  23961  ufilen  23963  fin1aufil  23965  fmf  23978  rnelfm  23986  flimclslem  24017  hauspwpwf1  24020  supnfcls  24053  flimfnfcls  24061  fclscmp  24063  alexsubALTlem2  24081  alexsubALTlem3  24082  alexsubALT  24084  ptcmplem1  24085  cnextrel  24096  tsmsfbas  24161  ustref  24252  trust  24262  restutop  24270  isusp  24294  xmet0  24375  imasdsf1olem  24406  blfvalps  24416  blfps  24439  blf  24440  restmetu  24603  dscmet  24605  isngp2  24630  nm0  24662  nrginvrcn  24725  nmoix  24762  qdensere  24802  iccconn  24864  iccpnfcnv  24979  xrhmeo  24981  lebnumlem3  24998  metsscmetcld  25350  bcthlem5  25363  csschl  25411  rrxmfval  25441  minveclem3b  25463  cniccbdd  25496  ovolicc2lem4  25555  iunmbl  25588  ioorinv  25611  ioorcl  25612  i1f1lem  25724  limcvallem  25906  ellimc2  25912  limccnp  25926  limccnp2  25927  limcco  25928  perfdvf  25938  recnprss  25939  fncpn  25968  dvcmulf  25980  c1lip1  26032  lhop2  26050  q1pcl  26190  r1pdeglt  26193  ply1remlem  26198  plyssc  26233  ulm0  26424  cxpeq0  26713  cxplea  26731  cxplogb  26821  asinlem  26903  isppw2  27149  muval2  27168  dchrfi  27289  dchrpt  27301  bposlem6  27323  lgsdir2lem2  27360  lgsqr  27385  gausslemma2dlem4  27403  2lgslem2  27429  2lgslem3  27438  2lgs  27441  2sqlem7  27458  2sqlem11  27463  chtppilim  27509  nosgnn0i  27693  nolesgn2ores  27706  nogesgn1ores  27708  nosepnelem  27713  nosepdmlem  27717  nosupbnd1lem3  27744  nosupbnd1lem5  27746  nosupbnd2lem1  27749  noinfbnd1lem3  27759  noinfbnd1lem5  27761  noinfbnd2lem1  27764  oldval  27897  made0  27926  lrrecpo  28004  pncan2s  28137  divscan3d  28299  abssor  28309  om2noseqfo  28361  noseqrdglem  28368  noseqrdgfn  28369  noseqrdg0  28370  onsfi  28419  nohalf  28487  expsne0  28499  pw2divscan3d  28504  tgldimor  28641  tgcgr4  28670  tglnfn  28686  tglnunirn  28687  mirne  28806  mircinv  28807  perpln1  28849  perpln2  28850  lmiisolem  28935  xmstrkgc  29025  axcgrtr  29055  axsegconlem9  29065  axlowdimlem5  29086  axlowdimlem17  29098  axlowdim1  29099  uhgr0e  29211  edglnl  29283  uhgr0edgfi  29380  issubgr2  29412  subgrprop2  29414  egrsubgr  29417  0grsubgr  29418  0uhgrsubgr  29419  uhgrsubgrself  29420  nbgr1vtx  29498  nbgrssovtx  29501  nb3grprlem1  29520  uvtx01vtx  29537  cplgr1vlem  29569  cplgr1v  29570  usgrexilem  29580  wlkcomp  29770  wlk1walk  29778  wlkp1lem5  29815  uhgrwkspthlem1  29892  pthdlem1  29905  clwlkcomp  29918  lfgrn1cycl  29944  uspgrn2crct  29947  wwlksn0s  30000  usgrwwlks2on  30097  umgrwwlks2on  30098  clwwlkn  30167  clwwlkn1  30182  0ewlk  30255  1ewlk  30256  0spth  30267  upgr1wlkdlem2  30287  wlk2v2e  30298  upgr3v3e3cycl  30321  upgr4cycl4dv4e  30326  eupth0  30355  frgr0v  30403  frgr1v  30412  1vwmgr  30417  ex-opab  30573  grpoinvf  30674  nvmid  30801  nmlnoubi  30938  hiidrcl  31237  hsn0elch  31390  shjshseli  31635  cmbr4i  31743  dfiop2  31895  kbpj  32098  nmopun  32156  adjeq0  32233  kbass2  32259  pjssdif1i  32317  pjinvari  32333  pjcmul2i  32344  pj3i  32350  stge1i  32380  stle0i  32381  sumdmdlem2  32561  dmdbr6ati  32565  dmdbr7ati  32566  rabsnel  32641  unidifsnel  32676  unidifsnne  32677  disjdifprg  32717  ofoprabco  32809  padct  32863  fpwrelmapffslem  32877  nn0mnfxrd  32896  xrlelttric  32897  xnn0gt0  32914  iundisj2cnt  32944  f1ocnt  32945  fz1nnct  32946  fz1nntr  32947  hashxpe  32952  nn0min  32966  sgnmulsgn  32987  sgnmulsgp  32988  wrdt2ind  33085  xrge0tsmsbi  33208  opprabs  33624  rtelextdg2lem  33977  2sqr3minply  34031  locfinref  34092  dispcmp  34110  zartopn  34126  zarcmplem  34132  pstmxmet  34148  xrge0iifcnv  34184  xrge0iif1  34189  qqhre  34271  esumcl  34281  esumpr2  34318  esumpinfval  34324  esumpcvgval  34329  ofcfn  34351  pwsiga  34381  prsiga  34382  sigainb  34387  ldgenpisyslem1  34414  measiuns  34468  relfae  34498  pmeasmono  34575  sitgf  34598  eulerpartgbij  34623  signswch  34812  signslema  34813  signstlen  34818  signstfvn  34820  circlevma  34893  bnj216  34985  bnj151  35129  bnj517  35137  bnj970  35199  bnj1145  35245  bnj1498  35313  r1omhfb  35363  fineqvrep  35365  fineqvac  35367  fineqvnttrclselem1  35372  fineqvnttrclselem2  35373  fineqvnttrclse  35375  fineqvinfep  35376  r1omhfbregs  35388  wevgblacfn  35407  0nn0m1nnn0  35411  pthhashvtx  35426  acycgr0v  35446  prclisacycgr  35449  umgracycusgr  35452  cusgracyclt3v  35454  subfacp1lem5  35482  erdszelem8  35496  kur14lem1  35504  indispconn  35532  cvmsss2  35572  satfvsuclem2  35658  satfrel  35665  satfrnmapom  35668  satfv0fun  35669  satf00  35672  satf0suclem  35673  fmlasuc0  35682  msubrn  35827  dfon2lem7  36085  brbigcup  36194  elsingles  36214  fnimage  36225  funpartlem  36240  dfrdg4  36249  imagesset  36251  altopthsn  36259  elaltxp  36273  ellines  36450  linethru  36451  rankeq1o  36469  elhf2  36473  hfninf  36484  nn0prpwlem  36630  fneref  36658  neibastop2lem  36668  limsucncmpi  36753  tz9.1tco  36791  bj-exlimmpbir  37347  curryset  37379  bj-snglex  37406  bj-axnul  37505  bj-restpw  37530  bj-inftyexpidisj  37650  topdifinffinlem  37789  relowlssretop  37805  rdgeqoa  37812  finxpreclem6  37838  fvineqsneq  37854  pibt2  37859  poimirlem23  38090  poimirlem29  38096  poimirlem31  38098  volsupnfl  38112  cnambfre  38115  dvasin  38151  dvacos  38152  sdclem2  38189  sstotbnd2  38221  ssbnd  38235  ismgmOLD  38297  grpokerinj  38340  rngomndo  38382  isdrngo1  38403  ac6s6  38619  iss2  38791  relecxrn  38854  sucmapsuc  38936  cosselrels  39022  cnvelrels  39023  brssrid  39029  brcnvssrid  39034  dfdisjs5  39244  eldisjs5  39270  eldisjsim3  39384  mpets2  39402  pets  39413  prtlem12  39439  riotasv2d  39529  lkrscss  39670  islshpkrN  39692  isline  40311  ispointN  40314  0psubN  40321  linepsubN  40324  atpsubN  40325  cdlemk36  41485  diafn  41606  dibfna  41726  dibvalrel  41735  dicvalrelN  41757  diclspsn  41766  dihvalrel  41851  dih1  41858  lclkrlem1  42078  lclkr  42105  mapd1o  42220  mapdin  42234  hdmapfnN  42401  hgmapfnN  42460  lcmineqlem10  42603  sticksstones9  42719  sn-iotalem  42788  readvrec2  42918  readvrec  42919  repncan2  42939  elrfirn  43224  ismrcd1  43227  istopclsd  43229  rabren3dioph  43340  jm2.17b  43486  jm2.22  43520  jm2.23  43521  ttac  43561  pw2f1ocnv  43562  dnnumch1  43569  hbtlem5  43653  mncn0  43664  aaitgo  43687  rngunsnply  43694  unielss  43743  onexlimgt  43768  cantnfresb  43849  dflim5  43854  naddwordnexlem4  43926  safesnsupfiss  43939  safesnsupfidom1o  43941  safesnsupfilb  43942  ensucne0OLD  44054  clcnvlem  44147  relexp01min  44237  ntrf  44647  ssrecnpr  44832  seff  44833  sblpnf  44834  nzss  44841  dvconstbi  44858  ipo0  44972  ifr0  44973  addrfn  44995  subrfn  44996  mulvfn  44997  wfaxrep  45518  refsum2cnlem1  45565  rn1st  45796  ellimciota  46138  dvmptconst  46437  dvmptidg  46439  dvmulcncf  46447  dvdivcncf  46449  stoweidlem26  46548  stoweidlem50  46572  stoweidlem57  46579  aiotaval  47637  ndfatafv2nrn  47763  afv2ndefb  47766  funop1  47825  fun2dmnopgexmpl  47826  2ffzoeq  47870  2ltceilhalf  47874  m1modne  47896  iccpartiltu  47976  iccpartigtl  47977  zofldiv2ALTV  48232  evenprm2  48284  9fppr8  48307  stgoldbwt  48346  nnsum3primesle9  48364  nnsum4primeseven  48370  nnsum4primesevenALTV  48371  tgblthelfgott  48385  dfclnbgr6  48426  cycl3grtri  48517  grtrimap  48518  stgredgel  48527  stgr1  48531  isubgr3stgrlem2  48537  isubgr3stgrlem3  48538  usgrexmpl2trifr  48607  gpg5nbgrvtx13starlem1  48641  gpg5nbgrvtx13starlem2  48642  gpg5nbgrvtx13starlem3  48643  gpg5nbgr3star  48651  gpg3kgrtriex  48659  uspgrex  48720  0mgm  48736  nnsgrpmgm  48746  rngchomffvalALTV  48848  rhmsubcALTVlem1  48851  funcringcsetcALTV2lem4  48863  funcringcsetclem4ALTV  48886  srhmsubcALTV  48895  mapsnop  48914  zlmodzxzldeplem4  49073  zofldiv2  49101  fdivval  49109  nnlog2ge0lt1  49136  dig1  49178  itcoval2  49234  itcoval3  49235  mosn  49382  mo0  49383  mof02  49408  mofeu  49417  f102g  49421  f1mo  49422  tposres0  49446  f1omo  49462  f1omoOLD  49463  resipos  49544  intubeu  49553  unilbeu  49554  sectfn  49598  nelsubclem  49636  idfu1stf1o  49668  imaidfu  49679  oppfvallem  49704  funcoppc3  49716  idfth  49727  idsubc  49729  uptposlem  49766  swapf2fn  49837  swapf1f1o  49844  swapf2f1o  49845  swapf2f1oaALT  49847  fucof1  49891  fucofn2  49893  fucofn22  49909  reldmprcof1  49950  reldmprcof2  49951  fucoppcid  49977  fucoppc  49979  functhinclem1  50013  fullthinc  50019  thincciso  50022  indcthing  50029  indthinc  50031  indthincALT  50032  functermc  50077  discsntermlem  50139  reldmlan2  50186  reldmran2  50187  rellan  50192  relran  50193  termolmd  50239