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  2926  raleleq  3339  raleleqOLD  3340  ceqsexv2d  3532  dedhb  3711  sbceqalOLD  3857  csbie2df  4448  ssdifeq0  4492  r19.2zb  4501  dedth  4588  pwidg  4624  snidg  4664  rexreusng  4683  exsnrex  4684  ifpr  4697  rmosn  4723  rabrsn  4728  prid1g  4764  tpid1g  4773  tpid2g  4775  tpid3g  4776  pwpw0  4817  sssn  4830  elpreqpr  4871  unimax  4948  intmin3  4980  eqbrtrdi  5186  al0ssb  5313  rabelpw  5341  intabs  5354  difelpw  5359  0inp0  5364  axpr  5432  intidg  5467  copsexgw  5500  copsexg  5501  euotd  5522  elopab  5536  elvvuni  5764  posn  5773  frsn  5775  eqrelriv  5801  relsnb  5814  relopabiALT  5835  opabid2  5840  ididg  5866  iss  6054  dfpo2  6317  ord0eln0  6440  sucidg  6466  nsuceq0  6468  funopg  6601  fn0  6699  f00  6790  f0bi  6791  f10d  6882  f1o00  6883  fo00  6884  brprcneu  6896  brprcneuALT  6897  dffn5  6966  fsn  7154  funop  7168  funsndifnop  7170  fnsnb  7185  eufnfv  7248  f1ounsn  7291  f1eqcocnv  7320  nfriotadw  7395  nfriotad  7398  riotaprop  7414  oprabidw  7461  oprabid  7462  elrnmpo  7568  ov6g  7596  ovelrn  7608  caovmo  7669  offn  7709  caofinvl  7728  fr3nr  7790  onprc  7796  ordeleqon  7800  onint0  7810  0elsuc  7854  onuninsuci  7860  orduninsuc  7863  ordzsl  7865  onzsl  7866  tfinds  7880  limomss  7891  limom  7902  peano5  7915  xpexr  7940  eqop2  8055  opreuopreu  8057  1stconst  8123  2ndconst  8124  frxp2  8167  frxp3  8174  funsssuppss  8213  dftpos3  8267  dftpos4  8268  wfrlem4OLD  8350  wfrlem14OLD  8360  oawordeulem  8590  omwordi  8607  nnmwordi  8671  riiner  8828  ecopover  8859  map0g  8922  mapsnd  8924  elixpsn  8975  en0  9056  en0ALT  9057  en0r  9058  en1  9062  snfi  9081  fiprc  9083  sbthlem2  9122  sbthlem4  9124  sbthlem5  9125  0domg  9138  findcard  9201  findcard2  9202  nneneq  9243  nneneqOLD  9255  sdom1  9275  sdom1OLD  9276  1sdom2dom  9280  fineqvlem  9295  nfielex  9304  enp1i  9310  elfiun  9467  marypha1lem  9470  oicl  9566  oif  9567  oion  9573  hartogslem1  9579  hartogs  9581  wemapso2  9590  card2on  9591  0wdom  9607  brwdom2  9610  inf3lem6  9670  cantnflem3  9728  cantnflem4  9729  wemapwe  9734  cnfcom  9737  ssttrcl  9752  ttrclselem2  9763  tctr  9777  r1tr  9813  r1rankidb  9841  r1pw  9882  scottex  9922  scott0  9923  bnd2  9930  eldju2ndl  9961  tskwe  9987  oncard  9997  cardlim  10009  harsdom  10032  en2eleq  10045  dfac8alem  10066  cardaleph  10126  iunfictbso  10151  infmap2  10254  ackbij1lem18  10273  cff  10285  cfsuc  10294  cff1  10295  cflim2  10300  cfss  10302  sdom2en01  10339  infpssrlem4  10343  fin23lem7  10353  fin23lem11  10354  isfin2-2  10356  fin23lem26  10362  fin23lem19  10373  fin23lem17  10375  isf34lem2  10410  isf34lem4  10414  fin1a2lem6  10442  fin1a2lem10  10446  fin1a2lem12  10448  itunifn  10454  hsmexlem1  10463  axcc2lem  10473  dcomex  10484  axdc3lem4  10490  ondomon  10600  konigthlem  10605  pwcfsdom  10620  cfpwsdom  10621  axpowndlem3  10636  canth4  10684  canthnumlem  10685  canthwelem  10687  canthwe  10688  canthp1lem2  10690  pwfseqlem4  10699  pwfseqlem5  10700  gchaleph  10708  gch2  10712  winainflem  10730  0tsk  10792  rankcf  10814  tskcard  10818  gruina  10855  grutsk  10859  tskmid  10877  indpi  10944  nqereu  10966  mulcanenq  10997  recmulnq  11001  archnq  11017  ltsopr  11069  1ne0sr  11133  0idsr  11134  00sr  11136  leid  11354  lelttric  11365  divcan3  11945  divid  11950  div0  11952  lemul1a  12118  nn1suc  12285  nn0n0n1ge2b  12592  xnn0xr  12601  xnn0nemnf  12607  nn0lt10b  12677  nn0ind-raph  12715  elnn1uz2  12964  indstr2  12966  uzsupss  12979  rpnnen1lem4  13019  rpnnen1lem5  13020  xrnemnf  13156  xrnepnf  13157  mnfltxr  13166  xnn0n0n1ge2b  13170  xnn0ge0  13172  xrlttri  13177  xrlttr  13178  xrleid  13189  qbtwnxr  13238  xmullem2  13303  xlemul1a  13326  xrub  13350  reltxrnmnf  13380  ixxun  13399  xnn0xrge0  13542  fztpval  13622  fseq1p1m1  13634  elfznelfzob  13808  ltweuz  13998  fzfi  14009  fsuppmapnn0fiubex  14029  ser0f  14092  0exp  14134  faclbnd4lem1  14328  bcn1  14348  hashnemnf  14379  hashv01gt1  14380  hashsnle1  14452  hashgt12el2  14458  hashpw  14471  hashf1  14492  fz1isolem  14496  hash2prb  14507  hash3tpb  14530  0wrd0  14574  wrdlen1  14588  ccatvalfn  14615  eqs1  14646  wrdl1exs1  14647  swrdlen  14681  swrdwrdsymb  14696  swrdspsleq  14699  cats1un  14755  wrdind  14756  wrd2ind  14757  swrdccatin1  14759  repswsymballbi  14814  cshw1  14856  scshwfzeqfzo  14861  wrdl2exs2  14981  trclfvcotr  15044  relexp1g  15061  relexp0rel  15072  relexprelg  15073  relexpreld  15075  sqrt0  15276  sqrtsq  15304  mptfzshft  15810  prodf1f  15924  egt2lt3  16238  0dvds  16310  nn0onn  16413  nn0o  16416  divalgmod  16439  flodddiv4  16448  bitsp1o  16466  gcddvds  16536  bezout  16576  lcmdvds  16641  rpdvds  16693  1nprm  16712  prmind2  16718  dvdszzq  16754  nnoddn2prmb  16846  pcpre1  16875  vdwapf  17005  vdwapid1  17008  ram0  17055  ramz  17058  prmolefac  17079  cshws0  17135  prmlem0  17139  strle1  17191  restsspw  17477  prdsdsfn  17511  imasdsfn  17560  imasaddfnlem  17574  imasvscafn  17583  xpsfrnel  17608  isacs1i  17701  cidfn  17723  fnhomeqhomf  17735  comffn  17749  isoval  17812  sscres  17870  cofucl  17938  idffth  17986  ressffth  17991  cat1lem  18149  catcoppccl  18170  catcoppcclOLD  18171  estrchomfn  18189  funcestrcsetclem4  18198  funcestrcsetclem7  18201  equivestrcsetc  18207  funcsetcestrclem4  18213  funcsetcestrclem7  18216  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  yonedainv  18337  pospo  18402  lubfun  18409  glbfun  18422  joindmss  18436  meetdmss  18450  ipopos  18593  acsficl2d  18609  dirref  18658  mgmidcl  18691  mgmlrid  18692  ielefmnd  18912  smndex1basss  18930  smndex1n0mnd  18937  cntzssv  19358  idresperm  19417  symgvalstruct  19428  symgvalstructOLD  19429  pmtrfmvdn0  19494  symggen  19502  psgnunilem1  19525  psgnprfval  19553  slwpgp  19645  frgpmhm  19797  frgpuptinv  19803  frgpup3lem  19809  gsumzoppg  19976  gsumcom2  20007  c0snmhm  20479  srhmsubc  20696  rhmsubclem1  20701  rrgsupp  20717  abv0  20840  zrhrhm  21539  psgnodpmr  21625  frlmphllem  21817  ellspd  21839  psrvscafval  21985  psrridm  22000  ltbwe  22079  psrbag0  22103  psrbagsn  22104  subrgascl  22107  psdmul  22187  mattpostpos  22475  mavmul0  22573  mavmul0g  22574  mdet0f1o  22614  m1detdiag  22618  m2detleiblem5  22646  m2detleiblem6  22647  m2detleiblem3  22650  m2detleiblem4  22651  maducoeval2  22661  d1mat2pmat  22760  chpmat1dlem  22856  chpmat1d  22857  baspartn  22976  eltg3  22984  topnex  23018  fctop  23026  cctop  23028  discld  23112  mretopd  23115  neipeltop  23152  neitr  23203  restcls  23204  ordtbaslem  23211  ordtuni  23213  idcn  23280  cnrmi  23383  cmpsublem  23422  cmpsub  23423  tgcmp  23424  uncmp  23426  hauscmplem  23429  cmpfi  23431  bwth  23433  1stcrestlem  23475  disllycmp  23521  dis1stc  23522  refref  23536  kgeni  23560  1stckgenlem  23576  kqffn  23748  snfil  23887  filconn  23906  cfinfil  23916  ufileu  23942  filufint  23943  fixufil  23945  cfinufil  23951  ufilen  23953  fin1aufil  23955  fmf  23968  rnelfm  23976  flimclslem  24007  hauspwpwf1  24010  supnfcls  24043  flimfnfcls  24051  fclscmp  24053  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem1  24075  cnextrel  24086  tsmsfbas  24151  ustref  24242  trust  24253  restutop  24261  isusp  24285  xmet0  24367  imasdsf1olem  24398  blfvalps  24408  blfps  24431  blf  24432  restmetu  24598  dscmet  24600  isngp2  24625  nm0  24657  nrginvrcn  24728  nmoix  24765  qdensere  24805  iccconn  24865  iccpnfcnv  24988  xrhmeo  24990  lebnumlem3  25008  metsscmetcld  25362  bcthlem5  25375  csschl  25423  rrxmfval  25453  minveclem3b  25475  cniccbdd  25509  ovolicc2lem4  25568  iunmbl  25601  ioorinv  25624  ioorcl  25625  i1f1lem  25737  limcvallem  25920  ellimc2  25926  limccnp  25940  limccnp2  25941  limcco  25942  perfdvf  25952  recnprss  25953  fncpn  25983  dvcmulf  25996  c1lip1  26050  lhop2  26068  q1pcl  26210  r1pdeglt  26213  ply1remlem  26218  plyssc  26253  ulm0  26448  cxpeq0  26734  cxplea  26752  cxplogb  26843  asinlem  26925  isppw2  27172  muval2  27191  dchrfi  27313  dchrpt  27325  bposlem6  27347  lgsdir2lem2  27384  lgsqr  27409  gausslemma2dlem4  27427  2lgslem2  27453  2lgslem3  27462  2lgs  27465  2sqlem7  27482  2sqlem11  27487  chtppilim  27533  nosgnn0i  27718  nolesgn2ores  27731  nogesgn1ores  27733  nosepnelem  27738  nosepdmlem  27742  nosupbnd1lem3  27769  nosupbnd1lem5  27771  nosupbnd2lem1  27774  noinfbnd1lem3  27784  noinfbnd1lem5  27786  noinfbnd2lem1  27789  oldval  27907  made0  27926  lrrecpo  27988  pncan2s  28118  divscan3d  28274  abssor  28284  om2noseqfo  28318  noseqrdglem  28325  noseqrdgfn  28326  noseqrdg0  28327  n0scut  28352  nohalf  28421  expsne0  28428  tgldimor  28524  tgcgr4  28553  tglnfn  28569  tglnunirn  28570  mirne  28689  mircinv  28690  perpln1  28732  perpln2  28733  lmiisolem  28818  xmstrkgc  28914  axcgrtr  28944  axsegconlem9  28954  axlowdimlem5  28975  axlowdimlem17  28987  axlowdim1  28988  uhgr0e  29102  edglnl  29174  uhgr0edgfi  29271  issubgr2  29303  subgrprop2  29305  egrsubgr  29308  0grsubgr  29309  0uhgrsubgr  29310  uhgrsubgrself  29311  nbgr1vtx  29389  nbgrssovtx  29392  nb3grprlem1  29411  uvtx01vtx  29428  cplgr1vlem  29460  cplgr1v  29461  usgrexilem  29471  wlkcomp  29663  wlk1walk  29671  wlkp1lem5  29709  uhgrwkspthlem1  29785  pthdlem1  29798  clwlkcomp  29811  lfgrn1cycl  29834  uspgrn2crct  29837  wwlksn0s  29890  umgrwwlks2on  29986  clwwlkn  30054  clwwlkn1  30069  0ewlk  30142  1ewlk  30143  0spth  30154  upgr1wlkdlem2  30174  wlk2v2e  30185  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth0  30242  frgr0v  30290  frgr1v  30299  1vwmgr  30304  ex-opab  30460  grpoinvf  30560  nvmid  30687  nmlnoubi  30824  hiidrcl  31123  hsn0elch  31276  shjshseli  31521  cmbr4i  31629  dfiop2  31781  kbpj  31984  nmopun  32042  adjeq0  32119  kbass2  32145  pjssdif1i  32203  pjinvari  32219  pjcmul2i  32230  pj3i  32236  stge1i  32266  stle0i  32267  sumdmdlem2  32447  dmdbr6ati  32451  dmdbr7ati  32452  rabsnel  32527  unidifsnel  32560  unidifsnne  32561  disjdifprg  32594  ofoprabco  32680  padct  32736  fpwrelmapffslem  32749  xrlelttric  32762  xnn0gt0  32779  iundisj2cnt  32806  f1ocnt  32809  fz1nnct  32810  fz1nntr  32811  hashxpe  32816  nn0min  32826  wrdt2ind  32922  xrge0tsmsbi  33048  opprabs  33489  rtelextdg2lem  33731  2sqr3minply  33752  locfinref  33801  dispcmp  33819  zartopn  33835  zarcmplem  33841  pstmxmet  33857  xrge0iifcnv  33893  xrge0iif1  33898  qqhre  33982  esumcl  34010  esumpr2  34047  esumpinfval  34053  esumpcvgval  34058  ofcfn  34080  pwsiga  34110  prsiga  34111  sigainb  34116  ldgenpisyslem1  34143  measiuns  34197  relfae  34227  pmeasmono  34305  sitgf  34328  eulerpartgbij  34353  sgnmulsgn  34530  sgnmulsgp  34531  signswch  34554  signslema  34555  signstlen  34560  signstfvn  34562  circlevma  34635  bnj216  34724  bnj151  34869  bnj517  34877  bnj970  34939  bnj1145  34985  bnj1498  35053  fineqvrep  35087  fineqvac  35089  wevgblacfn  35092  0nn0m1nnn0  35096  pthhashvtx  35111  acycgr0v  35132  prclisacycgr  35135  umgracycusgr  35138  cusgracyclt3v  35140  subfacp1lem5  35168  erdszelem8  35182  kur14lem1  35190  indispconn  35218  cvmsss2  35258  satfvsuclem2  35344  satfrel  35351  satfrnmapom  35354  satfv0fun  35355  satf00  35358  satf0suclem  35359  fmlasuc0  35368  msubrn  35513  dfon2lem7  35770  brbigcup  35879  elsingles  35899  fnimage  35910  funpartlem  35923  dfrdg4  35932  imagesset  35934  altopthsn  35942  elaltxp  35956  ellines  36133  linethru  36134  rankeq1o  36152  elhf2  36156  hfninf  36167  nn0prpwlem  36304  fneref  36332  neibastop2lem  36342  limsucncmpi  36427  bj-exlimmpbir  36896  curryset  36928  bj-snglex  36955  bj-restpw  37074  bj-inftyexpidisj  37192  topdifinffinlem  37329  relowlssretop  37345  rdgeqoa  37352  finxpreclem6  37378  fvineqsneq  37394  pibt2  37399  poimirlem23  37629  poimirlem29  37635  poimirlem31  37637  volsupnfl  37651  cnambfre  37654  dvasin  37690  dvacos  37691  sdclem2  37728  sstotbnd2  37760  ssbnd  37774  ismgmOLD  37836  grpokerinj  37879  rngomndo  37921  isdrngo1  37942  ac6s6  38158  iss2  38325  cnvelrels  38476  cosselrels  38477  brssrid  38483  brcnvssrid  38488  dfdisjs5  38693  eldisjs5  38707  mpets2  38822  pets  38833  prtlem12  38848  riotasv2d  38938  lkrscss  39079  islshpkrN  39101  isline  39721  ispointN  39724  0psubN  39731  linepsubN  39734  atpsubN  39735  cdlemk36  40895  diafn  41016  dibfna  41136  dibvalrel  41145  dicvalrelN  41167  diclspsn  41176  dihvalrel  41261  dih1  41268  lclkrlem1  41488  lclkr  41515  mapd1o  41630  mapdin  41644  hdmapfnN  41811  hgmapfnN  41870  lcmineqlem10  42019  sticksstones9  42135  sn-iotalem  42238  readvrec2  42369  readvrec  42370  repncan2  42388  sn-inelr  42473  elrfirn  42682  ismrcd1  42685  istopclsd  42687  rabren3dioph  42802  jm2.17b  42949  jm2.22  42983  jm2.23  42984  ttac  43024  pw2f1ocnv  43025  dnnumch1  43032  hbtlem5  43116  mncn0  43127  aaitgo  43150  rngunsnply  43157  unielss  43206  onexlimgt  43231  cantnfresb  43313  dflim5  43318  naddwordnexlem4  43390  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  ensucne0OLD  43519  clcnvlem  43612  relexp01min  43702  ntrf  44112  ssrecnpr  44303  seff  44304  sblpnf  44305  nzss  44312  dvconstbi  44329  ipo0  44444  ifr0  44445  addrfn  44467  subrfn  44468  mulvfn  44469  wfaxrep  44949  refsum2cnlem1  44974  rn1st  45218  ellimciota  45569  dvmptconst  45870  dvmptidg  45872  dvmulcncf  45880  dvdivcncf  45882  stoweidlem26  45981  stoweidlem50  46005  stoweidlem57  46012  aiotaval  47044  ndfatafv2nrn  47170  afv2ndefb  47173  funop1  47232  fun2dmnopgexmpl  47233  2ffzoeq  47276  m1modne  47287  iccpartiltu  47346  iccpartigtl  47347  zofldiv2ALTV  47586  evenprm2  47638  9fppr8  47661  stgoldbwt  47700  nnsum3primesle9  47718  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  tgblthelfgott  47739  dfclnbgr6  47779  grtrimap  47850  stgredgel  47859  stgr1  47863  isubgr3stgrlem2  47869  isubgr3stgrlem3  47870  usgrexmpl2trifr  47931  2ltceilhalf  47949  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg5nbgr3star  47971  uspgrex  47993  0mgm  48009  nnsgrpmgm  48019  rngchomffvalALTV  48121  rhmsubcALTVlem1  48124  funcringcsetcALTV2lem4  48136  funcringcsetclem4ALTV  48159  srhmsubcALTV  48168  mapsnop  48188  zlmodzxzldeplem4  48348  zofldiv2  48380  fdivval  48388  nnlog2ge0lt1  48415  dig1  48457  itcoval2  48513  itcoval3  48514  mosn  48660  mo0  48661  mof02  48668  mofeu  48677  f102g  48681  f1mo  48682  f1omo  48690  intubeu  48772  unilbeu  48773  functhinclem1  48840  fullthinc  48845  thincciso  48848  indthinc  48852  indthincALT  48853