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  2398  nfald2  2449  nfabd2  2922  raleleq  3321  raleleqOLD  3322  ceqsexv2d  3512  dedhb  3686  csbie2df  4418  ssdifeq0  4462  r19.2zb  4471  dedth  4559  pwidg  4595  snidg  4636  rexreusng  4655  exsnrex  4656  ifpr  4669  rmosn  4695  rabrsn  4700  prid1g  4736  tpid1g  4745  tpid2g  4747  tpid3g  4748  pwpw0  4789  sssn  4802  elpreqpr  4843  unimax  4920  intmin3  4952  eqbrtrdi  5158  al0ssb  5278  rabelpw  5306  intabs  5319  difelpw  5324  0inp0  5329  axpr  5397  intidg  5432  copsexgw  5465  copsexg  5466  euotd  5488  elopab  5502  elvvuni  5731  posn  5740  frsn  5742  eqrelriv  5768  relsnb  5781  relopabiALT  5802  opabid2  5807  ididg  5833  iss  6022  dfpo2  6285  ord0eln0  6408  sucidg  6434  nsuceq0  6436  funopg  6569  fn0  6668  f00  6759  f0bi  6760  f10d  6851  f1o00  6852  fo00  6853  brprcneu  6865  brprcneuALT  6866  dffn5  6936  fsn  7124  funop  7138  funsndifnop  7140  fnsnbOLD  7157  eufnfv  7220  f1ounsn  7264  f1eqcocnv  7293  nfriotadw  7368  nfriotad  7371  riotaprop  7387  oprabidw  7434  oprabid  7435  elrnmpo  7541  ov6g  7569  ovelrn  7581  caovmo  7642  offn  7682  caofinvl  7701  fr3nr  7764  onprc  7770  ordeleqon  7774  onint0  7783  0elsuc  7827  onuninsuci  7833  orduninsuc  7836  ordzsl  7838  onzsl  7839  tfinds  7853  limomss  7864  limom  7875  peano5  7887  xpexr  7912  eqop2  8029  opreuopreu  8031  1stconst  8097  2ndconst  8098  frxp2  8141  frxp3  8148  funsssuppss  8187  dftpos3  8241  dftpos4  8242  wfrlem4OLD  8324  wfrlem14OLD  8334  oawordeulem  8564  omwordi  8581  nnmwordi  8645  riiner  8802  ecopover  8833  map0g  8896  mapsnd  8898  elixpsn  8949  en0  9030  en0ALT  9031  en0r  9032  en1  9036  snfi  9055  fiprc  9057  sbthlem2  9096  sbthlem4  9098  sbthlem5  9099  0domg  9112  findcard  9175  findcard2  9176  nneneq  9218  sdom1  9248  sdom1OLD  9249  1sdom2dom  9253  fineqvlem  9268  nfielex  9277  enp1i  9283  elfiun  9440  marypha1lem  9443  oicl  9541  oif  9542  oion  9548  hartogslem1  9554  hartogs  9556  wemapso2  9565  card2on  9566  0wdom  9582  brwdom2  9585  inf3lem6  9645  cantnflem3  9703  cantnflem4  9704  wemapwe  9709  cnfcom  9712  ssttrcl  9727  ttrclselem2  9738  tctr  9752  r1tr  9788  r1rankidb  9816  r1pw  9857  scottex  9897  scott0  9898  bnd2  9905  eldju2ndl  9936  tskwe  9962  oncard  9972  cardlim  9984  harsdom  10007  en2eleq  10020  dfac8alem  10041  cardaleph  10101  iunfictbso  10126  infmap2  10229  ackbij1lem18  10248  cff  10260  cfsuc  10269  cff1  10270  cflim2  10275  cfss  10277  sdom2en01  10314  infpssrlem4  10318  fin23lem7  10328  fin23lem11  10329  isfin2-2  10331  fin23lem26  10337  fin23lem19  10348  fin23lem17  10350  isf34lem2  10385  isf34lem4  10389  fin1a2lem6  10417  fin1a2lem10  10421  fin1a2lem12  10423  itunifn  10429  hsmexlem1  10438  axcc2lem  10448  dcomex  10459  axdc3lem4  10465  ondomon  10575  konigthlem  10580  pwcfsdom  10595  cfpwsdom  10596  axpowndlem3  10611  canth4  10659  canthnumlem  10660  canthwelem  10662  canthwe  10663  canthp1lem2  10665  pwfseqlem4  10674  pwfseqlem5  10675  gchaleph  10683  gch2  10687  winainflem  10705  0tsk  10767  rankcf  10789  tskcard  10793  gruina  10830  grutsk  10834  tskmid  10852  indpi  10919  nqereu  10941  mulcanenq  10972  recmulnq  10976  archnq  10992  ltsopr  11044  1ne0sr  11108  0idsr  11109  00sr  11111  leid  11329  lelttric  11340  divcan3  11920  divid  11925  div0  11927  lemul1a  12093  nn1suc  12260  nn0n0n1ge2b  12568  xnn0xr  12577  xnn0nemnf  12583  nn0lt10b  12653  nn0ind-raph  12691  elnn1uz2  12939  indstr2  12941  uzsupss  12954  rpnnen1lem4  12994  rpnnen1lem5  12995  xrnemnf  13131  xrnepnf  13132  mnfltxr  13141  xnn0n0n1ge2b  13146  xnn0ge0  13148  xrlttri  13153  xrlttr  13154  xrleid  13165  qbtwnxr  13214  xmullem2  13279  xlemul1a  13302  xrub  13326  reltxrnmnf  13357  ixxun  13376  xnn0xrge0  13521  fztpval  13601  fseq1p1m1  13613  elfznelfzob  13787  ltweuz  13977  fzfi  13988  fsuppmapnn0fiubex  14008  ser0f  14071  0exp  14113  faclbnd4lem1  14309  bcn1  14329  hashnemnf  14360  hashv01gt1  14361  hashsnle1  14433  hashgt12el2  14439  hashpw  14452  hashf1  14473  fz1isolem  14477  hash2prb  14488  hash3tpb  14511  0wrd0  14556  wrdlen1  14570  ccatvalfn  14597  eqs1  14628  wrdl1exs1  14629  swrdlen  14663  swrdwrdsymb  14678  swrdspsleq  14681  cats1un  14737  wrdind  14738  wrd2ind  14739  swrdccatin1  14741  repswsymballbi  14796  cshw1  14838  scshwfzeqfzo  14843  wrdl2exs2  14963  trclfvcotr  15026  relexp1g  15043  relexp0rel  15054  relexprelg  15055  relexpreld  15057  sqrt0  15258  sqrtsq  15286  mptfzshft  15792  prodf1f  15906  egt2lt3  16222  0dvds  16294  nn0onn  16397  nn0o  16400  divalgmod  16423  flodddiv4  16432  bitsp1o  16450  gcddvds  16520  bezout  16560  lcmdvds  16625  rpdvds  16677  1nprm  16696  prmind2  16702  dvdszzq  16738  nnoddn2prmb  16831  pcpre1  16860  vdwapf  16990  vdwapid1  16993  ram0  17040  ramz  17043  prmolefac  17064  cshws0  17119  prmlem0  17123  strle1  17175  restsspw  17443  prdsdsfn  17477  imasdsfn  17526  imasaddfnlem  17540  imasvscafn  17549  xpsfrnel  17574  isacs1i  17667  cidfn  17689  fnhomeqhomf  17701  comffn  17715  isoval  17776  sscres  17834  cofucl  17899  idffth  17946  ressffth  17951  cat1lem  18107  catcoppccl  18128  estrchomfn  18145  funcestrcsetclem4  18153  funcestrcsetclem7  18156  equivestrcsetc  18162  funcsetcestrclem4  18168  funcsetcestrclem7  18171  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlfcl  18232  curf1cl  18238  curfcl  18242  hofcl  18269  yonedainv  18291  pospo  18353  lubfun  18360  glbfun  18373  joindmss  18387  meetdmss  18401  ipopos  18544  acsficl2d  18560  dirref  18609  mgmidcl  18642  mgmlrid  18643  ielefmnd  18863  smndex1basss  18881  smndex1n0mnd  18888  cntzssv  19309  idresperm  19365  symgvalstruct  19376  pmtrfmvdn0  19441  symggen  19449  psgnunilem1  19472  psgnprfval  19500  slwpgp  19592  frgpmhm  19744  frgpuptinv  19750  frgpup3lem  19756  gsumzoppg  19923  gsumcom2  19954  c0snmhm  20421  srhmsubc  20638  rhmsubclem1  20643  rrgsupp  20659  abv0  20781  zrhrhm  21470  psgnodpmr  21548  frlmphllem  21738  ellspd  21760  psrvscafval  21906  psrridm  21921  ltbwe  22000  psrbag0  22018  psrbagsn  22019  subrgascl  22022  psdmul  22102  mattpostpos  22390  mavmul0  22488  mavmul0g  22489  mdet0f1o  22529  m1detdiag  22533  m2detleiblem5  22561  m2detleiblem6  22562  m2detleiblem3  22565  m2detleiblem4  22566  maducoeval2  22576  d1mat2pmat  22675  chpmat1dlem  22771  chpmat1d  22772  baspartn  22890  eltg3  22898  topnex  22932  fctop  22940  cctop  22942  discld  23025  mretopd  23028  neipeltop  23065  neitr  23116  restcls  23117  ordtbaslem  23124  ordtuni  23126  idcn  23193  cnrmi  23296  cmpsublem  23335  cmpsub  23336  tgcmp  23337  uncmp  23339  hauscmplem  23342  cmpfi  23344  bwth  23346  1stcrestlem  23388  disllycmp  23434  dis1stc  23435  refref  23449  kgeni  23473  1stckgenlem  23489  kqffn  23661  snfil  23800  filconn  23819  cfinfil  23829  ufileu  23855  filufint  23856  fixufil  23858  cfinufil  23864  ufilen  23866  fin1aufil  23868  fmf  23881  rnelfm  23889  flimclslem  23920  hauspwpwf1  23923  supnfcls  23956  flimfnfcls  23964  fclscmp  23966  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALT  23987  ptcmplem1  23988  cnextrel  23999  tsmsfbas  24064  ustref  24155  trust  24166  restutop  24174  isusp  24198  xmet0  24279  imasdsf1olem  24310  blfvalps  24320  blfps  24343  blf  24344  restmetu  24507  dscmet  24509  isngp2  24534  nm0  24566  nrginvrcn  24629  nmoix  24666  qdensere  24706  iccconn  24768  iccpnfcnv  24891  xrhmeo  24893  lebnumlem3  24911  metsscmetcld  25265  bcthlem5  25278  csschl  25326  rrxmfval  25356  minveclem3b  25378  cniccbdd  25412  ovolicc2lem4  25471  iunmbl  25504  ioorinv  25527  ioorcl  25528  i1f1lem  25640  limcvallem  25822  ellimc2  25828  limccnp  25842  limccnp2  25843  limcco  25844  perfdvf  25854  recnprss  25855  fncpn  25885  dvcmulf  25898  c1lip1  25952  lhop2  25970  q1pcl  26112  r1pdeglt  26115  ply1remlem  26120  plyssc  26155  ulm0  26350  cxpeq0  26637  cxplea  26655  cxplogb  26746  asinlem  26828  isppw2  27075  muval2  27094  dchrfi  27216  dchrpt  27228  bposlem6  27250  lgsdir2lem2  27287  lgsqr  27312  gausslemma2dlem4  27330  2lgslem2  27356  2lgslem3  27365  2lgs  27368  2sqlem7  27385  2sqlem11  27390  chtppilim  27436  nosgnn0i  27621  nolesgn2ores  27634  nogesgn1ores  27636  nosepnelem  27641  nosepdmlem  27645  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd2lem1  27677  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd2lem1  27692  oldval  27810  made0  27829  lrrecpo  27891  pncan2s  28021  divscan3d  28177  abssor  28187  om2noseqfo  28221  noseqrdglem  28228  noseqrdgfn  28229  noseqrdg0  28230  n0scut  28255  nohalf  28324  expsne0  28331  tgldimor  28427  tgcgr4  28456  tglnfn  28472  tglnunirn  28473  mirne  28592  mircinv  28593  perpln1  28635  perpln2  28636  lmiisolem  28721  xmstrkgc  28811  axcgrtr  28840  axsegconlem9  28850  axlowdimlem5  28871  axlowdimlem17  28883  axlowdim1  28884  uhgr0e  28996  edglnl  29068  uhgr0edgfi  29165  issubgr2  29197  subgrprop2  29199  egrsubgr  29202  0grsubgr  29203  0uhgrsubgr  29204  uhgrsubgrself  29205  nbgr1vtx  29283  nbgrssovtx  29286  nb3grprlem1  29305  uvtx01vtx  29322  cplgr1vlem  29354  cplgr1v  29355  usgrexilem  29365  wlkcomp  29557  wlk1walk  29565  wlkp1lem5  29603  uhgrwkspthlem1  29681  pthdlem1  29694  clwlkcomp  29707  lfgrn1cycl  29733  uspgrn2crct  29736  wwlksn0s  29789  umgrwwlks2on  29885  clwwlkn  29953  clwwlkn1  29968  0ewlk  30041  1ewlk  30042  0spth  30053  upgr1wlkdlem2  30073  wlk2v2e  30084  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eupth0  30141  frgr0v  30189  frgr1v  30198  1vwmgr  30203  ex-opab  30359  grpoinvf  30459  nvmid  30586  nmlnoubi  30723  hiidrcl  31022  hsn0elch  31175  shjshseli  31420  cmbr4i  31528  dfiop2  31680  kbpj  31883  nmopun  31941  adjeq0  32018  kbass2  32044  pjssdif1i  32102  pjinvari  32118  pjcmul2i  32129  pj3i  32135  stge1i  32165  stle0i  32166  sumdmdlem2  32346  dmdbr6ati  32350  dmdbr7ati  32351  rabsnel  32427  unidifsnel  32462  unidifsnne  32463  disjdifprg  32502  ofoprabco  32588  padct  32643  fpwrelmapffslem  32655  xrlelttric  32675  xnn0gt0  32692  iundisj2cnt  32722  f1ocnt  32725  fz1nnct  32726  fz1nntr  32727  hashxpe  32732  nn0min  32745  sgnmulsgn  32767  sgnmulsgp  32768  wrdt2ind  32875  xrge0tsmsbi  33003  opprabs  33443  rtelextdg2lem  33706  2sqr3minply  33760  locfinref  33818  dispcmp  33836  zartopn  33852  zarcmplem  33858  pstmxmet  33874  xrge0iifcnv  33910  xrge0iif1  33915  qqhre  33997  esumcl  34007  esumpr2  34044  esumpinfval  34050  esumpcvgval  34055  ofcfn  34077  pwsiga  34107  prsiga  34108  sigainb  34113  ldgenpisyslem1  34140  measiuns  34194  relfae  34224  pmeasmono  34302  sitgf  34325  eulerpartgbij  34350  signswch  34539  signslema  34540  signstlen  34545  signstfvn  34547  circlevma  34620  bnj216  34709  bnj151  34854  bnj517  34862  bnj970  34924  bnj1145  34970  bnj1498  35038  fineqvrep  35072  fineqvac  35074  wevgblacfn  35077  0nn0m1nnn0  35081  pthhashvtx  35096  acycgr0v  35116  prclisacycgr  35119  umgracycusgr  35122  cusgracyclt3v  35124  subfacp1lem5  35152  erdszelem8  35166  kur14lem1  35174  indispconn  35202  cvmsss2  35242  satfvsuclem2  35328  satfrel  35335  satfrnmapom  35338  satfv0fun  35339  satf00  35342  satf0suclem  35343  fmlasuc0  35352  msubrn  35497  dfon2lem7  35753  brbigcup  35862  elsingles  35882  fnimage  35893  funpartlem  35906  dfrdg4  35915  imagesset  35917  altopthsn  35925  elaltxp  35939  ellines  36116  linethru  36117  rankeq1o  36135  elhf2  36139  hfninf  36150  nn0prpwlem  36286  fneref  36314  neibastop2lem  36324  limsucncmpi  36409  bj-exlimmpbir  36878  curryset  36910  bj-snglex  36937  bj-restpw  37056  bj-inftyexpidisj  37174  topdifinffinlem  37311  relowlssretop  37327  rdgeqoa  37334  finxpreclem6  37360  fvineqsneq  37376  pibt2  37381  poimirlem23  37613  poimirlem29  37619  poimirlem31  37621  volsupnfl  37635  cnambfre  37638  dvasin  37674  dvacos  37675  sdclem2  37712  sstotbnd2  37744  ssbnd  37758  ismgmOLD  37820  grpokerinj  37863  rngomndo  37905  isdrngo1  37926  ac6s6  38142  iss2  38308  cnvelrels  38459  cosselrels  38460  brssrid  38466  brcnvssrid  38471  dfdisjs5  38676  eldisjs5  38690  mpets2  38805  pets  38816  prtlem12  38831  riotasv2d  38921  lkrscss  39062  islshpkrN  39084  isline  39704  ispointN  39707  0psubN  39714  linepsubN  39717  atpsubN  39718  cdlemk36  40878  diafn  40999  dibfna  41119  dibvalrel  41128  dicvalrelN  41150  diclspsn  41159  dihvalrel  41244  dih1  41251  lclkrlem1  41471  lclkr  41498  mapd1o  41613  mapdin  41627  hdmapfnN  41794  hgmapfnN  41853  lcmineqlem10  41997  sticksstones9  42113  sn-iotalem  42218  readvrec2  42351  readvrec  42352  repncan2  42372  sn-inelr  42457  elrfirn  42665  ismrcd1  42668  istopclsd  42670  rabren3dioph  42785  jm2.17b  42932  jm2.22  42966  jm2.23  42967  ttac  43007  pw2f1ocnv  43008  dnnumch1  43015  hbtlem5  43099  mncn0  43110  aaitgo  43133  rngunsnply  43140  unielss  43189  onexlimgt  43214  cantnfresb  43295  dflim5  43300  naddwordnexlem4  43372  safesnsupfiss  43386  safesnsupfidom1o  43388  safesnsupfilb  43389  ensucne0OLD  43501  clcnvlem  43594  relexp01min  43684  ntrf  44094  ssrecnpr  44280  seff  44281  sblpnf  44282  nzss  44289  dvconstbi  44306  ipo0  44421  ifr0  44422  addrfn  44444  subrfn  44445  mulvfn  44446  wfaxrep  44967  refsum2cnlem1  45009  rn1st  45245  ellimciota  45591  dvmptconst  45892  dvmptidg  45894  dvmulcncf  45902  dvdivcncf  45904  stoweidlem26  46003  stoweidlem50  46027  stoweidlem57  46034  aiotaval  47072  ndfatafv2nrn  47198  afv2ndefb  47201  funop1  47260  fun2dmnopgexmpl  47261  2ffzoeq  47304  2ltceilhalf  47305  m1modne  47325  iccpartiltu  47384  iccpartigtl  47385  zofldiv2ALTV  47624  evenprm2  47676  9fppr8  47699  stgoldbwt  47738  nnsum3primesle9  47756  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  tgblthelfgott  47777  dfclnbgr6  47817  cycl3grtri  47907  grtrimap  47908  stgredgel  47917  stgr1  47921  isubgr3stgrlem2  47927  isubgr3stgrlem3  47928  usgrexmpl2trifr  47989  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg5nbgr3star  48031  gpg3kgrtriex  48039  uspgrex  48073  0mgm  48089  nnsgrpmgm  48099  rngchomffvalALTV  48201  rhmsubcALTVlem1  48204  funcringcsetcALTV2lem4  48216  funcringcsetclem4ALTV  48239  srhmsubcALTV  48248  mapsnop  48267  zlmodzxzldeplem4  48427  zofldiv2  48459  fdivval  48467  nnlog2ge0lt1  48494  dig1  48536  itcoval2  48592  itcoval3  48593  mosn  48739  mo0  48740  mof02  48765  mofeu  48774  f102g  48778  f1mo  48779  tposres0  48800  f1omo  48816  resipos  48897  intubeu  48906  unilbeu  48907  sectfn  48947  nelsubclem  48982  imaidfu  49017  oppfvallem  49029  funcoppc3  49038  idfth  49046  idsubc  49047  uptposlem  49078  swapf2fn  49133  swapf1f1o  49140  swapf2f1o  49141  swapf2f1oaALT  49143  fucof1  49181  fucofn2  49183  fucofn22  49199  reldmprcof1  49239  reldmprcof2  49240  functhinclem1  49278  fullthinc  49284  thincciso  49287  indcthing  49294  indthinc  49296  indthincALT  49297  functermc  49341  discsntermlem  49395  reldmlan2  49440  reldmran2  49441  rellan  49446  relran  49447