Theorem mpbiri 258

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  elimh  1083  spei  2399  nfald2  2450  nfabd2  2923  raleleq  3308  raleleqOLD  3309  ceqsexv2d  3480  dedhb  3650  csbie2df  4384  ssdifeq0  4427  dedth  4526  pwidg  4562  snidg  4605  rexreusng  4624  exsnrex  4625  ifpr  4638  rmosn  4664  rabrsn  4669  prid1g  4705  tpid1g  4714  tpid2g  4716  tpid3g  4717  pwpw0  4757  sssn  4770  elpreqpr  4811  unimax  4888  intmin3  4919  eqbrtrdi  5125  al0ssb  5244  vneqv  5252  rabelpw  5278  intabs  5291  difelpw  5296  0inp0  5301  axpr  5370  intidg  5410  copsexgw  5444  copsexgwOLD  5445  copsexg  5446  euotd  5468  elopab  5482  elvvuni  5708  posn  5717  frsn  5719  eqrelriv  5745  relsnb  5758  relopabiALT  5779  opabid2  5784  ididg  5809  iss  6001  dfpo2  6261  ord0eln0  6380  sucidg  6407  nsuceq0  6409  funopg  6533  fn0  6630  f00  6723  f0bi  6724  f10d  6815  f1o00  6816  fo00  6817  brprcneu  6831  brprcneuALT  6832  dffn5  6899  fsn  7089  funop  7103  funsndifnop  7105  fnsnbOLD  7121  eufnfv  7184  f1ounsn  7227  f1eqcocnv  7256  nfriotadw  7332  nfriotad  7335  riotaprop  7351  oprabidw  7398  oprabid  7399  elrnmpo  7503  ov6g  7531  ovelrn  7543  caovmo  7604  offn  7644  caofinvl  7663  fr3nr  7726  onprc  7732  ordeleqon  7736  onint0  7745  0elsuc  7786  onuninsuci  7791  orduninsuc  7794  ordzsl  7796  onzsl  7797  tfinds  7811  limomss  7822  limom  7833  peano5  7844  xpexr  7869  eqop2  7985  opreuopreu  7987  1stconst  8050  2ndconst  8051  frxp2  8094  frxp3  8101  funsssuppss  8140  dftpos3  8194  dftpos4  8195  oawordeulem  8489  omwordi  8506  nnmwordi  8571  riiner  8737  ecopover  8768  map0g  8832  mapsnd  8834  elixpsn  8885  en0  8965  en0ALT  8966  en0r  8967  en1  8971  snfi  8990  fiprc  8991  sbthlem2  9026  sbthlem4  9028  sbthlem5  9029  0domg  9042  findcard  9098  findcard2  9099  nneneq  9140  sdom1  9160  1sdom2dom  9164  fineqvlem  9176  nfielex  9184  enp1i  9189  elfiun  9343  marypha1lem  9346  oicl  9444  oif  9445  oion  9451  hartogslem1  9457  hartogs  9459  wemapso2  9468  card2on  9469  0wdom  9485  brwdom2  9488  inf3lem6  9554  cantnflem3  9612  cantnflem4  9613  wemapwe  9618  cnfcom  9621  ssttrcl  9636  ttrclselem2  9647  tctr  9659  r1tr  9700  r1rankidb  9728  r1pw  9769  scottex  9809  scott0  9810  bnd2  9817  eldju2ndl  9848  tskwe  9874  oncard  9884  cardlim  9896  harsdom  9919  en2eleq  9930  dfac8alem  9951  cardaleph  10011  iunfictbso  10036  infmap2  10139  ackbij1lem18  10158  cff  10170  cfsuc  10179  cff1  10180  cflim2  10185  cfss  10187  sdom2en01  10224  infpssrlem4  10228  fin23lem7  10238  fin23lem11  10239  isfin2-2  10241  fin23lem26  10247  fin23lem19  10258  fin23lem17  10260  isf34lem2  10295  isf34lem4  10299  fin1a2lem6  10327  fin1a2lem10  10331  fin1a2lem12  10333  itunifn  10339  hsmexlem1  10348  axcc2lem  10358  dcomex  10369  axdc3lem4  10375  ondomon  10485  konigthlem  10491  pwcfsdom  10506  cfpwsdom  10507  axpowndlem3  10522  canth4  10570  canthnumlem  10571  canthwelem  10573  canthwe  10574  canthp1lem2  10576  pwfseqlem4  10585  pwfseqlem5  10586  gchaleph  10594  gch2  10598  winainflem  10616  0tsk  10678  rankcf  10700  tskcard  10704  gruina  10741  grutsk  10745  tskmid  10763  indpi  10830  nqereu  10852  mulcanenq  10883  recmulnq  10887  archnq  10903  ltsopr  10955  1ne0sr  11019  0idsr  11020  00sr  11022  leid  11242  lelttric  11253  divcan3  11835  divid  11840  div0  11842  lemul1a  12009  nn1suc  12196  nn0n0n1ge2b  12506  xnn0xr  12515  xnn0nemnf  12521  nn0lt10b  12591  nn0ind-raph  12629  elnn1uz2  12875  indstr2  12877  uzsupss  12890  rpnnen1lem4  12930  rpnnen1lem5  12931  xrnemnf  13068  xrnepnf  13069  mnfltxr  13078  xnn0n0n1ge2b  13083  xnn0ge0  13085  xrlttri  13090  xrlttr  13091  xrleid  13102  qbtwnxr  13152  xmullem2  13217  xlemul1a  13240  xrub  13264  reltxrnmnf  13295  ixxun  13314  xnn0xrge0  13459  fztpval  13540  fseq1p1m1  13552  elfznelfzob  13729  ltweuz  13923  fzfi  13934  fsuppmapnn0fiubex  13954  ser0f  14017  0exp  14059  faclbnd4lem1  14255  bcn1  14275  hashnemnf  14306  hashv01gt1  14307  hashsnle1  14379  hashgt12el2  14385  hashpw  14398  hashf1  14419  fz1isolem  14423  hash2prb  14434  hash3tpb  14457  0wrd0  14502  wrdlen1  14516  ccatvalfn  14543  eqs1  14575  wrdl1exs1  14576  swrdlen  14610  swrdwrdsymb  14625  swrdspsleq  14628  cats1un  14683  wrdind  14684  wrd2ind  14685  swrdccatin1  14687  repswsymballbi  14742  cshw1  14784  scshwfzeqfzo  14788  wrdl2exs2  14908  trclfvcotr  14971  relexp1g  14988  relexp0rel  14999  relexprelg  15000  relexpreld  15002  sqrt0  15203  sqrtsq  15231  mptfzshft  15740  prodf1f  15857  egt2lt3  16173  0dvds  16245  nn0onn  16349  nn0o  16352  divalgmod  16375  flodddiv4  16384  bitsp1o  16402  gcddvds  16472  bezout  16512  lcmdvds  16577  rpdvds  16629  1nprm  16648  prmind2  16654  dvdszzq  16691  nnoddn2prmb  16784  pcpre1  16813  vdwapf  16943  vdwapid1  16946  ram0  16993  ramz  16996  prmolefac  17017  cshws0  17072  prmlem0  17076  strle1  17128  restsspw  17394  prdsdsfn  17428  imasdsfn  17478  imasaddfnlem  17492  imasvscafn  17501  xpsfrnel  17526  isacs1i  17623  cidfn  17645  fnhomeqhomf  17657  comffn  17671  isoval  17732  sscres  17790  cofucl  17855  idffth  17902  ressffth  17907  cat1lem  18063  catcoppccl  18084  estrchomfn  18101  funcestrcsetclem4  18109  funcestrcsetclem7  18112  equivestrcsetc  18118  funcsetcestrclem4  18124  funcsetcestrclem7  18127  1stfcl  18163  2ndfcl  18164  prfcl  18169  evlfcl  18188  curf1cl  18194  curfcl  18198  hofcl  18225  yonedainv  18247  pospo  18309  lubfun  18316  glbfun  18329  joindmss  18343  meetdmss  18357  ipopos  18502  acsficl2d  18518  dirref  18567  mgmidcl  18634  mgmlrid  18635  ielefmnd  18855  smndex1basss  18876  smndex1n0mnd  18883  cntzssv  19303  idresperm  19361  symgvalstruct  19372  pmtrfmvdn0  19437  symggen  19445  psgnunilem1  19468  psgnprfval  19496  slwpgp  19588  frgpmhm  19740  frgpuptinv  19746  frgpup3lem  19752  gsumzoppg  19919  gsumcom2  19950  c0snmhm  20443  srhmsubc  20657  rhmsubclem1  20662  rrgsupp  20678  abv0  20800  zrhrhm  21491  psgnodpmr  21570  frlmphllem  21760  ellspd  21782  psrvscafval  21927  psrridm  21941  ltbwe  22022  psrbag0  22040  psrbagsn  22041  subrgascl  22044  psdmul  22132  mattpostpos  22419  mavmul0  22517  mavmul0g  22518  mdet0f1o  22558  m1detdiag  22562  m2detleiblem5  22590  m2detleiblem6  22591  m2detleiblem3  22594  m2detleiblem4  22595  maducoeval2  22605  d1mat2pmat  22704  chpmat1dlem  22800  chpmat1d  22801  baspartn  22919  eltg3  22927  topnex  22961  fctop  22969  cctop  22971  discld  23054  mretopd  23057  neipeltop  23094  neitr  23145  restcls  23146  ordtbaslem  23153  ordtuni  23155  idcn  23222  cnrmi  23325  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  hauscmplem  23371  cmpfi  23373  bwth  23375  1stcrestlem  23417  disllycmp  23463  dis1stc  23464  refref  23478  kgeni  23502  1stckgenlem  23518  kqffn  23690  snfil  23829  filconn  23848  cfinfil  23858  ufileu  23884  filufint  23885  fixufil  23887  cfinufil  23893  ufilen  23895  fin1aufil  23897  fmf  23910  rnelfm  23918  flimclslem  23949  hauspwpwf1  23952  supnfcls  23985  flimfnfcls  23993  fclscmp  23995  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem1  24017  cnextrel  24028  tsmsfbas  24093  ustref  24184  trust  24194  restutop  24202  isusp  24226  xmet0  24307  imasdsf1olem  24338  blfvalps  24348  blfps  24371  blf  24372  restmetu  24535  dscmet  24537  isngp2  24562  nm0  24594  nrginvrcn  24657  nmoix  24694  qdensere  24734  iccconn  24796  iccpnfcnv  24911  xrhmeo  24913  lebnumlem3  24930  metsscmetcld  25282  bcthlem5  25295  csschl  25343  rrxmfval  25373  minveclem3b  25395  cniccbdd  25428  ovolicc2lem4  25487  iunmbl  25520  ioorinv  25543  ioorcl  25544  i1f1lem  25656  limcvallem  25838  ellimc2  25844  limccnp  25858  limccnp2  25859  limcco  25860  perfdvf  25870  recnprss  25871  fncpn  25900  dvcmulf  25912  c1lip1  25964  lhop2  25982  q1pcl  26122  r1pdeglt  26125  ply1remlem  26130  plyssc  26165  ulm0  26356  cxpeq0  26642  cxplea  26660  cxplogb  26750  asinlem  26832  isppw2  27078  muval2  27097  dchrfi  27218  dchrpt  27230  bposlem6  27252  lgsdir2lem2  27289  lgsqr  27314  gausslemma2dlem4  27332  2lgslem2  27358  2lgslem3  27367  2lgs  27370  2sqlem7  27387  2sqlem11  27392  chtppilim  27438  nosgnn0i  27623  nolesgn2ores  27636  nogesgn1ores  27638  nosepnelem  27643  nosepdmlem  27647  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  oldval  27826  made0  27855  lrrecpo  27933  pncan2s  28066  divscan3d  28228  abssor  28238  om2noseqfo  28290  noseqrdglem  28297  noseqrdgfn  28298  noseqrdg0  28299  onsfi  28348  nohalf  28416  expsne0  28428  pw2divscan3d  28433  tgldimor  28570  tgcgr4  28599  tglnfn  28615  tglnunirn  28616  mirne  28735  mircinv  28736  perpln1  28778  perpln2  28779  lmiisolem  28864  xmstrkgc  28954  axcgrtr  28984  axsegconlem9  28994  axlowdimlem5  29015  axlowdimlem17  29027  axlowdim1  29028  uhgr0e  29140  edglnl  29212  uhgr0edgfi  29309  issubgr2  29341  subgrprop2  29343  egrsubgr  29346  0grsubgr  29347  0uhgrsubgr  29348  uhgrsubgrself  29349  nbgr1vtx  29427  nbgrssovtx  29430  nb3grprlem1  29449  uvtx01vtx  29466  cplgr1vlem  29498  cplgr1v  29499  usgrexilem  29509  wlkcomp  29699  wlk1walk  29707  wlkp1lem5  29744  uhgrwkspthlem1  29821  pthdlem1  29834  clwlkcomp  29847  lfgrn1cycl  29873  uspgrn2crct  29876  wwlksn0s  29929  usgrwwlks2on  30026  umgrwwlks2on  30027  clwwlkn  30096  clwwlkn1  30111  0ewlk  30184  1ewlk  30185  0spth  30196  upgr1wlkdlem2  30216  wlk2v2e  30227  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth0  30284  frgr0v  30332  frgr1v  30341  1vwmgr  30346  ex-opab  30502  grpoinvf  30603  nvmid  30730  nmlnoubi  30867  hiidrcl  31166  hsn0elch  31319  shjshseli  31564  cmbr4i  31672  dfiop2  31824  kbpj  32027  nmopun  32085  adjeq0  32162  kbass2  32188  pjssdif1i  32246  pjinvari  32262  pjcmul2i  32273  pj3i  32279  stge1i  32309  stle0i  32310  sumdmdlem2  32490  dmdbr6ati  32494  dmdbr7ati  32495  rabsnel  32570  unidifsnel  32605  unidifsnne  32606  disjdifprg  32645  ofoprabco  32737  padct  32791  fpwrelmapffslem  32805  nn0mnfxrd  32824  xrlelttric  32825  xnn0gt0  32842  iundisj2cnt  32872  f1ocnt  32873  fz1nnct  32874  fz1nntr  32875  hashxpe  32880  nn0min  32894  sgnmulsgn  32915  sgnmulsgp  32916  wrdt2ind  33013  xrge0tsmsbi  33135  opprabs  33542  rtelextdg2lem  33870  2sqr3minply  33924  locfinref  33985  dispcmp  34003  zartopn  34019  zarcmplem  34025  pstmxmet  34041  xrge0iifcnv  34077  xrge0iif1  34082  qqhre  34164  esumcl  34174  esumpr2  34211  esumpinfval  34217  esumpcvgval  34222  ofcfn  34244  pwsiga  34274  prsiga  34275  sigainb  34280  ldgenpisyslem1  34307  measiuns  34361  relfae  34391  pmeasmono  34468  sitgf  34491  eulerpartgbij  34516  signswch  34705  signslema  34706  signstlen  34711  signstfvn  34713  circlevma  34786  bnj216  34875  bnj151  35019  bnj517  35027  bnj970  35089  bnj1145  35135  bnj1498  35203  r1omhfb  35256  fineqvrep  35258  fineqvac  35260  fineqvnttrclselem1  35265  fineqvnttrclselem2  35266  fineqvnttrclse  35268  fineqvinfep  35269  r1omhfbregs  35281  wevgblacfn  35291  0nn0m1nnn0  35295  pthhashvtx  35310  acycgr0v  35330  prclisacycgr  35333  umgracycusgr  35336  cusgracyclt3v  35338  subfacp1lem5  35366  erdszelem8  35380  kur14lem1  35388  indispconn  35416  cvmsss2  35456  satfvsuclem2  35542  satfrel  35549  satfrnmapom  35552  satfv0fun  35553  satf00  35556  satf0suclem  35557  fmlasuc0  35566  msubrn  35711  dfon2lem7  35969  brbigcup  36078  elsingles  36098  fnimage  36109  funpartlem  36124  dfrdg4  36133  imagesset  36135  altopthsn  36143  elaltxp  36157  ellines  36334  linethru  36335  rankeq1o  36353  elhf2  36357  hfninf  36368  nn0prpwlem  36504  fneref  36532  neibastop2lem  36542  limsucncmpi  36627  tz9.1tco  36665  bj-exlimmpbir  37221  curryset  37253  bj-snglex  37280  bj-axnul  37379  bj-restpw  37404  bj-inftyexpidisj  37524  topdifinffinlem  37663  relowlssretop  37679  rdgeqoa  37686  finxpreclem6  37712  fvineqsneq  37728  pibt2  37733  poimirlem23  37964  poimirlem29  37970  poimirlem31  37972  volsupnfl  37986  cnambfre  37989  dvasin  38025  dvacos  38026  sdclem2  38063  sstotbnd2  38095  ssbnd  38109  ismgmOLD  38171  grpokerinj  38214  rngomndo  38256  isdrngo1  38277  ac6s6  38493  iss2  38665  relecxrn  38728  sucmapsuc  38810  cosselrels  38896  cnvelrels  38897  brssrid  38903  brcnvssrid  38908  dfdisjs5  39118  eldisjs5  39144  eldisjsim3  39258  mpets2  39276  pets  39287  prtlem12  39313  riotasv2d  39403  lkrscss  39544  islshpkrN  39566  isline  40185  ispointN  40188  0psubN  40195  linepsubN  40198  atpsubN  40199  cdlemk36  41359  diafn  41480  dibfna  41600  dibvalrel  41609  dicvalrelN  41631  diclspsn  41640  dihvalrel  41725  dih1  41732  lclkrlem1  41952  lclkr  41979  mapd1o  42094  mapdin  42108  hdmapfnN  42275  hgmapfnN  42334  lcmineqlem10  42477  sticksstones9  42593  sn-iotalem  42662  readvrec2  42793  readvrec  42794  repncan2  42814  elrfirn  43127  ismrcd1  43130  istopclsd  43132  rabren3dioph  43243  jm2.17b  43389  jm2.22  43423  jm2.23  43424  ttac  43464  pw2f1ocnv  43465  dnnumch1  43472  hbtlem5  43556  mncn0  43567  aaitgo  43590  rngunsnply  43597  unielss  43646  onexlimgt  43671  cantnfresb  43752  dflim5  43757  naddwordnexlem4  43829  safesnsupfiss  43842  safesnsupfidom1o  43844  safesnsupfilb  43845  ensucne0OLD  43957  clcnvlem  44050  relexp01min  44140  ntrf  44550  ssrecnpr  44735  seff  44736  sblpnf  44737  nzss  44744  dvconstbi  44761  ipo0  44875  ifr0  44876  addrfn  44898  subrfn  44899  mulvfn  44900  wfaxrep  45421  refsum2cnlem1  45468  rn1st  45702  ellimciota  46044  dvmptconst  46343  dvmptidg  46345  dvmulcncf  46353  dvdivcncf  46355  stoweidlem26  46454  stoweidlem50  46478  stoweidlem57  46485  aiotaval  47537  ndfatafv2nrn  47663  afv2ndefb  47666  funop1  47725  fun2dmnopgexmpl  47726  2ffzoeq  47770  2ltceilhalf  47774  m1modne  47796  iccpartiltu  47876  iccpartigtl  47877  zofldiv2ALTV  48132  evenprm2  48184  9fppr8  48207  stgoldbwt  48246  nnsum3primesle9  48264  nnsum4primeseven  48270  nnsum4primesevenALTV  48271  tgblthelfgott  48285  dfclnbgr6  48326  cycl3grtri  48417  grtrimap  48418  stgredgel  48427  stgr1  48431  isubgr3stgrlem2  48437  isubgr3stgrlem3  48438  usgrexmpl2trifr  48507  gpg5nbgrvtx13starlem1  48541  gpg5nbgrvtx13starlem2  48542  gpg5nbgrvtx13starlem3  48543  gpg5nbgr3star  48551  gpg3kgrtriex  48559  uspgrex  48620  0mgm  48636  nnsgrpmgm  48646  rngchomffvalALTV  48748  rhmsubcALTVlem1  48751  funcringcsetcALTV2lem4  48763  funcringcsetclem4ALTV  48786  srhmsubcALTV  48795  mapsnop  48814  zlmodzxzldeplem4  48973  zofldiv2  49001  fdivval  49009  nnlog2ge0lt1  49036  dig1  49078  itcoval2  49134  itcoval3  49135  mosn  49282  mo0  49283  mof02  49308  mofeu  49317  f102g  49321  f1mo  49322  tposres0  49346  f1omo  49362  f1omoOLD  49363  resipos  49444  intubeu  49453  unilbeu  49454  sectfn  49498  nelsubclem  49536  idfu1stf1o  49568  imaidfu  49579  oppfvallem  49604  funcoppc3  49616  idfth  49627  idsubc  49629  uptposlem  49666  swapf2fn  49737  swapf1f1o  49744  swapf2f1o  49745  swapf2f1oaALT  49747  fucof1  49791  fucofn2  49793  fucofn22  49809  reldmprcof1  49850  reldmprcof2  49851  fucoppcid  49877  fucoppc  49879  functhinclem1  49913  fullthinc  49919  thincciso  49922  indcthing  49929  indthinc  49931  indthincALT  49932  functermc  49977  discsntermlem  50039  reldmlan2  50086  reldmran2  50087  rellan  50092  relran  50093  termolmd  50139