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  2929  raleleq  3342  raleleqOLD  3343  ceqsexv2d  3533  dedhb  3709  sbceqalOLD  3852  csbie2df  4443  ssdifeq0  4487  r19.2zb  4496  dedth  4584  pwidg  4620  snidg  4660  rexreusng  4679  exsnrex  4680  ifpr  4693  rmosn  4719  rabrsn  4724  prid1g  4760  tpid1g  4769  tpid2g  4771  tpid3g  4772  pwpw0  4813  sssn  4826  elpreqpr  4867  unimax  4944  intmin3  4976  eqbrtrdi  5182  al0ssb  5308  rabelpw  5336  intabs  5349  difelpw  5354  0inp0  5359  axpr  5427  intidg  5462  copsexgw  5495  copsexg  5496  euotd  5518  elopab  5532  elvvuni  5762  posn  5771  frsn  5773  eqrelriv  5799  relsnb  5812  relopabiALT  5833  opabid2  5838  ididg  5864  iss  6053  dfpo2  6316  ord0eln0  6439  sucidg  6465  nsuceq0  6467  funopg  6600  fn0  6699  f00  6790  f0bi  6791  f10d  6882  f1o00  6883  fo00  6884  brprcneu  6896  brprcneuALT  6897  dffn5  6967  fsn  7155  funop  7169  funsndifnop  7171  fnsnb  7186  eufnfv  7249  f1ounsn  7292  f1eqcocnv  7321  nfriotadw  7396  nfriotad  7399  riotaprop  7415  oprabidw  7462  oprabid  7463  elrnmpo  7569  ov6g  7597  ovelrn  7609  caovmo  7670  offn  7710  caofinvl  7729  fr3nr  7792  onprc  7798  ordeleqon  7802  onint0  7811  0elsuc  7855  onuninsuci  7861  orduninsuc  7864  ordzsl  7866  onzsl  7867  tfinds  7881  limomss  7892  limom  7903  peano5  7915  xpexr  7940  eqop2  8057  opreuopreu  8059  1stconst  8125  2ndconst  8126  frxp2  8169  frxp3  8176  funsssuppss  8215  dftpos3  8269  dftpos4  8270  wfrlem4OLD  8352  wfrlem14OLD  8362  oawordeulem  8592  omwordi  8609  nnmwordi  8673  riiner  8830  ecopover  8861  map0g  8924  mapsnd  8926  elixpsn  8977  en0  9058  en0ALT  9059  en0r  9060  en1  9064  snfi  9083  fiprc  9085  sbthlem2  9124  sbthlem4  9126  sbthlem5  9127  0domg  9140  findcard  9203  findcard2  9204  nneneq  9246  nneneqOLD  9258  sdom1  9278  sdom1OLD  9279  1sdom2dom  9283  fineqvlem  9298  nfielex  9307  enp1i  9313  elfiun  9470  marypha1lem  9473  oicl  9569  oif  9570  oion  9576  hartogslem1  9582  hartogs  9584  wemapso2  9593  card2on  9594  0wdom  9610  brwdom2  9613  inf3lem6  9673  cantnflem3  9731  cantnflem4  9732  wemapwe  9737  cnfcom  9740  ssttrcl  9755  ttrclselem2  9766  tctr  9780  r1tr  9816  r1rankidb  9844  r1pw  9885  scottex  9925  scott0  9926  bnd2  9933  eldju2ndl  9964  tskwe  9990  oncard  10000  cardlim  10012  harsdom  10035  en2eleq  10048  dfac8alem  10069  cardaleph  10129  iunfictbso  10154  infmap2  10257  ackbij1lem18  10276  cff  10288  cfsuc  10297  cff1  10298  cflim2  10303  cfss  10305  sdom2en01  10342  infpssrlem4  10346  fin23lem7  10356  fin23lem11  10357  isfin2-2  10359  fin23lem26  10365  fin23lem19  10376  fin23lem17  10378  isf34lem2  10413  isf34lem4  10417  fin1a2lem6  10445  fin1a2lem10  10449  fin1a2lem12  10451  itunifn  10457  hsmexlem1  10466  axcc2lem  10476  dcomex  10487  axdc3lem4  10493  ondomon  10603  konigthlem  10608  pwcfsdom  10623  cfpwsdom  10624  axpowndlem3  10639  canth4  10687  canthnumlem  10688  canthwelem  10690  canthwe  10691  canthp1lem2  10693  pwfseqlem4  10702  pwfseqlem5  10703  gchaleph  10711  gch2  10715  winainflem  10733  0tsk  10795  rankcf  10817  tskcard  10821  gruina  10858  grutsk  10862  tskmid  10880  indpi  10947  nqereu  10969  mulcanenq  11000  recmulnq  11004  archnq  11020  ltsopr  11072  1ne0sr  11136  0idsr  11137  00sr  11139  leid  11357  lelttric  11368  divcan3  11948  divid  11953  div0  11955  lemul1a  12121  nn1suc  12288  nn0n0n1ge2b  12595  xnn0xr  12604  xnn0nemnf  12610  nn0lt10b  12680  nn0ind-raph  12718  elnn1uz2  12967  indstr2  12969  uzsupss  12982  rpnnen1lem4  13022  rpnnen1lem5  13023  xrnemnf  13159  xrnepnf  13160  mnfltxr  13169  xnn0n0n1ge2b  13174  xnn0ge0  13176  xrlttri  13181  xrlttr  13182  xrleid  13193  qbtwnxr  13242  xmullem2  13307  xlemul1a  13330  xrub  13354  reltxrnmnf  13384  ixxun  13403  xnn0xrge0  13546  fztpval  13626  fseq1p1m1  13638  elfznelfzob  13812  ltweuz  14002  fzfi  14013  fsuppmapnn0fiubex  14033  ser0f  14096  0exp  14138  faclbnd4lem1  14332  bcn1  14352  hashnemnf  14383  hashv01gt1  14384  hashsnle1  14456  hashgt12el2  14462  hashpw  14475  hashf1  14496  fz1isolem  14500  hash2prb  14511  hash3tpb  14534  0wrd0  14578  wrdlen1  14592  ccatvalfn  14619  eqs1  14650  wrdl1exs1  14651  swrdlen  14685  swrdwrdsymb  14700  swrdspsleq  14703  cats1un  14759  wrdind  14760  wrd2ind  14761  swrdccatin1  14763  repswsymballbi  14818  cshw1  14860  scshwfzeqfzo  14865  wrdl2exs2  14985  trclfvcotr  15048  relexp1g  15065  relexp0rel  15076  relexprelg  15077  relexpreld  15079  sqrt0  15280  sqrtsq  15308  mptfzshft  15814  prodf1f  15928  egt2lt3  16242  0dvds  16314  nn0onn  16417  nn0o  16420  divalgmod  16443  flodddiv4  16452  bitsp1o  16470  gcddvds  16540  bezout  16580  lcmdvds  16645  rpdvds  16697  1nprm  16716  prmind2  16722  dvdszzq  16758  nnoddn2prmb  16851  pcpre1  16880  vdwapf  17010  vdwapid1  17013  ram0  17060  ramz  17063  prmolefac  17084  cshws0  17139  prmlem0  17143  strle1  17195  restsspw  17476  prdsdsfn  17510  imasdsfn  17559  imasaddfnlem  17573  imasvscafn  17582  xpsfrnel  17607  isacs1i  17700  cidfn  17722  fnhomeqhomf  17734  comffn  17748  isoval  17809  sscres  17867  cofucl  17933  idffth  17980  ressffth  17985  cat1lem  18141  catcoppccl  18162  estrchomfn  18179  funcestrcsetclem4  18188  funcestrcsetclem7  18191  equivestrcsetc  18197  funcsetcestrclem4  18203  funcsetcestrclem7  18206  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  yonedainv  18326  pospo  18390  lubfun  18397  glbfun  18410  joindmss  18424  meetdmss  18438  ipopos  18581  acsficl2d  18597  dirref  18646  mgmidcl  18679  mgmlrid  18680  ielefmnd  18900  smndex1basss  18918  smndex1n0mnd  18925  cntzssv  19346  idresperm  19403  symgvalstruct  19414  symgvalstructOLD  19415  pmtrfmvdn0  19480  symggen  19488  psgnunilem1  19511  psgnprfval  19539  slwpgp  19631  frgpmhm  19783  frgpuptinv  19789  frgpup3lem  19795  gsumzoppg  19962  gsumcom2  19993  c0snmhm  20463  srhmsubc  20680  rhmsubclem1  20685  rrgsupp  20701  abv0  20824  zrhrhm  21522  psgnodpmr  21608  frlmphllem  21800  ellspd  21822  psrvscafval  21968  psrridm  21983  ltbwe  22062  psrbag0  22086  psrbagsn  22087  subrgascl  22090  psdmul  22170  mattpostpos  22460  mavmul0  22558  mavmul0g  22559  mdet0f1o  22599  m1detdiag  22603  m2detleiblem5  22631  m2detleiblem6  22632  m2detleiblem3  22635  m2detleiblem4  22636  maducoeval2  22646  d1mat2pmat  22745  chpmat1dlem  22841  chpmat1d  22842  baspartn  22961  eltg3  22969  topnex  23003  fctop  23011  cctop  23013  discld  23097  mretopd  23100  neipeltop  23137  neitr  23188  restcls  23189  ordtbaslem  23196  ordtuni  23198  idcn  23265  cnrmi  23368  cmpsublem  23407  cmpsub  23408  tgcmp  23409  uncmp  23411  hauscmplem  23414  cmpfi  23416  bwth  23418  1stcrestlem  23460  disllycmp  23506  dis1stc  23507  refref  23521  kgeni  23545  1stckgenlem  23561  kqffn  23733  snfil  23872  filconn  23891  cfinfil  23901  ufileu  23927  filufint  23928  fixufil  23930  cfinufil  23936  ufilen  23938  fin1aufil  23940  fmf  23953  rnelfm  23961  flimclslem  23992  hauspwpwf1  23995  supnfcls  24028  flimfnfcls  24036  fclscmp  24038  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALT  24059  ptcmplem1  24060  cnextrel  24071  tsmsfbas  24136  ustref  24227  trust  24238  restutop  24246  isusp  24270  xmet0  24352  imasdsf1olem  24383  blfvalps  24393  blfps  24416  blf  24417  restmetu  24583  dscmet  24585  isngp2  24610  nm0  24642  nrginvrcn  24713  nmoix  24750  qdensere  24790  iccconn  24852  iccpnfcnv  24975  xrhmeo  24977  lebnumlem3  24995  metsscmetcld  25349  bcthlem5  25362  csschl  25410  rrxmfval  25440  minveclem3b  25462  cniccbdd  25496  ovolicc2lem4  25555  iunmbl  25588  ioorinv  25611  ioorcl  25612  i1f1lem  25724  limcvallem  25906  ellimc2  25912  limccnp  25926  limccnp2  25927  limcco  25928  perfdvf  25938  recnprss  25939  fncpn  25969  dvcmulf  25982  c1lip1  26036  lhop2  26054  q1pcl  26196  r1pdeglt  26199  ply1remlem  26204  plyssc  26239  ulm0  26434  cxpeq0  26720  cxplea  26738  cxplogb  26829  asinlem  26911  isppw2  27158  muval2  27177  dchrfi  27299  dchrpt  27311  bposlem6  27333  lgsdir2lem2  27370  lgsqr  27395  gausslemma2dlem4  27413  2lgslem2  27439  2lgslem3  27448  2lgs  27451  2sqlem7  27468  2sqlem11  27473  chtppilim  27519  nosgnn0i  27704  nolesgn2ores  27717  nogesgn1ores  27719  nosepnelem  27724  nosepdmlem  27728  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  oldval  27893  made0  27912  lrrecpo  27974  pncan2s  28104  divscan3d  28260  abssor  28270  om2noseqfo  28304  noseqrdglem  28311  noseqrdgfn  28312  noseqrdg0  28313  n0scut  28338  nohalf  28407  expsne0  28414  tgldimor  28510  tgcgr4  28539  tglnfn  28555  tglnunirn  28556  mirne  28675  mircinv  28676  perpln1  28718  perpln2  28719  lmiisolem  28804  xmstrkgc  28900  axcgrtr  28930  axsegconlem9  28940  axlowdimlem5  28961  axlowdimlem17  28973  axlowdim1  28974  uhgr0e  29088  edglnl  29160  uhgr0edgfi  29257  issubgr2  29289  subgrprop2  29291  egrsubgr  29294  0grsubgr  29295  0uhgrsubgr  29296  uhgrsubgrself  29297  nbgr1vtx  29375  nbgrssovtx  29378  nb3grprlem1  29397  uvtx01vtx  29414  cplgr1vlem  29446  cplgr1v  29447  usgrexilem  29457  wlkcomp  29649  wlk1walk  29657  wlkp1lem5  29695  uhgrwkspthlem1  29773  pthdlem1  29786  clwlkcomp  29799  lfgrn1cycl  29825  uspgrn2crct  29828  wwlksn0s  29881  umgrwwlks2on  29977  clwwlkn  30045  clwwlkn1  30060  0ewlk  30133  1ewlk  30134  0spth  30145  upgr1wlkdlem2  30165  wlk2v2e  30176  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth0  30233  frgr0v  30281  frgr1v  30290  1vwmgr  30295  ex-opab  30451  grpoinvf  30551  nvmid  30678  nmlnoubi  30815  hiidrcl  31114  hsn0elch  31267  shjshseli  31512  cmbr4i  31620  dfiop2  31772  kbpj  31975  nmopun  32033  adjeq0  32110  kbass2  32136  pjssdif1i  32194  pjinvari  32210  pjcmul2i  32221  pj3i  32227  stge1i  32257  stle0i  32258  sumdmdlem2  32438  dmdbr6ati  32442  dmdbr7ati  32443  rabsnel  32519  unidifsnel  32553  unidifsnne  32554  disjdifprg  32588  ofoprabco  32674  padct  32731  fpwrelmapffslem  32743  xrlelttric  32756  xnn0gt0  32773  iundisj2cnt  32801  f1ocnt  32804  fz1nnct  32805  fz1nntr  32806  hashxpe  32811  nn0min  32822  wrdt2ind  32938  xrge0tsmsbi  33066  opprabs  33510  rtelextdg2lem  33767  2sqr3minply  33791  locfinref  33840  dispcmp  33858  zartopn  33874  zarcmplem  33880  pstmxmet  33896  xrge0iifcnv  33932  xrge0iif1  33937  qqhre  34021  esumcl  34031  esumpr2  34068  esumpinfval  34074  esumpcvgval  34079  ofcfn  34101  pwsiga  34131  prsiga  34132  sigainb  34137  ldgenpisyslem1  34164  measiuns  34218  relfae  34248  pmeasmono  34326  sitgf  34349  eulerpartgbij  34374  sgnmulsgn  34552  sgnmulsgp  34553  signswch  34576  signslema  34577  signstlen  34582  signstfvn  34584  circlevma  34657  bnj216  34746  bnj151  34891  bnj517  34899  bnj970  34961  bnj1145  35007  bnj1498  35075  fineqvrep  35109  fineqvac  35111  wevgblacfn  35114  0nn0m1nnn0  35118  pthhashvtx  35133  acycgr0v  35153  prclisacycgr  35156  umgracycusgr  35159  cusgracyclt3v  35161  subfacp1lem5  35189  erdszelem8  35203  kur14lem1  35211  indispconn  35239  cvmsss2  35279  satfvsuclem2  35365  satfrel  35372  satfrnmapom  35375  satfv0fun  35376  satf00  35379  satf0suclem  35380  fmlasuc0  35389  msubrn  35534  dfon2lem7  35790  brbigcup  35899  elsingles  35919  fnimage  35930  funpartlem  35943  dfrdg4  35952  imagesset  35954  altopthsn  35962  elaltxp  35976  ellines  36153  linethru  36154  rankeq1o  36172  elhf2  36176  hfninf  36187  nn0prpwlem  36323  fneref  36351  neibastop2lem  36361  limsucncmpi  36446  bj-exlimmpbir  36915  curryset  36947  bj-snglex  36974  bj-restpw  37093  bj-inftyexpidisj  37211  topdifinffinlem  37348  relowlssretop  37364  rdgeqoa  37371  finxpreclem6  37397  fvineqsneq  37413  pibt2  37418  poimirlem23  37650  poimirlem29  37656  poimirlem31  37658  volsupnfl  37672  cnambfre  37675  dvasin  37711  dvacos  37712  sdclem2  37749  sstotbnd2  37781  ssbnd  37795  ismgmOLD  37857  grpokerinj  37900  rngomndo  37942  isdrngo1  37963  ac6s6  38179  iss2  38345  cnvelrels  38496  cosselrels  38497  brssrid  38503  brcnvssrid  38508  dfdisjs5  38713  eldisjs5  38727  mpets2  38842  pets  38853  prtlem12  38868  riotasv2d  38958  lkrscss  39099  islshpkrN  39121  isline  39741  ispointN  39744  0psubN  39751  linepsubN  39754  atpsubN  39755  cdlemk36  40915  diafn  41036  dibfna  41156  dibvalrel  41165  dicvalrelN  41187  diclspsn  41196  dihvalrel  41281  dih1  41288  lclkrlem1  41508  lclkr  41535  mapd1o  41650  mapdin  41664  hdmapfnN  41831  hgmapfnN  41890  lcmineqlem10  42039  sticksstones9  42155  sn-iotalem  42260  readvrec2  42391  readvrec  42392  repncan2  42412  sn-inelr  42497  elrfirn  42706  ismrcd1  42709  istopclsd  42711  rabren3dioph  42826  jm2.17b  42973  jm2.22  43007  jm2.23  43008  ttac  43048  pw2f1ocnv  43049  dnnumch1  43056  hbtlem5  43140  mncn0  43151  aaitgo  43174  rngunsnply  43181  unielss  43230  onexlimgt  43255  cantnfresb  43337  dflim5  43342  naddwordnexlem4  43414  safesnsupfiss  43428  safesnsupfidom1o  43430  safesnsupfilb  43431  ensucne0OLD  43543  clcnvlem  43636  relexp01min  43726  ntrf  44136  ssrecnpr  44327  seff  44328  sblpnf  44329  nzss  44336  dvconstbi  44353  ipo0  44468  ifr0  44469  addrfn  44491  subrfn  44492  mulvfn  44493  wfaxrep  45011  refsum2cnlem1  45042  rn1st  45280  ellimciota  45629  dvmptconst  45930  dvmptidg  45932  dvmulcncf  45940  dvdivcncf  45942  stoweidlem26  46041  stoweidlem50  46065  stoweidlem57  46072  aiotaval  47107  ndfatafv2nrn  47233  afv2ndefb  47236  funop1  47295  fun2dmnopgexmpl  47296  2ffzoeq  47339  m1modne  47350  iccpartiltu  47409  iccpartigtl  47410  zofldiv2ALTV  47649  evenprm2  47701  9fppr8  47724  stgoldbwt  47763  nnsum3primesle9  47781  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  tgblthelfgott  47802  dfclnbgr6  47842  cycl3grtri  47914  grtrimap  47915  stgredgel  47924  stgr1  47928  isubgr3stgrlem2  47934  isubgr3stgrlem3  47935  usgrexmpl2trifr  47996  2ltceilhalf  48015  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg5nbgr3star  48037  gpg3kgrtriex  48045  uspgrex  48066  0mgm  48082  nnsgrpmgm  48092  rngchomffvalALTV  48194  rhmsubcALTVlem1  48197  funcringcsetcALTV2lem4  48209  funcringcsetclem4ALTV  48232  srhmsubcALTV  48241  mapsnop  48260  zlmodzxzldeplem4  48420  zofldiv2  48452  fdivval  48460  nnlog2ge0lt1  48487  dig1  48529  itcoval2  48585  itcoval3  48586  mosn  48732  mo0  48733  mof02  48748  mofeu  48757  f102g  48761  f1mo  48762  tposres0  48777  f1omo  48792  intubeu  48873  unilbeu  48874  swapf2fn  48974  swapf1f1o  48981  swapf2f1o  48982  swapf2f1oaALT  48984  fucof1  49017  fucofn2  49019  fucofn22  49035  functhinclem1  49093  fullthinc  49099  thincciso  49102  indthinc  49109  indthincALT  49110  functermc  49140