Theorem mpbiri 261

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 260	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ 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:  elimh  1097  spei  2424  nfald2  2475  nfabd2  2946  raleleq  3333  ceqsexv2d  3502  dedhb  3665  csbie2df  4407  ssdifeq0  4446  dedth  4545  pwidgOLD  4582  snidg  4625  rexreusng  4644  exsnrex  4645  ifpr  4658  rmosn  4684  rabrsn  4689  prid1g  4725  tpid1g  4734  tpid2g  4736  tpid3g  4737  pwpw0  4778  sssn  4791  elpreqpr  4831  unimax  4909  intmin3  4940  eqbrtrdi  5149  al0ssb  5270  vneqv  5278  rabelpw  5306  intabs  5319  difelpw  5324  0inp0  5329  axpr  5398  intidg  5438  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  euotd  5496  elopab  5511  elvvuni  5738  posn  5747  frsn  5749  eqrelriv  5775  relsnb  5789  relopabiALT  5810  opabid2  5815  ididg  5839  iss  6037  dfpo2  6297  ord0eln0  6417  sucidg  6444  nsuceq0  6446  funopg  6570  fn0  6666  f00  6760  f0bi  6761  f10d  6855  f1o00  6856  fo00  6857  brprcneu  6871  brprcneuALT  6872  dffn5  6939  fsn  7131  funop  7146  funsndifnop  7148  fnsnbOLD  7164  eufnfv  7227  f1ounsn  7270  f1eqcocnv  7299  nfriotadw  7375  nfriotad  7378  riotaprop  7394  oprabidw  7441  oprabid  7442  elrnmpo  7546  ov6g  7574  ovelrn  7586  caovmo  7647  offn  7687  caofinvl  7706  fr3nr  7770  onprc  7776  ordeleqon  7780  onint0  7789  0elsuc  7830  onuninsuci  7835  orduninsuc  7838  ordzsl  7840  onzsl  7841  tfinds  7855  limomss  7866  limom  7877  peano5  7889  xpexr  7914  eqop2  8028  opreuopreu  8030  1stconst  8094  2ndconst  8095  frxp2  8139  frxp3  8146  funsssuppss  8185  dftpos3  8239  dftpos4  8240  oawordeulem  8538  omwordi  8555  nnmwordi  8620  riiner  8787  ecopover  8818  map0g  8881  mapsnd  8883  elixpsn  8934  en0  9014  en0ALT  9015  en0r  9016  en1  9020  snfi  9039  fiprc  9040  sbthlem2  9075  sbthlem4  9077  sbthlem5  9078  0domg  9091  findcard  9147  findcard2  9148  nneneq  9189  sdom1  9209  1sdom2dom  9213  fineqvlem  9225  nfielex  9233  enp1i  9238  elfiun  9389  marypha1lem  9392  oicl  9490  oif  9491  oion  9497  hartogslem1  9503  hartogs  9505  wemapso2  9514  card2on  9515  0wdom  9531  brwdom2  9534  elirrv  9558  inf3lem6  9601  cantnflem3  9659  cantnflem4  9660  wemapwe  9665  cnfcom  9668  ssttrcl  9683  ttrclselem2  9694  tctr  9706  r1tr  9747  r1rankidb  9775  r1pw  9816  scottex  9858  scott0  9859  bnd2  9878  eldju2ndl  9909  tskwe  9935  oncard  9945  cardlim  9957  harsdom  9980  en2eleq  9991  dfac8alem  10012  cardaleph  10072  iunfictbso  10097  infmap2  10199  ackbij1lem18  10218  cff  10230  cfsuc  10240  cff1  10241  cflim2  10246  cfss  10248  sdom2en01  10285  infpssrlem4  10289  fin23lem7  10299  fin23lem11  10300  isfin2-2  10302  fin23lem26  10308  fin23lem19  10319  fin23lem17  10321  isf34lem2  10356  isf34lem4  10360  fin1a2lem6  10388  fin1a2lem10  10392  fin1a2lem12  10394  itunifn  10400  hsmexlem1  10409  axcc2lem  10419  dcomex  10430  axdc3lem4  10436  ondomon  10546  konigthlem  10552  pwcfsdom  10567  cfpwsdom  10568  axpowndlem3  10583  canth4  10631  canthnumlem  10632  canthwelem  10634  canthwe  10635  canthp1lem2  10637  pwfseqlem4  10646  pwfseqlem5  10647  gchaleph  10655  gch2  10659  winainflem  10677  0tsk  10739  rankcf  10761  tskcard  10765  gruina  10802  grutsk  10806  tskmid  10824  indpi  10891  nqereu  10913  mulcanenq  10944  recmulnq  10948  archnq  10964  ltsopr  11016  1ne0sr  11080  0idsr  11081  00sr  11083  leid  11305  lelttric  11316  divcan3  11897  divid  11901  div0  11902  lemul1a  12068  nn1suc  12254  nn0n0n1ge2b  12572  xnn0xr  12581  xnn0nemnf  12587  nn0lt10b  12657  nn0ind-raph  12695  elnn1uz2  12948  indstr2  12950  uzsupss  12963  rpnnen1lem4  13003  rpnnen1lem5  13004  xrnemnf  13141  xrnepnf  13142  mnfltxr  13151  xnn0n0n1ge2b  13156  xnn0ge0  13158  xrlttri  13163  xrlttr  13164  xrleid  13175  qbtwnxr  13225  xmullem2  13290  xlemul1a  13313  xrub  13337  reltxrnmnf  13368  ixxun  13387  xnn0xrge0  13532  fztpval  13614  fseq1p1m1  13626  elfznelfzob  13803  ltweuz  13997  fzfi  14008  fsuppmapnn0fiubex  14028  ser0f  14091  0exp  14133  faclbnd4lem1  14329  bcn1  14349  hashnemnf  14380  hashv01gt1  14381  hashsnle1  14454  hashgt12el2  14460  hashpw  14473  hashf1  14494  fz1isolem  14498  hash2prb  14509  hash3tpb  14532  0wrd0  14577  wrdlen1  14591  ccatvalfn  14618  eqs1  14650  wrdl1exs1  14651  swrdlen  14685  swrdwrdsymb  14700  swrdspsleq  14703  cats1un  14758  wrdind  14759  wrd2ind  14760  swrdccatin1  14762  repswsymballbi  14817  cshw1  14859  scshwfzeqfzo  14863  wrdl2exs2  14983  trclfvcotr  15046  relexp1g  15063  relexp0rel  15074  relexprelg  15075  relexpreld  15077  sgnmulsgn  15146  sqrt0  15292  sqrtsq  15320  mptfzshft  15829  prodf1f  15946  egt2lt3  16261  0dvds  16333  nn0onn  16437  nn0o  16440  divalgmod  16463  flodddiv4  16472  bitsp1o  16490  gcddvds  16560  bezout  16600  lcmdvds  16665  rpdvds  16717  1nprm  16736  prmind2  16742  dvdszzq  16779  nnoddn2prmb  16872  pcpre1  16901  vdwapf  17031  vdwapid1  17034  ram0  17081  ramz  17084  prmolefac  17105  cshws0  17160  prmlem0  17164  strle1  17217  restsspw  17483  prdsdsfn  17517  imasdsfn  17567  imasaddfnlem  17581  imasvscafn  17590  xpsfrnel  17615  isacs1i  17712  cidfn  17734  fnhomeqhomf  17746  comffn  17760  isoval  17821  sscres  17879  cofucl  17944  idffth  17991  ressffth  17996  cat1lem  18152  catcoppccl  18173  estrchomfn  18190  funcestrcsetclem4  18198  funcestrcsetclem7  18201  equivestrcsetc  18207  funcsetcestrclem4  18213  funcsetcestrclem7  18216  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18277  curf1cl  18283  curfcl  18287  hofcl  18314  yonedainv  18336  pospo  18398  lubfun  18405  glbfun  18418  joindmss  18432  meetdmss  18446  ipopos  18591  acsficl2d  18607  dirref  18656  mgmidcl  18723  mgmlrid  18724  ielefmnd  18945  smndex1basss  18966  smndex1n0mnd  18973  cntzssv  19397  idresperm  19455  symgvalstruct  19466  pmtrfmvdn0  19531  symggen  19539  psgnunilem1  19562  psgnprfval  19590  slwpgp  19682  frgpmhm  19834  frgpuptinv  19840  frgpup3lem  19846  gsumzoppg  20013  gsumcom2  20044  c0snmhm  20544  srhmsubc  20764  rhmsubclem1  20769  rrgsupp  20785  abv0  20905  zrhrhm  21640  psgnodpmr  21719  frlmphllem  21909  ellspd  21931  psrvscafval  22077  psrridm  22091  ltbwe  22174  psrbag0  22192  psrbagsn  22193  subrgascl  22196  psdmul  22308  mattpostpos  22590  mavmul0  22688  mavmul0g  22689  mdet0f1o  22729  m1detdiag  22733  m2detleiblem5  22761  m2detleiblem6  22762  m2detleiblem3  22765  m2detleiblem4  22766  maducoeval2  22776  d1mat2pmat  22875  chpmat1dlem  22971  chpmat1d  22972  baspartn  23090  eltg3  23098  topnex  23132  fctop  23140  cctop  23142  discld  23225  mretopd  23228  neipeltop  23265  neitr  23316  restcls  23317  ordtbaslem  23324  ordtuni  23326  idcn  23393  cnrmi  23496  cmpsublem  23535  cmpsub  23536  tgcmp  23537  uncmp  23539  hauscmplem  23542  cmpfi  23544  bwth  23546  1stcrestlem  23588  disllycmp  23634  dis1stc  23635  refref  23649  kgeni  23673  1stckgenlem  23689  kqffn  23861  snfil  24000  filconn  24019  cfinfil  24029  ufileu  24055  filufint  24056  fixufil  24058  cfinufil  24064  ufilen  24066  fin1aufil  24068  fmf  24081  rnelfm  24089  flimclslem  24120  hauspwpwf1  24123  supnfcls  24156  flimfnfcls  24164  fclscmp  24166  alexsubALTlem2  24184  alexsubALTlem3  24185  alexsubALT  24187  ptcmplem1  24188  cnextrel  24199  tsmsfbas  24264  ustref  24355  trust  24365  restutop  24373  isusp  24397  xmet0  24478  imasdsf1olem  24509  blfvalps  24519  blfps  24542  blf  24543  restmetu  24706  dscmet  24708  isngp2  24733  nm0  24765  nrginvrcn  24828  nmoix  24865  qdensere  24905  iccconn  24967  iccpnfcnv  25082  xrhmeo  25084  lebnumlem3  25101  metsscmetcld  25453  bcthlem5  25466  csschl  25514  rrxmfval  25544  minveclem3b  25566  cniccbdd  25599  ovolicc2lem4  25658  iunmbl  25691  ioorinv  25714  ioorcl  25715  i1f1lem  25827  limcvallem  26009  ellimc2  26015  limccnp  26029  limccnp2  26030  limcco  26031  perfdvf  26041  recnprss  26042  fncpn  26071  dvcmulf  26083  c1lip1  26135  lhop2  26153  q1pcl  26293  r1pdeglt  26296  ply1remlem  26301  plyssc  26336  ulm0  26530  cxpeq0  26819  cxplea  26837  cxplogb  26927  asinlem  27009  isppw2  27255  muval2  27274  dchrfi  27395  dchrpt  27407  bposlem6  27429  lgsdir2lem2  27466  lgsqr  27491  gausslemma2dlem4  27509  2lgslem2  27535  2lgslem3  27544  2lgs  27547  2sqlem7  27564  2sqlem11  27569  chtppilim  27615  nosgnn0i  27799  nolesgn2ores  27812  nogesgn1ores  27814  nosepnelem  27819  nosepdmlem  27823  nosupbnd1lem3  27850  nosupbnd1lem5  27852  nosupbnd2lem1  27855  noinfbnd1lem3  27865  noinfbnd1lem5  27867  noinfbnd2lem1  27870  oldval  28003  made0  28032  lrrecpo  28110  pncan2s  28243  divscan3d  28405  abssor  28415  om2noseqfo  28467  noseqrdglem  28474  noseqrdgfn  28475  noseqrdg0  28476  onsfi  28525  nohalf  28593  expsne0  28605  pw2divscan3d  28610  tgldimor  28747  tgcgr4  28776  tglnfn  28792  tglnunirn  28793  mirne  28920  mircinv  28921  perpln1  28965  perpln2  28966  tgplnfn  29031  lmiisolem  29079  prlngmid2  29183  xmstrkgc  29201  axcgrtr  29231  axsegconlem9  29241  axlowdimlem5  29262  axlowdimlem17  29274  axlowdim1  29275  uhgr0e  29387  edglnl  29459  uhgr0edgfi  29556  issubgr2  29588  subgrprop2  29590  egrsubgr  29593  0grsubgr  29594  0uhgrsubgr  29595  uhgrsubgrself  29596  nbgr1vtx  29674  nbgrssovtx  29677  nb3grprlem1  29696  uvtx01vtx  29713  cplgr1vlem  29745  cplgr1v  29746  usgrexilem  29756  wlkcomp  29946  wlk1walk  29954  wlkp1lem5  29991  uhgrwkspthlem1  30068  pthdlem1  30081  clwlkcomp  30094  lfgrn1cycl  30120  uspgrn2crct  30123  wwlksn0s  30176  usgrwwlks2on  30273  umgrwwlks2on  30274  clwwlkn  30343  clwwlkn1  30358  0ewlk  30431  1ewlk  30432  0spth  30443  upgr1wlkdlem2  30463  wlk2v2e  30474  upgr3v3e3cycl  30497  upgr4cycl4dv4e  30502  eupth0  30531  frgr0v  30579  frgr1v  30588  1vwmgr  30593  ex-opab  30749  grpoinvf  30850  nvmid  30977  nmlnoubi  31114  hiidrcl  31413  hsn0elch  31566  shjshseli  31811  cmbr4i  31919  dfiop2  32071  kbpj  32274  nmopun  32332  adjeq0  32409  kbass2  32435  pjssdif1i  32493  pjinvari  32509  pjcmul2i  32520  pj3i  32526  stge1i  32556  stle0i  32557  sumdmdlem2  32737  dmdbr6ati  32741  dmdbr7ati  32742  rabsnel  32812  unidifsnel  32847  unidifsnne  32848  disjdifprg  32886  ofoprabco  32975  padct  33029  fpwrelmapffslem  33043  nn0mnfxrd  33062  xrlelttric  33063  xnn0gt0  33080  iundisj2cnt  33110  f1ocnt  33111  fz1nnct  33112  fz1nntr  33113  hashxpe  33118  nn0min  33131  sgnmulsgp  33142  wrdt2ind  33239  xrge0tsmsbi  33360  opprabs  33730  rtelextdg2lem  34082  2sqr3minply  34136  locfinref  34197  dispcmp  34215  zartopn  34231  zarcmplem  34237  pstmxmet  34253  xrge0iifcnv  34289  xrge0iif1  34294  qqhre  34376  esumcl  34386  esumpr2  34423  esumpinfval  34429  esumpcvgval  34434  ofcfn  34456  pwsiga  34486  prsiga  34487  sigainb  34492  ldgenpisyslem1  34519  measiuns  34573  relfae  34603  pmeasmono  34680  sitgf  34703  eulerpartgbij  34728  signswch  34914  signslema  34915  signstlen  34920  signstfvn  34922  circlevma  34995  bnj216  35087  bnj151  35231  bnj517  35239  bnj970  35301  bnj1145  35347  bnj1498  35415  r1omhfb  35474  rankscottu  35489  fineqvrep  35493  fineqvac  35495  fineqvnttrclselem1  35500  fineqvnttrclselem2  35501  fineqvnttrclse  35503  fineqvinfep  35504  r1omhfbregs  35516  kard0b  35538  rankkardu  35550  wevgblacfn  35561  vonf1osev  35562  0nn0m1nnn0  35570  pthhashvtx  35586  acycgr0v  35606  prclisacycgr  35609  umgracycusgr  35612  cusgracyclt3v  35614  subfacp1lem5  35642  erdszelem8  35656  kur14lem1  35664  indispconn  35692  cvmsss2  35732  satfvsuclem2  35818  satfrel  35825  satfrnmapom  35828  satfv0fun  35829  satf00  35832  satf0suclem  35833  fmlasuc0  35842  msubrn  35987  dfon2lem7  36245  brbigcup  36354  elsingles  36374  fnimage  36385  funpartlem  36400  dfrdg4  36409  imagesset  36411  altopthsn  36419  elaltxp  36433  ellines  36610  linethru  36611  rankeq1o  36629  elhf2  36633  hfninf  36644  nn0prpwlem  36799  fneref  36827  neibastop2lem  36837  limsucncmpi  36922  tz9.1tco  36960  bj-exlimmpbir  37515  curryset  37548  bj-snglex  37575  bj-axnul  37675  bj-restpw  37700  bj-inftyexpidisj  37820  topdifinffinlem  37959  relowlssretop  37975  rdgeqoa  37982  finxpreclem6  38008  fvineqsneq  38024  pibt2  38029  poimirlem23  38260  poimirlem29  38266  poimirlem31  38268  volsupnfl  38282  cnambfre  38285  dvasin  38321  dvacos  38322  sdclem2  38359  sstotbnd2  38391  ssbnd  38405  ismgmOLD  38467  grpokerinj  38510  rngomndo  38552  isdrngo1  38573  ac6s6  38789  iss2  38961  relecxrn  39024  sucmapsuc  39106  cosselrels  39192  cnvelrels  39193  brssrid  39199  brcnvssrid  39204  dfdisjs5  39414  eldisjs5  39440  eldisjsim3  39554  mpets2  39572  pets  39583  prtlem12  39609  riotasv2d  39699  lkrscss  39840  islshpkrN  39862  isline  40481  ispointN  40484  0psubN  40491  linepsubN  40494  atpsubN  40495  cdlemk36  41655  diafn  41776  dibfna  41896  dibvalrel  41905  dicvalrelN  41927  diclspsn  41936  dihvalrel  42021  dih1  42028  lclkrlem1  42248  lclkr  42275  mapd1o  42390  mapdin  42404  hdmapfnN  42571  hgmapfnN  42630  lcmineqlem10  42773  sticksstones9  42889  sn-iotalem  42960  readvrec2  43090  readvrec  43091  repncan2  43111  elrfirn  43396  ismrcd1  43399  istopclsd  43401  rabren3dioph  43512  jm2.17b  43658  jm2.22  43692  jm2.23  43693  ttac  43733  pw2f1ocnv  43734  dnnumch1  43741  hbtlem5  43825  mncn0  43836  aaitgo  43859  rngunsnply  43866  unielss  43915  onexlimgt  43940  cantnfresb  44021  dflim5  44026  naddwordnexlem4  44098  safesnsupfiss  44111  safesnsupfidom1o  44113  safesnsupfilb  44114  ensucne0OLD  44226  clcnvlem  44319  relexp01min  44409  ntrf  44819  ssrecnpr  44988  seff  44989  sblpnf  44990  nzss  44997  dvconstbi  45014  ipo0  45128  ifr0  45129  addrfn  45150  subrfn  45151  mulvfn  45152  wfaxrep  45673  refsum2cnlem1  45727  rn1st  45958  ellimciota  46300  dvmptconst  46599  dvmptidg  46601  dvmulcncf  46609  dvdivcncf  46611  stoweidlem26  46710  stoweidlem50  46734  stoweidlem57  46741  aiotaval  47799  ndfatafv2nrn  47925  afv2ndefb  47928  funop1  47987  fun2dmnopgexmpl  47988  2ffzoeq  48032  2ltceilhalf  48036  m1modne  48058  iccpartiltu  48138  iccpartigtl  48139  zofldiv2ALTV  48394  evenprm2  48446  9fppr8  48469  stgoldbwt  48508  nnsum3primesle9  48526  nnsum4primeseven  48532  nnsum4primesevenALTV  48533  tgblthelfgott  48547  dfclnbgr6  48588  cycl3grtri  48679  grtrimap  48680  stgredgel  48689  stgr1  48693  isubgr3stgrlem2  48699  isubgr3stgrlem3  48700  usgrexmpl2trifr  48769  gpg5nbgrvtx13starlem1  48803  gpg5nbgrvtx13starlem2  48804  gpg5nbgrvtx13starlem3  48805  gpg5nbgr3star  48813  gpg3kgrtriex  48821  uspgrex  48882  0mgm  48898  nnsgrpmgm  48908  rngchomffvalALTV  49010  rhmsubcALTVlem1  49013  funcringcsetcALTV2lem4  49025  funcringcsetclem4ALTV  49048  srhmsubcALTV  49057  mapsnop  49091  zlmodzxzldeplem4  49250  zofldiv2  49278  fdivval  49286  nnlog2ge0lt1  49313  dig1  49355  itcoval2  49411  itcoval3  49412  mosn  49558  mo0  49559  mof02  49584  mofeu  49593  f102g  49597  f1mo  49598  tposres0  49622  f1omo  49638  f1omoOLD  49639  resipos  49720  intubeu  49729  unilbeu  49730  sectfn  49774  nelsubclem  49812  idfu1stf1o  49844  imaidfu  49855  oppfvallem  49880  funcoppc3  49892  idfth  49903  idsubc  49905  uptposlem  49942  swapf2fn  50013  swapf1f1o  50020  swapf2f1o  50021  swapf2f1oaALT  50023  fucof1  50067  fucofn2  50069  fucofn22  50085  reldmprcof1  50126  reldmprcof2  50127  fucoppcid  50153  fucoppc  50155  functhinclem1  50189  fullthinc  50195  thincciso  50198  indcthing  50205  indthinc  50207  indthincALT  50208  functermc  50253  discsntermlem  50315  reldmlan2  50362  reldmran2  50363  rellan  50368  relran  50369  termolmd  50415