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  1082  spei  2396  nfald2  2447  nfabd2  2920  raleleq  3310  raleleqOLD  3311  ceqsexv2d  3489  dedhb  3659  csbie2df  4394  ssdifeq0  4438  r19.2zb  4447  dedth  4535  pwidg  4571  snidg  4614  rexreusng  4633  exsnrex  4634  ifpr  4647  rmosn  4673  rabrsn  4678  prid1g  4714  tpid1g  4723  tpid2g  4725  tpid3g  4726  pwpw0  4766  sssn  4779  elpreqpr  4820  unimax  4897  intmin3  4928  eqbrtrdi  5134  al0ssb  5250  rabelpw  5278  intabs  5291  difelpw  5296  0inp0  5301  axpr  5369  intidg  5402  copsexgw  5435  copsexg  5436  euotd  5458  elopab  5472  elvvuni  5698  posn  5707  frsn  5709  eqrelriv  5735  relsnb  5748  relopabiALT  5770  opabid2  5775  ididg  5800  iss  5991  dfpo2  6251  ord0eln0  6370  sucidg  6397  nsuceq0  6399  funopg  6523  fn0  6620  f00  6713  f0bi  6714  f10d  6805  f1o00  6806  fo00  6807  brprcneu  6821  brprcneuALT  6822  dffn5  6889  fsn  7077  funop  7091  funsndifnop  7093  fnsnbOLD  7109  eufnfv  7172  f1ounsn  7215  f1eqcocnv  7244  nfriotadw  7320  nfriotad  7323  riotaprop  7339  oprabidw  7386  oprabid  7387  elrnmpo  7491  ov6g  7519  ovelrn  7531  caovmo  7592  offn  7632  caofinvl  7651  fr3nr  7714  onprc  7720  ordeleqon  7724  onint0  7733  0elsuc  7774  onuninsuci  7779  orduninsuc  7782  ordzsl  7784  onzsl  7785  tfinds  7799  limomss  7810  limom  7821  peano5  7832  xpexr  7857  eqop2  7973  opreuopreu  7975  1stconst  8039  2ndconst  8040  frxp2  8083  frxp3  8090  funsssuppss  8129  dftpos3  8183  dftpos4  8184  oawordeulem  8478  omwordi  8495  nnmwordi  8559  riiner  8723  ecopover  8754  map0g  8817  mapsnd  8819  elixpsn  8870  en0  8950  en0ALT  8951  en0r  8952  en1  8956  snfi  8975  fiprc  8976  sbthlem2  9011  sbthlem4  9013  sbthlem5  9014  0domg  9027  findcard  9083  findcard2  9084  nneneq  9125  sdom1  9144  1sdom2dom  9148  fineqvlem  9160  nfielex  9168  enp1i  9173  elfiun  9324  marypha1lem  9327  oicl  9425  oif  9426  oion  9432  hartogslem1  9438  hartogs  9440  wemapso2  9449  card2on  9450  0wdom  9466  brwdom2  9469  inf3lem6  9533  cantnflem3  9591  cantnflem4  9592  wemapwe  9597  cnfcom  9600  ssttrcl  9615  ttrclselem2  9626  tctr  9638  r1tr  9679  r1rankidb  9707  r1pw  9748  scottex  9788  scott0  9789  bnd2  9796  eldju2ndl  9827  tskwe  9853  oncard  9863  cardlim  9875  harsdom  9898  en2eleq  9909  dfac8alem  9930  cardaleph  9990  iunfictbso  10015  infmap2  10118  ackbij1lem18  10137  cff  10149  cfsuc  10158  cff1  10159  cflim2  10164  cfss  10166  sdom2en01  10203  infpssrlem4  10207  fin23lem7  10217  fin23lem11  10218  isfin2-2  10220  fin23lem26  10226  fin23lem19  10237  fin23lem17  10239  isf34lem2  10274  isf34lem4  10278  fin1a2lem6  10306  fin1a2lem10  10310  fin1a2lem12  10312  itunifn  10318  hsmexlem1  10327  axcc2lem  10337  dcomex  10348  axdc3lem4  10354  ondomon  10464  konigthlem  10469  pwcfsdom  10484  cfpwsdom  10485  axpowndlem3  10500  canth4  10548  canthnumlem  10549  canthwelem  10551  canthwe  10552  canthp1lem2  10554  pwfseqlem4  10563  pwfseqlem5  10564  gchaleph  10572  gch2  10576  winainflem  10594  0tsk  10656  rankcf  10678  tskcard  10682  gruina  10719  grutsk  10723  tskmid  10741  indpi  10808  nqereu  10830  mulcanenq  10861  recmulnq  10865  archnq  10881  ltsopr  10933  1ne0sr  10997  0idsr  10998  00sr  11000  leid  11219  lelttric  11230  divcan3  11812  divid  11817  div0  11819  lemul1a  11985  nn1suc  12157  nn0n0n1ge2b  12460  xnn0xr  12469  xnn0nemnf  12475  nn0lt10b  12545  nn0ind-raph  12583  elnn1uz2  12833  indstr2  12835  uzsupss  12848  rpnnen1lem4  12888  rpnnen1lem5  12889  xrnemnf  13026  xrnepnf  13027  mnfltxr  13036  xnn0n0n1ge2b  13041  xnn0ge0  13043  xrlttri  13048  xrlttr  13049  xrleid  13060  qbtwnxr  13109  xmullem2  13174  xlemul1a  13197  xrub  13221  reltxrnmnf  13252  ixxun  13271  xnn0xrge0  13416  fztpval  13496  fseq1p1m1  13508  elfznelfzob  13684  ltweuz  13878  fzfi  13889  fsuppmapnn0fiubex  13909  ser0f  13972  0exp  14014  faclbnd4lem1  14210  bcn1  14230  hashnemnf  14261  hashv01gt1  14262  hashsnle1  14334  hashgt12el2  14340  hashpw  14353  hashf1  14374  fz1isolem  14378  hash2prb  14389  hash3tpb  14412  0wrd0  14457  wrdlen1  14471  ccatvalfn  14498  eqs1  14530  wrdl1exs1  14531  swrdlen  14565  swrdwrdsymb  14580  swrdspsleq  14583  cats1un  14638  wrdind  14639  wrd2ind  14640  swrdccatin1  14642  repswsymballbi  14697  cshw1  14739  scshwfzeqfzo  14743  wrdl2exs2  14863  trclfvcotr  14926  relexp1g  14943  relexp0rel  14954  relexprelg  14955  relexpreld  14957  sqrt0  15158  sqrtsq  15186  mptfzshft  15695  prodf1f  15809  egt2lt3  16125  0dvds  16197  nn0onn  16301  nn0o  16304  divalgmod  16327  flodddiv4  16336  bitsp1o  16354  gcddvds  16424  bezout  16464  lcmdvds  16529  rpdvds  16581  1nprm  16600  prmind2  16606  dvdszzq  16642  nnoddn2prmb  16735  pcpre1  16764  vdwapf  16894  vdwapid1  16897  ram0  16944  ramz  16947  prmolefac  16968  cshws0  17023  prmlem0  17027  strle1  17079  restsspw  17345  prdsdsfn  17379  imasdsfn  17428  imasaddfnlem  17442  imasvscafn  17451  xpsfrnel  17476  isacs1i  17573  cidfn  17595  fnhomeqhomf  17607  comffn  17621  isoval  17682  sscres  17740  cofucl  17805  idffth  17852  ressffth  17857  cat1lem  18013  catcoppccl  18034  estrchomfn  18051  funcestrcsetclem4  18059  funcestrcsetclem7  18062  equivestrcsetc  18068  funcsetcestrclem4  18074  funcsetcestrclem7  18077  1stfcl  18113  2ndfcl  18114  prfcl  18119  evlfcl  18138  curf1cl  18144  curfcl  18148  hofcl  18175  yonedainv  18197  pospo  18259  lubfun  18266  glbfun  18279  joindmss  18293  meetdmss  18307  ipopos  18452  acsficl2d  18468  dirref  18517  mgmidcl  18584  mgmlrid  18585  ielefmnd  18805  smndex1basss  18823  smndex1n0mnd  18830  cntzssv  19250  idresperm  19308  symgvalstruct  19319  pmtrfmvdn0  19384  symggen  19392  psgnunilem1  19415  psgnprfval  19443  slwpgp  19535  frgpmhm  19687  frgpuptinv  19693  frgpup3lem  19699  gsumzoppg  19866  gsumcom2  19897  c0snmhm  20391  srhmsubc  20605  rhmsubclem1  20610  rrgsupp  20626  abv0  20748  zrhrhm  21458  psgnodpmr  21537  frlmphllem  21727  ellspd  21749  psrvscafval  21895  psrridm  21910  ltbwe  21989  psrbag0  22007  psrbagsn  22008  subrgascl  22011  psdmul  22091  mattpostpos  22379  mavmul0  22477  mavmul0g  22478  mdet0f1o  22518  m1detdiag  22522  m2detleiblem5  22550  m2detleiblem6  22551  m2detleiblem3  22554  m2detleiblem4  22555  maducoeval2  22565  d1mat2pmat  22664  chpmat1dlem  22760  chpmat1d  22761  baspartn  22879  eltg3  22887  topnex  22921  fctop  22929  cctop  22931  discld  23014  mretopd  23017  neipeltop  23054  neitr  23105  restcls  23106  ordtbaslem  23113  ordtuni  23115  idcn  23182  cnrmi  23285  cmpsublem  23324  cmpsub  23325  tgcmp  23326  uncmp  23328  hauscmplem  23331  cmpfi  23333  bwth  23335  1stcrestlem  23377  disllycmp  23423  dis1stc  23424  refref  23438  kgeni  23462  1stckgenlem  23478  kqffn  23650  snfil  23789  filconn  23808  cfinfil  23818  ufileu  23844  filufint  23845  fixufil  23847  cfinufil  23853  ufilen  23855  fin1aufil  23857  fmf  23870  rnelfm  23878  flimclslem  23909  hauspwpwf1  23912  supnfcls  23945  flimfnfcls  23953  fclscmp  23955  alexsubALTlem2  23973  alexsubALTlem3  23974  alexsubALT  23976  ptcmplem1  23977  cnextrel  23988  tsmsfbas  24053  ustref  24144  trust  24154  restutop  24162  isusp  24186  xmet0  24267  imasdsf1olem  24298  blfvalps  24308  blfps  24331  blf  24332  restmetu  24495  dscmet  24497  isngp2  24522  nm0  24554  nrginvrcn  24617  nmoix  24654  qdensere  24694  iccconn  24756  iccpnfcnv  24879  xrhmeo  24881  lebnumlem3  24899  metsscmetcld  25252  bcthlem5  25265  csschl  25313  rrxmfval  25343  minveclem3b  25365  cniccbdd  25399  ovolicc2lem4  25458  iunmbl  25491  ioorinv  25514  ioorcl  25515  i1f1lem  25627  limcvallem  25809  ellimc2  25815  limccnp  25829  limccnp2  25830  limcco  25831  perfdvf  25841  recnprss  25842  fncpn  25872  dvcmulf  25885  c1lip1  25939  lhop2  25957  q1pcl  26099  r1pdeglt  26102  ply1remlem  26107  plyssc  26142  ulm0  26337  cxpeq0  26624  cxplea  26642  cxplogb  26733  asinlem  26815  isppw2  27062  muval2  27081  dchrfi  27203  dchrpt  27215  bposlem6  27237  lgsdir2lem2  27274  lgsqr  27299  gausslemma2dlem4  27317  2lgslem2  27343  2lgslem3  27352  2lgs  27355  2sqlem7  27372  2sqlem11  27377  chtppilim  27423  nosgnn0i  27608  nolesgn2ores  27621  nogesgn1ores  27623  nosepnelem  27628  nosepdmlem  27632  nosupbnd1lem3  27659  nosupbnd1lem5  27661  nosupbnd2lem1  27664  noinfbnd1lem3  27674  noinfbnd1lem5  27676  noinfbnd2lem1  27679  oldval  27805  made0  27828  lrrecpo  27894  pncan2s  28024  divscan3d  28184  abssor  28194  om2noseqfo  28238  noseqrdglem  28245  noseqrdgfn  28246  noseqrdg0  28247  onsfi  28293  nohalf  28357  expsne0  28369  pw2divscan3d  28374  tgldimor  28490  tgcgr4  28519  tglnfn  28535  tglnunirn  28536  mirne  28655  mircinv  28656  perpln1  28698  perpln2  28699  lmiisolem  28784  xmstrkgc  28874  axcgrtr  28904  axsegconlem9  28914  axlowdimlem5  28935  axlowdimlem17  28947  axlowdim1  28948  uhgr0e  29060  edglnl  29132  uhgr0edgfi  29229  issubgr2  29261  subgrprop2  29263  egrsubgr  29266  0grsubgr  29267  0uhgrsubgr  29268  uhgrsubgrself  29269  nbgr1vtx  29347  nbgrssovtx  29350  nb3grprlem1  29369  uvtx01vtx  29386  cplgr1vlem  29418  cplgr1v  29419  usgrexilem  29429  wlkcomp  29620  wlk1walk  29628  wlkp1lem5  29665  uhgrwkspthlem1  29742  pthdlem1  29755  clwlkcomp  29768  lfgrn1cycl  29794  uspgrn2crct  29797  wwlksn0s  29850  usgrwwlks2on  29947  umgrwwlks2on  29948  clwwlkn  30017  clwwlkn1  30032  0ewlk  30105  1ewlk  30106  0spth  30117  upgr1wlkdlem2  30137  wlk2v2e  30148  upgr3v3e3cycl  30171  upgr4cycl4dv4e  30176  eupth0  30205  frgr0v  30253  frgr1v  30262  1vwmgr  30267  ex-opab  30423  grpoinvf  30523  nvmid  30650  nmlnoubi  30787  hiidrcl  31086  hsn0elch  31239  shjshseli  31484  cmbr4i  31592  dfiop2  31744  kbpj  31947  nmopun  32005  adjeq0  32082  kbass2  32108  pjssdif1i  32166  pjinvari  32182  pjcmul2i  32193  pj3i  32199  stge1i  32229  stle0i  32230  sumdmdlem2  32410  dmdbr6ati  32414  dmdbr7ati  32415  rabsnel  32491  unidifsnel  32526  unidifsnne  32527  disjdifprg  32566  ofoprabco  32657  padct  32712  fpwrelmapffslem  32726  xrlelttric  32746  xnn0gt0  32763  iundisj2cnt  32792  f1ocnt  32793  fz1nnct  32794  fz1nntr  32795  hashxpe  32800  nn0min  32814  sgnmulsgn  32836  sgnmulsgp  32837  wrdt2ind  32945  xrge0tsmsbi  33054  opprabs  33458  rtelextdg2lem  33750  2sqr3minply  33804  locfinref  33865  dispcmp  33883  zartopn  33899  zarcmplem  33905  pstmxmet  33921  xrge0iifcnv  33957  xrge0iif1  33962  qqhre  34044  esumcl  34054  esumpr2  34091  esumpinfval  34097  esumpcvgval  34102  ofcfn  34124  pwsiga  34154  prsiga  34155  sigainb  34160  ldgenpisyslem1  34187  measiuns  34241  relfae  34271  pmeasmono  34348  sitgf  34371  eulerpartgbij  34396  signswch  34585  signslema  34586  signstlen  34591  signstfvn  34593  circlevma  34666  bnj216  34755  bnj151  34900  bnj517  34908  bnj970  34970  bnj1145  35016  bnj1498  35084  r1omhfb  35134  r1omhfbregs  35144  fineqvrep  35148  fineqvac  35150  fineqvnttrclselem1  35152  fineqvnttrclselem2  35153  fineqvnttrclse  35155  wevgblacfn  35164  0nn0m1nnn0  35168  pthhashvtx  35183  acycgr0v  35203  prclisacycgr  35206  umgracycusgr  35209  cusgracyclt3v  35211  subfacp1lem5  35239  erdszelem8  35253  kur14lem1  35261  indispconn  35289  cvmsss2  35329  satfvsuclem2  35415  satfrel  35422  satfrnmapom  35425  satfv0fun  35426  satf00  35429  satf0suclem  35430  fmlasuc0  35439  msubrn  35584  dfon2lem7  35842  brbigcup  35951  elsingles  35971  fnimage  35982  funpartlem  35997  dfrdg4  36006  imagesset  36008  altopthsn  36016  elaltxp  36030  ellines  36207  linethru  36208  rankeq1o  36226  elhf2  36230  hfninf  36241  nn0prpwlem  36377  fneref  36405  neibastop2lem  36415  limsucncmpi  36500  bj-exlimmpbir  36969  curryset  37001  bj-snglex  37028  bj-restpw  37147  bj-inftyexpidisj  37265  topdifinffinlem  37402  relowlssretop  37418  rdgeqoa  37425  finxpreclem6  37451  fvineqsneq  37467  pibt2  37472  poimirlem23  37693  poimirlem29  37699  poimirlem31  37701  volsupnfl  37715  cnambfre  37718  dvasin  37754  dvacos  37755  sdclem2  37792  sstotbnd2  37824  ssbnd  37838  ismgmOLD  37900  grpokerinj  37943  rngomndo  37985  isdrngo1  38006  ac6s6  38222  iss2  38386  relecxrn  38441  sucmapsuc  38511  cosselrels  38597  cnvelrels  38598  brssrid  38604  brcnvssrid  38609  dfdisjs5  38820  eldisjs5  38834  mpets2  38949  pets  38960  prtlem12  38976  riotasv2d  39066  lkrscss  39207  islshpkrN  39229  isline  39848  ispointN  39851  0psubN  39858  linepsubN  39861  atpsubN  39862  cdlemk36  41022  diafn  41143  dibfna  41263  dibvalrel  41272  dicvalrelN  41294  diclspsn  41303  dihvalrel  41388  dih1  41395  lclkrlem1  41615  lclkr  41642  mapd1o  41757  mapdin  41771  hdmapfnN  41938  hgmapfnN  41997  lcmineqlem10  42141  sticksstones9  42257  sn-iotalem  42329  readvrec2  42469  readvrec  42470  repncan2  42490  elrfirn  42802  ismrcd1  42805  istopclsd  42807  rabren3dioph  42922  jm2.17b  43068  jm2.22  43102  jm2.23  43103  ttac  43143  pw2f1ocnv  43144  dnnumch1  43151  hbtlem5  43235  mncn0  43246  aaitgo  43269  rngunsnply  43276  unielss  43325  onexlimgt  43350  cantnfresb  43431  dflim5  43436  naddwordnexlem4  43508  safesnsupfiss  43522  safesnsupfidom1o  43524  safesnsupfilb  43525  ensucne0OLD  43637  clcnvlem  43730  relexp01min  43820  ntrf  44230  ssrecnpr  44415  seff  44416  sblpnf  44417  nzss  44424  dvconstbi  44441  ipo0  44555  ifr0  44556  addrfn  44578  subrfn  44579  mulvfn  44580  wfaxrep  45101  refsum2cnlem1  45148  rn1st  45384  ellimciota  45728  dvmptconst  46027  dvmptidg  46029  dvmulcncf  46037  dvdivcncf  46039  stoweidlem26  46138  stoweidlem50  46162  stoweidlem57  46169  aiotaval  47209  ndfatafv2nrn  47335  afv2ndefb  47338  funop1  47397  fun2dmnopgexmpl  47398  2ffzoeq  47441  2ltceilhalf  47442  m1modne  47462  iccpartiltu  47536  iccpartigtl  47537  zofldiv2ALTV  47776  evenprm2  47828  9fppr8  47851  stgoldbwt  47890  nnsum3primesle9  47908  nnsum4primeseven  47914  nnsum4primesevenALTV  47915  tgblthelfgott  47929  dfclnbgr6  47970  cycl3grtri  48061  grtrimap  48062  stgredgel  48071  stgr1  48075  isubgr3stgrlem2  48081  isubgr3stgrlem3  48082  usgrexmpl2trifr  48151  gpg5nbgrvtx13starlem1  48185  gpg5nbgrvtx13starlem2  48186  gpg5nbgrvtx13starlem3  48187  gpg5nbgr3star  48195  gpg3kgrtriex  48203  uspgrex  48264  0mgm  48280  nnsgrpmgm  48290  rngchomffvalALTV  48392  rhmsubcALTVlem1  48395  funcringcsetcALTV2lem4  48407  funcringcsetclem4ALTV  48430  srhmsubcALTV  48439  mapsnop  48458  zlmodzxzldeplem4  48618  zofldiv2  48646  fdivval  48654  nnlog2ge0lt1  48681  dig1  48723  itcoval2  48779  itcoval3  48780  mosn  48927  mo0  48928  mof02  48953  mofeu  48962  f102g  48966  f1mo  48967  tposres0  48991  f1omo  49007  f1omoOLD  49008  resipos  49089  intubeu  49098  unilbeu  49099  sectfn  49144  nelsubclem  49182  idfu1stf1o  49214  imaidfu  49225  oppfvallem  49250  funcoppc3  49262  idfth  49273  idsubc  49275  uptposlem  49312  swapf2fn  49383  swapf1f1o  49390  swapf2f1o  49391  swapf2f1oaALT  49393  fucof1  49437  fucofn2  49439  fucofn22  49455  reldmprcof1  49496  reldmprcof2  49497  fucoppcid  49523  fucoppc  49525  functhinclem1  49559  fullthinc  49565  thincciso  49568  indcthing  49575  indthinc  49577  indthincALT  49578  functermc  49623  discsntermlem  49685  reldmlan2  49732  reldmran2  49733  rellan  49738  relran  49739  termolmd  49785