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  1076  dedtOLD  1079  spei  2412  nfald2  2467  nfabd2  3002  nfabd2OLD  3003  raleleqALT  3428  dedhb  3695  sbceqal  3835  csbie2df  4392  ssdifeq0  4432  r19.2zb  4441  dedth  4523  pwidg  4561  elpr2  4591  snidg  4599  rexreusng  4617  exsnrex  4618  ifpr  4629  rmosn  4655  rabrsn  4660  prid1g  4696  tpid1g  4705  tpid2g  4707  tpid3g  4708  pwpw0  4746  sssn  4759  elpreqpr  4797  pwsnOLD  4831  unimax  4874  intmin3  4904  eqbrtrdi  5105  al0ssb  5212  intabs  5245  pwnss  5250  difelpw  5252  rabelpw  5253  0inp0  5259  copsexgw  5381  copsexg  5382  euotd  5403  elopab  5414  epelgOLD  5467  elvvuni  5628  posn  5637  frsn  5639  eqrelriv  5662  relsnb  5675  relopabiALT  5695  opabid2  5700  ididg  5724  iss  5903  ord0eln0  6245  sucidg  6269  nsuceq0  6271  onun2i  6306  funopg  6389  fn0  6479  f00  6561  f0bi  6562  f10d  6648  f1o00  6649  fo00  6650  brprcneu  6662  dffn5  6724  fsn  6897  funop  6911  funsndifnop  6913  fnsnb  6928  eufnfv  6991  f1eqcocnv  7057  nfriotadw  7122  nfriotad  7125  riotaprop  7141  oprabidw  7187  oprabid  7188  elrnmpo  7287  ov6g  7312  ovelrn  7324  caovmo  7385  offn  7420  caofinvl  7436  fr3nr  7494  onprc  7499  ordeleqon  7503  onint0  7511  0elsuc  7550  onuninsuci  7555  orduninsuc  7558  ordzsl  7560  onzsl  7561  tfinds  7574  limomss  7585  limom  7595  peano5  7605  xpexr  7623  eqop2  7732  opreuopreu  7734  1stconst  7795  2ndconst  7796  funsssuppss  7856  dftpos3  7910  dftpos4  7911  wfrlem4  7958  wfrlem14  7968  oawordeulem  8180  omwordi  8197  nnmwordi  8261  riiner  8370  ecopover  8401  map0g  8448  mapsnd  8450  elixpsn  8501  en0  8572  en1  8576  fiprc  8595  sbthlem2  8628  sbthlem4  8630  sbthlem5  8631  nneneq  8700  sdom1  8718  fineqvlem  8732  nfielex  8747  findcard  8757  findcard2  8758  elfiun  8894  marypha1lem  8897  oicl  8993  oif  8994  oion  9000  hartogslem1  9006  hartogs  9008  wemapso2  9017  card2on  9018  0wdom  9034  brwdom2  9037  inf3lem6  9096  cantnflem3  9154  cantnflem4  9155  wemapwe  9160  cnfcom  9163  tctr  9182  r1tr  9205  r1rankidb  9233  r1pw  9274  scottex  9314  scott0  9315  bnd2  9322  eldju2ndl  9353  tskwe  9379  oncard  9389  cardlim  9401  harsdom  9424  en2eleq  9434  dfac8alem  9455  cardaleph  9515  iunfictbso  9540  infmap2  9640  ackbij1lem18  9659  cff  9670  cfsuc  9679  cff1  9680  cflim2  9685  cfss  9687  sdom2en01  9724  infpssrlem4  9728  fin23lem7  9738  fin23lem11  9739  isfin2-2  9741  fin23lem26  9747  fin23lem19  9758  fin23lem17  9760  isf34lem2  9795  isf34lem4  9799  fin1a2lem6  9827  fin1a2lem10  9831  fin1a2lem12  9833  itunifn  9839  hsmexlem1  9848  axcc2lem  9858  dcomex  9869  axdc3lem4  9875  ondomon  9985  konigthlem  9990  pwcfsdom  10005  cfpwsdom  10006  axpowndlem3  10021  canth4  10069  canthnumlem  10070  canthwelem  10072  canthwe  10073  canthp1lem2  10075  pwfseqlem4  10084  pwfseqlem5  10085  gchaleph  10093  gch2  10097  winainflem  10115  0tsk  10177  rankcf  10199  tskcard  10203  gruina  10240  grutsk  10244  tskmid  10262  indpi  10329  nqereu  10351  mulcanenq  10382  recmulnq  10386  archnq  10402  ltsopr  10454  1ne0sr  10518  0idsr  10519  00sr  10521  leid  10736  lelttric  10747  divcan3  11324  lemul1a  11494  nn1suc  11660  nn0n0n1ge2b  11964  xnn0xr  11973  xnn0nemnf  11979  nn0lt10b  12045  nn0ind-raph  12083  elnn1uz2  12326  indstr2  12328  uzsupss  12341  rpnnen1lem4  12380  rpnnen1lem5  12381  xrnemnf  12513  xrnepnf  12514  mnfltxr  12523  xnn0n0n1ge2b  12527  xnn0ge0  12529  xrlttri  12533  xrlttr  12534  xrleid  12545  qbtwnxr  12594  xmullem2  12659  xlemul1a  12682  xrub  12706  reltxrnmnf  12736  ixxun  12755  xnn0xrge0  12892  fztpval  12970  fseq1p1m1  12982  elfznelfzob  13144  ltweuz  13330  fzfi  13341  fsuppmapnn0fiubex  13361  ser0f  13424  0exp  13465  faclbnd4lem1  13654  bcn1  13674  hashnemnf  13705  hashv01gt1  13706  hashsnle1  13779  hashgt12el2  13785  hashpw  13798  hashf1  13816  fz1isolem  13820  hash2prb  13831  wrdlndmOLD  13880  0wrd0  13890  wrdlen1  13906  ccatvalfn  13935  eqs1  13966  wrdl1exs1  13967  swrdlen  14009  swrdwrdsymb  14024  swrdspsleq  14027  cats1un  14083  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  repswsymballbi  14142  cshw1  14184  scshwfzeqfzo  14188  wrdl2exs2  14308  trclfvcotr  14369  relexp1g  14385  relexp0rel  14396  relexprelg  14397  sqr0lem  14600  sqrtsq  14629  mptfzshft  15133  prodf1f  15248  fprodrev  15331  egt2lt3  15559  0dvds  15630  nn0onn  15731  nn0o  15734  divalgmod  15757  flodddiv4  15764  bitsp1o  15782  gcddvds  15852  bezout  15891  lcmdvds  15952  rpdvds  16004  1nprm  16023  prmind2  16029  nnoddn2prmb  16150  pcpre1  16179  vdwapf  16308  vdwapid1  16311  ram0  16358  ramz  16361  prmolefac  16382  cshws0  16435  prmlem0  16439  strle1  16592  restsspw  16705  prdsdsfn  16738  imasdsfn  16787  imasaddfnlem  16801  imasvscafn  16810  xpsfrnel  16835  isacs1i  16928  cidfn  16950  fnhomeqhomf  16961  comffn  16975  isoval  17035  sscres  17093  cofucl  17158  idffth  17203  ressffth  17208  catcoppccl  17368  estrchomfn  17385  funcestrcsetclem4  17393  funcestrcsetclem7  17396  equivestrcsetc  17402  funcsetcestrclem4  17408  funcsetcestrclem7  17411  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  yonedainv  17531  pospo  17583  lubfun  17590  glbfun  17603  joindmss  17617  meetdmss  17631  ipopos  17770  acsficl2d  17786  dirref  17845  mgmidcl  17876  mgmlrid  17877  ielefmnd  18052  smndex1basss  18070  smndex1n0mnd  18077  cntzssv  18458  idresperm  18514  symgvalstruct  18525  pmtrfmvdn0  18590  symggen  18598  psgnunilem1  18621  psgnprfval  18649  slwpgp  18738  frgpmhm  18891  frgpuptinv  18897  frgpup3lem  18903  gsumzoppg  19064  gsumcom2  19095  abv0  19602  rrgsupp  20064  psrvscafval  20170  psrridm  20184  ltbwe  20253  psrbag0  20274  psrbagsn  20275  subrgascl  20278  zrhrhm  20659  psgnodpmr  20734  frlmphllem  20924  frlmphl  20925  ellspd  20946  mattpostpos  21063  mavmul0  21161  mavmul0g  21162  mdet0f1o  21202  m1detdiag  21206  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  maducoeval2  21249  d1mat2pmat  21347  chpmat1dlem  21443  chpmat1d  21444  baspartn  21562  eltg3  21570  topnex  21604  fctop  21612  cctop  21614  discld  21697  mretopd  21700  neipeltop  21737  neitr  21788  restcls  21789  ordtbaslem  21796  ordtuni  21798  idcn  21865  cnrmi  21968  cmpsublem  22007  cmpsub  22008  tgcmp  22009  uncmp  22011  hauscmplem  22014  cmpfi  22016  bwth  22018  1stcrestlem  22060  disllycmp  22106  dis1stc  22107  refref  22121  kgeni  22145  1stckgenlem  22161  kqffn  22333  snfil  22472  filconn  22491  cfinfil  22501  ufileu  22527  filufint  22528  fixufil  22530  cfinufil  22536  ufilen  22538  fin1aufil  22540  fmf  22553  rnelfm  22561  flimclslem  22592  hauspwpwf1  22595  supnfcls  22628  flimfnfcls  22636  fclscmp  22638  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALT  22659  ptcmplem1  22660  cnextrel  22671  tsmsfbas  22736  ustref  22827  trust  22838  restutop  22846  isusp  22870  xmet0  22952  imasdsf1olem  22983  blfvalps  22993  blfps  23016  blf  23017  restmetu  23180  dscmet  23182  isngp2  23206  nm0  23238  nrginvrcn  23301  nmoix  23338  qdensere  23378  iccconn  23438  iccpnfcnv  23548  xrhmeo  23550  lebnumlem3  23567  metsscmetcld  23918  bcthlem5  23931  csschl  23979  rrxmfval  24009  minveclem3b  24031  cniccbdd  24062  ovolicc2lem4  24121  iunmbl  24154  ioorinv  24177  ioorcl  24178  i1f1lem  24290  limcvallem  24469  ellimc2  24475  limccnp  24489  limccnp2  24490  limcco  24491  perfdvf  24501  recnprss  24502  fncpn  24530  dvcmulf  24542  c1lip1  24594  lhop2  24612  q1pcl  24749  r1pdeglt  24752  ply1remlem  24756  plyssc  24790  ulm0  24979  cxpeq0  25261  cxplea  25279  cxplogb  25364  asinlem  25446  isppw2  25692  muval2  25711  dchrfi  25831  dchrpt  25843  bposlem6  25865  lgsdir2lem2  25902  lgsqr  25927  gausslemma2dlem4  25945  2lgslem2  25971  2lgslem3  25980  2lgs  25983  2sqlem7  26000  2sqlem11  26005  chtppilim  26051  tgldimor  26288  tgcgr4  26317  tglnfn  26333  tglnunirn  26334  mirne  26453  mircinv  26454  perpln1  26496  perpln2  26497  lmiisolem  26582  xmstrkgc  26672  axcgrtr  26701  axsegconlem9  26711  axlowdimlem5  26732  axlowdimlem17  26744  axlowdim1  26745  uhgr0e  26856  edglnl  26928  uhgr0edgfi  27022  issubgr2  27054  subgrprop2  27056  egrsubgr  27059  0grsubgr  27060  0uhgrsubgr  27061  uhgrsubgrself  27062  nbgr0vtx  27138  nbgr1vtx  27140  nbgrssovtx  27143  nb3grprlem1  27162  uvtx01vtx  27179  cplgr1vlem  27211  cplgr1v  27212  usgrexilem  27222  wlkcomp  27412  wlk1walk  27420  wlkp1lem5  27459  uhgrwkspthlem1  27534  pthdlem1  27547  clwlkcomp  27560  lfgrn1cycl  27583  uspgrn2crct  27586  wwlksn0s  27639  umgrwwlks2on  27736  clwwlkn  27804  clwwlkn1  27819  0ewlk  27893  1ewlk  27894  0spth  27905  upgr1wlkdlem2  27925  wlk2v2e  27936  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth0  27993  frgr0v  28041  frgr1v  28050  1vwmgr  28055  ex-opab  28211  grpoinvf  28309  nvmid  28436  nmlnoubi  28573  hiidrcl  28872  hsn0elch  29025  shjshseli  29270  cmbr4i  29378  dfiop2  29530  kbpj  29733  nmopun  29791  adjeq0  29868  kbass2  29894  pjssdif1i  29952  pjinvari  29968  pjcmul2i  29979  pj3i  29985  stge1i  30015  stle0i  30016  sumdmdlem2  30196  dmdbr6ati  30200  dmdbr7ati  30201  rabsnel  30263  unidifsnel  30295  unidifsnne  30296  disjdifprg  30325  ofoprabco  30409  padct  30455  fpwrelmapffslem  30468  xrlelttric  30476  xnn0gt0  30494  iundisj2cnt  30522  f1ocnt  30525  fz1nnct  30526  fz1nntr  30527  hashxpe  30529  dvdszzq  30531  nn0min  30536  wrdt2ind  30627  xrge0tsmsbi  30693  locfinref  31105  dispcmp  31123  pstmxmet  31137  xrge0iifcnv  31176  xrge0iif1  31181  qqhre  31261  esumcl  31289  esumpr2  31326  esumpinfval  31332  esumpcvgval  31337  ofcfn  31359  pwsiga  31389  prsiga  31390  sigainb  31395  ldgenpisyslem1  31422  measiuns  31476  relfae  31506  pmeasmono  31582  sitgf  31605  eulerpartgbij  31630  sgnmulsgn  31807  sgnmulsgp  31808  signswch  31831  signslema  31832  signstlen  31837  signstfvn  31839  circlevma  31913  bnj216  32002  bnj151  32149  bnj517  32157  bnj970  32219  bnj1145  32265  bnj1498  32333  0nn0m1nnn0  32351  pthhashvtx  32374  acycgr0v  32395  prclisacycgr  32398  umgracycusgr  32401  cusgracyclt3v  32403  subfacp1lem5  32431  erdszelem8  32445  kur14lem1  32453  indispconn  32481  cvmsss2  32521  satfvsuclem2  32607  satfrel  32614  satfrnmapom  32617  satfv0fun  32618  satf00  32621  satf0suclem  32622  fmlasuc0  32631  msubrn  32776  dfpo2  32991  dfon2lem7  33034  nosgnn0i  33166  nolesgn2ores  33179  nosepnelem  33184  nosepdmlem  33187  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  brbigcup  33359  elsingles  33379  fnimage  33390  funpartlem  33403  dfrdg4  33412  imagesset  33414  altopthsn  33422  elaltxp  33436  ellines  33613  linethru  33614  rankeq1o  33632  elhf2  33636  hfninf  33647  nn0prpwlem  33670  fneref  33698  neibastop2lem  33708  limsucncmpi  33793  bj-exlimmpbir  34233  curryset  34260  bj-snglex  34288  bj-restpw  34386  bj-inftyexpidisj  34495  topdifinffinlem  34631  relowlssretop  34647  rdgeqoa  34654  finxpreclem6  34680  fvineqsneq  34696  pibt2  34701  poimirlem23  34930  poimirlem29  34936  poimirlem31  34938  volsupnfl  34952  cnambfre  34955  dvasin  34993  dvacos  34994  sdclem2  35032  sstotbnd2  35067  ssbnd  35081  ismgmOLD  35143  grpokerinj  35186  rngomndo  35228  isdrngo1  35249  ac6s6  35465  iss2  35616  cnvelrels  35750  cosselrels  35751  brssrid  35757  brcnvssrid  35762  dfdisjs5  35960  eldisjs5  35974  prtlem12  36018  riotasv2d  36108  lkrscss  36249  islshpkrN  36271  isline  36890  ispointN  36893  0psubN  36900  linepsubN  36903  atpsubN  36904  cdlemk36  38064  diafn  38185  dibfna  38305  dibvalrel  38314  dicvalrelN  38336  diclspsn  38345  dihvalrel  38430  dih1  38437  lclkrlem1  38657  lclkr  38684  mapd1o  38799  mapdin  38813  hdmapfnN  38980  hgmapfnN  39039  repncan2  39261  elrfirn  39341  ismrcd1  39344  istopclsd  39346  rabren3dioph  39461  jm2.17b  39607  jm2.22  39641  jm2.23  39642  ttac  39682  pw2f1ocnv  39683  dnnumch1  39693  hbtlem5  39777  mncn0  39788  aaitgo  39811  rngunsnply  39822  ensucne0OLD  39945  clcnvlem  40032  relexp01min  40107  ntrf  40522  ssrecnpr  40689  seff  40690  sblpnf  40691  nzss  40698  dvconstbi  40715  ipo0  40830  ifr0  40831  addrfn  40853  subrfn  40854  mulvfn  40855  refsum2cnlem1  41343  ellimciota  41944  dvmptconst  42248  dvmptidg  42250  dvmulcncf  42259  dvdivcncf  42261  stoweidlem26  42360  stoweidlem50  42384  stoweidlem57  42391  aiotaval  43342  ndfatafv2nrn  43469  afv2ndefb  43472  funop1  43531  fun2dmnopgexmpl  43532  2ffzoeq  43577  iccpartiltu  43631  iccpartigtl  43632  zofldiv2ALTV  43876  evenprm2  43928  9fppr8  43951  stgoldbwt  43990  nnsum3primesle9  44008  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  tgblthelfgott  44029  isomgreqve  44039  uspgrex  44074  0mgm  44090  nnsgrpmgm  44132  c0snmhm  44235  rngchomffvalALTV  44315  funcringcsetcALTV2lem4  44359  funcringcsetclem4ALTV  44382  srhmsubc  44396  rhmsubclem1  44406  srhmsubcALTV  44414  rhmsubcALTVlem1  44424  mapsnop  44442  zlmodzxzldeplem4  44607  zofldiv2  44640  fdivval  44648  nnlog2ge0lt1  44675  dig1  44717