Theorem mpbiri 261

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 260	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  elimh  1099  spei  2423  nfald2  2474  nfabd2  2945  raleleq  3331  ceqsexv2d  3499  dedhb  3660  csbie2df  4400  ssdifeq0  4441  dedth  4540  pwidgOLD  4577  snidg  4620  rexreusng  4639  exsnrex  4640  ifpr  4653  rmosn  4679  rabrsn  4684  prid1g  4720  tpid1g  4729  tpid2g  4731  tpid3g  4732  pwpw0  4773  sssn  4786  elpreqpr  4826  unimax  4904  intmin3  4935  eqbrtrdi  5143  al0ssb  5261  vneqv  5269  rabelpw  5297  intabs  5309  difelpw  5314  0inp0  5319  axpr  5388  intidg  5424  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  euotd  5485  elopab  5500  elvvuni  5727  posn  5736  frsn  5738  eqrelriv  5764  relsnb  5779  relopabiALT  5800  opabid2  5805  ididg  5830  iss  6026  cnveq0b  6191  dfpo2  6299  ord0eln0  6419  sucidg  6446  nsuceq0  6448  funopg  6574  fn0  6670  f00  6764  f0bi  6765  f10d  6859  f1o00  6860  fo00  6861  brprcneu  6875  brprcneuALT  6876  dffn5  6943  fsn  7136  funop  7153  funsndifnop  7155  fnsnbOLD  7171  eufnfv  7235  f1ounsn  7280  f1eqcocnv  7309  nfriotadw  7385  nfriotad  7388  riotaprop  7404  oprabidw  7451  oprabid  7452  elrnmpo  7556  ov6g  7584  ovelrn  7597  caovmo  7658  offn  7706  caofinvl  7725  fr3nr  7786  onprc  7792  ordeleqon  7796  onint0  7805  0elsuc  7846  onuninsuci  7851  orduninsuc  7854  ordzsl  7856  onzsl  7857  tfinds  7871  limomss  7882  limom  7893  peano5  7905  xpexr  7930  eqop2  8044  opreuopreu  8046  1stconst  8111  2ndconst  8112  frxp2  8161  frxp3  8168  funsssuppss  8208  dftpos3  8262  dftpos4  8263  oawordeulem  8563  omwordi  8580  nnmwordi  8645  riiner  8812  ecopover  8843  map0g  8913  mapsnd  8915  elixpsn  8966  en0  9046  en0ALT  9047  en0r  9048  en1  9052  snfi  9072  fiprc  9073  sbthlem2  9108  sbthlem4  9110  sbthlem5  9111  0domg  9124  findcard  9180  findcard2  9181  nneneq  9222  sdom1  9242  1sdom2dom  9246  fineqvlem  9258  nfielex  9266  enp1i  9271  elfiun  9423  marypha1lem  9426  oicl  9524  oif  9525  oion  9531  hartogslem1  9537  hartogs  9539  wemapso2  9548  card2on  9549  0wdom  9565  brwdom2  9568  elirrv  9592  inf3lem6  9635  cantnflem3  9693  cantnflem4  9694  wemapwe  9699  cnfcom  9702  ssttrcl  9717  ttrclselem2  9728  tctr  9740  r1tr  9784  r1rankidb  9813  r1pw  9860  elhf2  9911  scottex  9934  scottexOLD  9935  scott0b  9938  scott0OLD  9939  bnd2  9957  eldju2ndl  10006  tskwe  10032  oncard  10042  cardlim  10054  harsdom  10077  en2eleq  10088  dfac8alem  10109  dfac8b  10111  cardaleph  10169  iunfictbso  10194  infmap2  10296  ackbij1lem18  10315  cff  10326  cfsuc  10336  cff1  10337  cflim2  10342  cfss  10344  sdom2en01  10381  infpssrlem4  10385  fin23lem7  10395  fin23lem11  10396  isfin2-2  10398  fin23lem26  10404  fin23lem19  10415  fin23lem17  10417  isf34lem2  10452  isf34lem4  10456  fin1a2lem6  10484  fin1a2lem10  10488  fin1a2lem12  10490  itunifn  10496  hsmexlem1  10505  axcc2lem  10515  dcomex  10526  axdc3lem4  10532  ondomon  10648  konigthlem  10654  pwcfsdom  10669  cfpwsdom  10670  axpowndlem3  10685  canth4  10733  canthnumlem  10734  canthwelem  10736  canthwe  10737  canthp1lem2  10739  pwfseqlem4  10748  pwfseqlem5  10749  gchaleph  10757  gch2  10761  winainflem  10779  0tsk  10841  rankcf  10863  tskcard  10867  gruina  10904  grutsk  10908  tskmid  10926  indpi  10993  nqereu  11015  mulcanenq  11046  recmulnq  11050  archnq  11066  ltsopr  11118  1ne0sr  11182  0idsr  11183  00sr  11185  leid  11407  lelttric  11418  divcan3  12001  divid  12005  div0  12006  lemul1a  12172  nn1suc  12358  nn0n0n1ge2b  12676  xnn0xr  12685  xnn0nemnf  12691  0nn0m1nnn0  12754  nn0lt10b  12762  nn0ind-raph  12800  elnn1uz2  13053  indstr2  13055  uzsupss  13068  rpnnen1lem4  13109  rpnnen1lem5  13110  xrnemnf  13247  xrnepnf  13248  mnfltxr  13257  xnn0n0n1ge2b  13262  xnn0ge0  13264  xrlttri  13269  xrlttr  13270  xrleid  13281  qbtwnxr  13331  xmullem2  13396  xlemul1a  13419  xrub  13443  reltxrnmnf  13474  ixxun  13493  xnn0xrge0  13638  fztpval  13721  fseq1p1m1  13733  elfznelfzob  13910  ltweuz  14105  fzfi  14116  fsuppmapnn0fiubex  14136  ser0f  14199  0exp  14241  faclbnd4lem1  14438  bcn1  14458  hashnemnf  14489  hashv01gt1  14490  hashsnle1  14563  hashgt12el2  14569  hashpw  14582  hashf1  14603  fz1isolem  14607  hash2prb  14618  hash3tpb  14641  0wrd0  14686  wrdlen1  14700  ccatvalfn  14727  eqs1  14761  wrdl1exs1  14762  swrdlen  14796  swrdwrdsymb  14813  swrdspsleq  14816  cats1un  14871  wrdind  14872  wrd2ind  14873  swrdccatin1  14875  repswsymballbi  14932  cshw1  14974  scshwfzeqfzo  14978  wrdl2exs2  15098  trclfvcotr  15163  relexp1g  15180  relexp0rel  15191  relexprelg  15192  relexpreld  15194  sgnmulsgn  15263  sqrt0  15409  sqrtsq  15437  mptfzshft  15945  prodf1f  16062  egt2lt3  16375  0dvds  16447  nn0onn  16551  nn0o  16554  divalgmod  16577  flodddiv4  16586  bitsp1o  16604  gcddvds  16674  bezout  16717  lcmdvds  16784  rpdvds  16836  1nprm  16855  prmind2  16861  dvdszzq  16898  nnoddn2prmb  16992  pcpre1  17021  vdwapf  17151  vdwapid1  17154  ram0  17201  ramz  17204  prmolefac  17225  cshws0  17280  prmlem0  17284  strle1  17337  restsspw  17603  prdsdsfn  17637  imasdsfn  17687  imasaddfnlem  17701  imasvscafn  17710  xpsfrnel  17735  isacs1i  17832  cidfn  17854  fnhomeqhomf  17866  comffn  17880  isoval  17941  sscres  17999  cofucl  18064  idffth  18111  ressffth  18116  cat1lem  18272  catcoppccl  18293  estrchomfn  18310  funcestrcsetclem4  18318  funcestrcsetclem7  18321  equivestrcsetc  18327  funcsetcestrclem4  18333  funcsetcestrclem7  18336  1stfcl  18372  2ndfcl  18373  prfcl  18378  evlfcl  18397  curf1cl  18403  curfcl  18407  hofcl  18434  yonedainv  18456  pospo  18518  lubfun  18525  glbfun  18538  joindmss  18552  meetdmss  18566  ipopos  18711  acsficl2d  18727  dirref  18776  mgmidcl  18847  mgmlrid  18848  ielefmnd  19084  smndex1basss  19105  smndex1n0mnd  19112  degenmgm  19138  degenmgm2  19141  cntzssv  19543  idresperm  19601  symgvalstruct  19612  pmtrfmvdn0  19677  symggen  19685  psgnunilem1  19708  psgnprfval  19736  slwpgp  19828  frgpmhm  19980  frgpuptinv  19986  frgpup3lem  19992  gsumzoppg  20159  gsumcom2  20190  c0snmhm  20694  srhmsubc  20933  rhmsubclem1  20938  rrgsupp  20954  abv0  21081  zrhrhm  21818  psgnodpmr  21897  frlmphllem  22087  ellspd  22109  psrvscafval  22257  psrridm  22271  ltbwe  22354  psrbag0  22372  psrbagsn  22373  subrgascl  22376  psdmul  22488  mattpostpos  22770  mavmul0  22868  mavmul0g  22869  mdet0f1o  22909  m1detdiag  22913  m2detleiblem5  22941  m2detleiblem6  22942  m2detleiblem3  22945  m2detleiblem4  22946  maducoeval2  22956  d1mat2pmat  23058  chpmat1dlem  23154  chpmat1d  23155  baspartn  23273  eltg3  23281  topnex  23315  fctop  23323  cctop  23325  discld  23408  mretopd  23411  neipeltop  23448  neitr  23499  restcls  23500  ordtbaslem  23507  ordtuni  23509  idcn  23576  cnrmi  23679  cmpsublem  23718  cmpsub  23719  tgcmp  23720  uncmp  23722  hauscmplem  23725  cmpfi  23727  bwth  23729  1stcrestlem  23771  disllycmp  23818  dis1stc  23819  refref  23833  kgeni  23857  1stckgenlem  23873  kqffn  24045  snfil  24184  filconn  24203  cfinfil  24213  ufileu  24239  filufint  24240  fixufil  24242  cfinufil  24248  ufilen  24250  fin1aufil  24252  fmf  24265  rnelfm  24273  flimclslem  24304  hauspwpwf1  24307  supnfcls  24340  flimfnfcls  24348  fclscmp  24350  alexsubALTlem2  24368  alexsubALTlem3  24369  alexsubALT  24371  ptcmplem1  24372  cnextrel  24383  tsmsfbas  24448  ustref  24539  trust  24549  restutop  24557  isusp  24581  xmet0  24662  imasdsf1olem  24693  blfvalps  24703  blfps  24726  blf  24727  restmetu  24890  dscmet  24892  isngp2  24917  nm0  24949  nrginvrcn  25012  nmoix  25049  qdensere  25089  iccconn  25151  iccpnfcnv  25266  xrhmeo  25268  lebnumlem3  25285  metsscmetcld  25637  bcthlem5  25650  csschl  25698  rrxmfval  25728  minveclem3b  25750  cniccbdd  25783  ovolicc2lem4  25842  iunmbl  25875  ioorinv  25898  ioorcl  25899  i1f1lem  26011  limcvallem  26192  ellimc2  26198  limccnp  26212  limccnp2  26213  limcco  26214  perfdvf  26224  recnprss  26225  fncpn  26254  dvcmulf  26266  c1lip1  26318  lhop2  26336  q1pcl  26476  r1pdeglt  26479  ply1remlem  26484  plyssc  26519  ulm0  26719  cxpeq0  27007  cxplea  27025  cxplogb  27115  asinlem  27197  isppw2  27443  muval2  27462  dchrfi  27583  dchrpt  27595  bposlem6  27617  lgsdir2lem2  27654  lgsqr  27679  gausslemma2dlem4  27697  2lgslem2  27723  2lgslem3  27732  2lgs  27735  2sqlem7  27752  2sqlem11  27757  chtppilim  27803  nosgnn0i  28017  nolesgn2ores  28030  nogesgn1ores  28032  nosepnelem  28037  nosepdmlem  28041  nosupbnd1lem3  28068  nosupbnd1lem5  28070  nosupbnd2lem1  28073  noinfbnd1lem3  28083  noinfbnd1lem5  28085  noinfbnd2lem1  28088  oldval  28221  made0  28250  lrrecpo  28328  pncan2s  28461  divscan3d  28623  abssor  28633  om2noseqfo  28685  noseqrdglem  28692  noseqrdgfn  28693  noseqrdg0  28694  onsfi  28743  nohalf  28811  expsne0  28823  pw2divscan3d  28828  tgldimor  28966  tgcgr4  28995  tglnfn  29011  tglnunirn  29012  mirne  29140  mircinv  29141  perpln1  29186  perpln2  29187  tgplnfn  29254  lmiisolem  29302  prlngmid2  29440  xmstrkgc  29464  axcgrtr  29494  axsegconlem9  29504  axlowdimlem5  29525  axlowdimlem17  29537  axlowdim1  29538  uhgr0e  29650  edglnl  29722  uhgr0edgfi  29822  issubgr2  29854  subgrprop2  29856  egrsubgr  29859  0grsubgr  29860  0uhgrsubgr  29861  uhgrsubgrself  29862  nbgr1vtx  29940  nbgrssovtx  29943  nb3grprlem1  29962  uvtx01vtx  29979  cplgr1vlem  30011  cplgr1v  30012  usgrexilem  30022  wlkcomp  30212  wlk1walk  30220  wlkp1lem5  30257  pthhashvtx  30316  uhgrwkspthlem1  30340  pthdlem1  30353  clwlkcomp  30367  lfgrn1cycl  30395  uspgrn2crct  30398  wwlksn0s  30451  usgrwwlks2on  30548  umgrwwlks2on  30549  clwwlkn  30618  clwwlkn1  30633  0ewlk  30706  1ewlk  30707  0spth  30718  upgr1wlkdlem2  30738  wlk2v2e  30759  upgr3v3e3cycl  30782  upgr4cycl4dv4e  30787  eupth0  30816  frgr0v  30864  frgr1v  30873  1vwmgr  30878  ex-opab  31034  grpoinvf  31135  nvmid  31262  nmlnoubi  31399  hiidrcl  31698  hsn0elch  31851  shjshseli  32096  cmbr4i  32204  dfiop2  32356  kbpj  32559  nmopun  32617  adjeq0  32694  kbass2  32720  pjssdif1i  32778  pjinvari  32794  pjcmul2i  32805  pj3i  32811  stge1i  32841  stle0i  32842  sumdmdlem2  33022  dmdbr6ati  33026  dmdbr7ati  33027  rabsnel  33139  unidifsnel  33174  unidifsnne  33175  disjdifprg  33212  ofoprabco  33301  padct  33353  fpwrelmapffslem  33367  nn0mnfxrd  33386  xrlelttric  33387  xnn0gt0  33404  iundisj2cnt  33434  f1ocnt  33435  fz1nnct  33436  fz1nntr  33437  hashxpe  33442  nn0min  33455  sgnmulsgp  33466  wrdt2ind  33559  xrge0tsmsbi  33678  opprabs  34049  rtelextdg2lem  34401  2sqr3minply  34455  locfinref  34516  dispcmp  34534  zartopn  34550  zarcmplem  34556  pstmxmet  34572  xrge0iifcnv  34608  xrge0iif1  34613  qqhre  34695  esumcl  34705  esumpr2  34742  esumpinfval  34748  esumpcvgval  34753  ofcfn  34775  pwsiga  34805  prsiga  34806  sigainb  34812  ldgenpisyslem1  34839  measiuns  34893  relfae  34923  pmeasmono  34999  sitgf  35022  eulerpartgbij  35047  signswch  35233  signslema  35234  signstlen  35239  signstfvn  35241  circlevma  35314  bnj216  35406  bnj151  35550  bnj517  35558  bnj970  35620  bnj1145  35666  bnj1498  35734  r1omhfb  35783  rankscottu  35800  fineqvrep  35831  fineqvac  35833  fineqvnttrclselem1  35838  fineqvnttrclselem2  35839  fineqvnttrclse  35841  fineqvinfep  35842  r1omhfbregs  35854  kard0b  35876  rankkardu  35888  wevgblacfn  35951  vonf1osev  35952  acycgr0v  35982  prclisacycgr  35985  umgracycusgr  35988  cusgracyclt3v  35990  subfacp1lem5  36018  erdszelem8  36032  kur14lem1  36040  indispconn  36068  cvmsss2  36108  satfvsuclem2  36194  satfrel  36201  satfrnmapom  36204  satfv0fun  36205  satf00  36208  satf0suclem  36209  fmlasuc0  36218  msubrn  36363  onprcr  36531  dfon2lem7  36626  brbigcup  36735  elsingles  36755  fnimage  36766  funpartlem  36781  dfrdg4  36790  imagesset  36792  altopthsn  36801  elaltxp  36815  ellines  36992  linethru  36993  rankeq1o  37007  hfninf  37010  nn0prpwlem  37185  fneref  37213  neibastop2lem  37223  limsucncmpi  37308  tz9.1tco  37346  bj-exlimmpbir  37901  curryset  37934  bj-snglex  37961  bj-axnul  38063  bj-restpw  38088  bj-inftyexpidisj  38207  topdifinffinlem  38346  relowlssretop  38362  rdgeqoa  38369  finxpreclem6  38395  fvineqsneq  38411  pibt2  38416  poimirlem23  38637  poimirlem29  38643  poimirlem31  38645  volsupnfl  38659  cnambfre  38662  dvasin  38698  dvacos  38699  sdclem2  38752  sstotbnd2  38784  ssbnd  38798  ismgmOLD  38860  grpokerinj  38903  rngomndo  38945  isdrngo1  38966  ac6s6  39180  iss2  39352  relecxrn  39415  sucmapsuc  39497  cosselrels  39583  cnvelrels  39584  brssrid  39590  brcnvssrid  39595  dfdisjs5  39805  eldisjs5  39831  eldisjsim3  39945  mpets2  39963  pets  39974  prtlem12  40000  riotasv2d  40090  lkrscss  40231  islshpkrN  40253  isline  40872  ispointN  40875  0psubN  40882  linepsubN  40885  atpsubN  40886  cdlemk36  42046  diafn  42167  dibfna  42287  dibvalrel  42296  dicvalrelN  42318  diclspsn  42327  dihvalrel  42412  dih1  42419  lclkrlem1  42639  lclkr  42666  mapd1o  42781  mapdin  42795  hdmapfnN  42962  hgmapfnN  43021  lcmineqlem10  43164  sticksstones9  43280  sn-iotalem  43351  readvrec2  43488  readvrec  43489  repncan2  43509  elrfirn  43782  ismrcd1  43785  istopclsd  43787  rabren3dioph  43898  jm2.17b  44044  jm2.22  44078  jm2.23  44079  ttac  44119  pw2f1ocnv  44120  dnnumch1  44127  hbtlem5  44206  mncn0  44217  aaitgo  44240  rngunsnply  44247  unielss  44296  onexlimgt  44321  cantnfresb  44402  dflim5  44407  naddwordnexlem4  44479  safesnsupfiss  44492  safesnsupfidom1o  44494  safesnsupfilb  44495  ensucne0OLD  44607  clcnvlem  44699  relexp01min  44789  ntrf  45199  ssrecnpr  45368  seff  45369  sblpnf  45370  nzss  45377  dvconstbi  45394  ipo0  45508  ifr0  45509  addrfn  45530  subrfn  45531  mulvfn  45532  wfaxrep  46060  refsum2cnlem1  46130  rn1st  46361  ellimciota  46702  dvmptconst  47001  dvmptidg  47003  dvmulcncf  47011  dvdivcncf  47013  stoweidlem26  47112  stoweidlem50  47136  stoweidlem57  47143  tannpoly  48016  tmachlem-agreefin  48034  aiotaval  48241  ndfatafv2nrn  48367  afv2ndefb  48370  funop1  48429  fun2dmnopgexmpl  48430  2ffzoeq  48474  2ltceilhalf  48478  m1modne  48500  iccpartiltu  48580  iccpartigtl  48581  zofldiv2ALTV  48836  evenprm2  48888  9fppr8  48911  stgoldbwt  48950  nnsum3primesle9  48968  nnsum4primeseven  48974  nnsum4primesevenALTV  48975  tgblthelfgott  48989  dfclnbgr6  49030  cycl3grtri  49121  grtrimap  49122  stgredgel  49131  stgr1  49135  isubgr3stgrlem2  49141  isubgr3stgrlem3  49142  usgrexmpl2trifr  49211  gpg5nbgrvtx13starlem1  49245  gpg5nbgrvtx13starlem2  49246  gpg5nbgrvtx13starlem3  49247  gpg5nbgr3star  49255  gpg3kgrtriex  49263  uspgrex  49324  0mgm  49339  nnsgrpmgm  49349  rngchomffvalALTV  49451  rhmsubcALTVlem1  49454  funcringcsetcALTV2lem4  49466  funcringcsetclem4ALTV  49489  srhmsubcALTV  49498  mapsnop  49532  zlmodzxzldeplem4  49691  zofldiv2  49719  fdivval  49727  nnlog2ge0lt1  49754  dig1  49796  itcoval2  49852  itcoval3  49853  mosn  49999  mo0  50000  mof02  50025  mofeu  50034  f102g  50038  f1mo  50039  tposres0  50061  f1omo  50077  f1omoOLD  50078  resipos  50159  intubeu  50168  unilbeu  50169  sectfn  50213  nelsubclem  50251  idfu1stf1o  50283  imaidfu  50294  oppfvallem  50319  funcoppc3  50331  idfth  50342  idsubc  50344  uptposlem  50381  swapf2fn  50452  swapf1f1o  50459  swapf2f1o  50460  swapf2f1oaALT  50462  fucof1  50506  fucofn2  50508  fucofn22  50524  reldmprcof1  50565  reldmprcof2  50566  fucoppcid  50592  fucoppc  50594  functhinclem1  50628  fullthinc  50634  thincciso  50637  indcthing  50644  indthinc  50646  indthincALT  50647  functermc  50692  discsntermlem  50754  reldmlan2  50801  reldmran2  50802  rellan  50807  relran  50808  termolmd  50854  veronesev1lem  51049  veronesev2lem  51050  veronesev3lem  51051  veronesev4lem  51052  veronesev5lem  51053  veronesev6lem  51054  veronesevrowd  51055  veronesematrowd  51057