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  2402  nfald2  2453  nfabd2  2935  raleleq  3350  raleleqOLD  3351  ceqsexv2d  3545  dedhb  3725  sbceqalOLD  3871  csbie2df  4466  ssdifeq0  4510  r19.2zb  4519  dedth  4606  pwidg  4642  snidg  4682  rexreusng  4703  exsnrex  4704  ifpr  4716  rmosn  4744  rabrsn  4749  prid1g  4785  tpid1g  4794  tpid2g  4796  tpid3g  4797  pwpw0  4838  sssn  4851  elpreqpr  4891  unimax  4968  intmin3  5000  eqbrtrdi  5205  al0ssb  5326  rabelpw  5354  intabs  5367  difelpw  5372  0inp0  5377  intidg  5477  copsexgw  5510  copsexg  5511  euotd  5532  elopab  5546  elvvuni  5776  posn  5785  frsn  5787  eqrelriv  5813  relsnb  5826  relopabiALT  5847  opabid2  5852  ididg  5878  iss  6064  dfpo2  6327  ord0eln0  6450  sucidg  6476  nsuceq0  6478  funopg  6612  fn0  6711  f00  6803  f0bi  6804  f10d  6896  f1o00  6897  fo00  6898  brprcneu  6910  brprcneuALT  6911  dffn5  6980  fsn  7169  funop  7183  funsndifnop  7185  fnsnb  7200  eufnfv  7266  f1eqcocnv  7337  nfriotadw  7412  nfriotad  7416  riotaprop  7432  oprabidw  7479  oprabid  7480  elrnmpo  7586  ov6g  7614  ovelrn  7626  caovmo  7687  offn  7727  caofinvl  7745  fr3nr  7807  onprc  7813  ordeleqon  7817  onint0  7827  0elsuc  7871  onuninsuci  7877  orduninsuc  7880  ordzsl  7882  onzsl  7883  tfinds  7897  limomss  7908  limom  7919  peano5  7932  peano5OLD  7933  xpexr  7958  eqop2  8073  opreuopreu  8075  1stconst  8141  2ndconst  8142  frxp2  8185  frxp3  8192  funsssuppss  8231  dftpos3  8285  dftpos4  8286  wfrlem4OLD  8368  wfrlem14OLD  8378  oawordeulem  8610  omwordi  8627  nnmwordi  8691  riiner  8848  ecopover  8879  map0g  8942  mapsnd  8944  elixpsn  8995  en0  9078  en0OLD  9079  en0ALT  9080  en0r  9081  en1  9086  en1OLD  9087  snfi  9109  fiprc  9111  sbthlem2  9150  sbthlem4  9152  sbthlem5  9153  0domg  9166  findcard  9229  findcard2  9230  nneneq  9272  nneneqOLD  9284  sdom1  9305  sdom1OLD  9306  1sdom2dom  9310  fineqvlem  9325  nfielex  9335  enp1i  9341  elfiun  9499  marypha1lem  9502  oicl  9598  oif  9599  oion  9605  hartogslem1  9611  hartogs  9613  wemapso2  9622  card2on  9623  0wdom  9639  brwdom2  9642  inf3lem6  9702  cantnflem3  9760  cantnflem4  9761  wemapwe  9766  cnfcom  9769  ssttrcl  9784  ttrclselem2  9795  tctr  9809  r1tr  9845  r1rankidb  9873  r1pw  9914  scottex  9954  scott0  9955  bnd2  9962  eldju2ndl  9993  tskwe  10019  oncard  10029  cardlim  10041  harsdom  10064  en2eleq  10077  dfac8alem  10098  cardaleph  10158  iunfictbso  10183  infmap2  10286  ackbij1lem18  10305  cff  10317  cfsuc  10326  cff1  10327  cflim2  10332  cfss  10334  sdom2en01  10371  infpssrlem4  10375  fin23lem7  10385  fin23lem11  10386  isfin2-2  10388  fin23lem26  10394  fin23lem19  10405  fin23lem17  10407  isf34lem2  10442  isf34lem4  10446  fin1a2lem6  10474  fin1a2lem10  10478  fin1a2lem12  10480  itunifn  10486  hsmexlem1  10495  axcc2lem  10505  dcomex  10516  axdc3lem4  10522  ondomon  10632  konigthlem  10637  pwcfsdom  10652  cfpwsdom  10653  axpowndlem3  10668  canth4  10716  canthnumlem  10717  canthwelem  10719  canthwe  10720  canthp1lem2  10722  pwfseqlem4  10731  pwfseqlem5  10732  gchaleph  10740  gch2  10744  winainflem  10762  0tsk  10824  rankcf  10846  tskcard  10850  gruina  10887  grutsk  10891  tskmid  10909  indpi  10976  nqereu  10998  mulcanenq  11029  recmulnq  11033  archnq  11049  ltsopr  11101  1ne0sr  11165  0idsr  11166  00sr  11168  leid  11386  lelttric  11397  divcan3  11975  divid  11980  div0  11982  lemul1a  12148  nn1suc  12315  nn0n0n1ge2b  12621  xnn0xr  12630  xnn0nemnf  12636  nn0lt10b  12705  nn0ind-raph  12743  elnn1uz2  12990  indstr2  12992  uzsupss  13005  rpnnen1lem4  13045  rpnnen1lem5  13046  xrnemnf  13180  xrnepnf  13181  mnfltxr  13190  xnn0n0n1ge2b  13194  xnn0ge0  13196  xrlttri  13201  xrlttr  13202  xrleid  13213  qbtwnxr  13262  xmullem2  13327  xlemul1a  13350  xrub  13374  reltxrnmnf  13404  ixxun  13423  xnn0xrge0  13566  fztpval  13646  fseq1p1m1  13658  elfznelfzob  13823  ltweuz  14012  fzfi  14023  fsuppmapnn0fiubex  14043  ser0f  14106  0exp  14148  faclbnd4lem1  14342  bcn1  14362  hashnemnf  14393  hashv01gt1  14394  hashsnle1  14466  hashgt12el2  14472  hashpw  14485  hashf1  14506  fz1isolem  14510  hash2prb  14521  hash3tpb  14544  0wrd0  14588  wrdlen1  14602  ccatvalfn  14629  eqs1  14660  wrdl1exs1  14661  swrdlen  14695  swrdwrdsymb  14710  swrdspsleq  14713  cats1un  14769  wrdind  14770  wrd2ind  14771  swrdccatin1  14773  repswsymballbi  14828  cshw1  14870  scshwfzeqfzo  14875  wrdl2exs2  14995  trclfvcotr  15058  relexp1g  15075  relexp0rel  15086  relexprelg  15087  relexpreld  15089  sqrt0  15290  sqrtsq  15318  mptfzshft  15826  prodf1f  15940  egt2lt3  16254  0dvds  16325  nn0onn  16428  nn0o  16431  divalgmod  16454  flodddiv4  16461  bitsp1o  16479  gcddvds  16549  bezout  16590  lcmdvds  16655  rpdvds  16707  1nprm  16726  prmind2  16732  dvdszzq  16768  nnoddn2prmb  16860  pcpre1  16889  vdwapf  17019  vdwapid1  17022  ram0  17069  ramz  17072  prmolefac  17093  cshws0  17149  prmlem0  17153  strle1  17205  restsspw  17491  prdsdsfn  17525  imasdsfn  17574  imasaddfnlem  17588  imasvscafn  17597  xpsfrnel  17622  isacs1i  17715  cidfn  17737  fnhomeqhomf  17749  comffn  17763  isoval  17826  sscres  17884  cofucl  17952  idffth  18000  ressffth  18005  cat1lem  18163  catcoppccl  18184  catcoppcclOLD  18185  estrchomfn  18203  funcestrcsetclem4  18212  funcestrcsetclem7  18215  equivestrcsetc  18221  funcsetcestrclem4  18227  funcsetcestrclem7  18230  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  yonedainv  18351  pospo  18415  lubfun  18422  glbfun  18435  joindmss  18449  meetdmss  18463  ipopos  18606  acsficl2d  18622  dirref  18671  mgmidcl  18704  mgmlrid  18705  ielefmnd  18922  smndex1basss  18940  smndex1n0mnd  18947  cntzssv  19368  idresperm  19427  symgvalstruct  19438  symgvalstructOLD  19439  pmtrfmvdn0  19504  symggen  19512  psgnunilem1  19535  psgnprfval  19563  slwpgp  19655  frgpmhm  19807  frgpuptinv  19813  frgpup3lem  19819  gsumzoppg  19986  gsumcom2  20017  c0snmhm  20489  srhmsubc  20702  rhmsubclem1  20707  rrgsupp  20723  abv0  20846  zrhrhm  21545  psgnodpmr  21631  frlmphllem  21823  ellspd  21845  psrvscafval  21991  psrridm  22006  ltbwe  22085  psrbag0  22109  psrbagsn  22110  subrgascl  22113  psdmul  22193  mattpostpos  22481  mavmul0  22579  mavmul0g  22580  mdet0f1o  22620  m1detdiag  22624  m2detleiblem5  22652  m2detleiblem6  22653  m2detleiblem3  22656  m2detleiblem4  22657  maducoeval2  22667  d1mat2pmat  22766  chpmat1dlem  22862  chpmat1d  22863  baspartn  22982  eltg3  22990  topnex  23024  fctop  23032  cctop  23034  discld  23118  mretopd  23121  neipeltop  23158  neitr  23209  restcls  23210  ordtbaslem  23217  ordtuni  23219  idcn  23286  cnrmi  23389  cmpsublem  23428  cmpsub  23429  tgcmp  23430  uncmp  23432  hauscmplem  23435  cmpfi  23437  bwth  23439  1stcrestlem  23481  disllycmp  23527  dis1stc  23528  refref  23542  kgeni  23566  1stckgenlem  23582  kqffn  23754  snfil  23893  filconn  23912  cfinfil  23922  ufileu  23948  filufint  23949  fixufil  23951  cfinufil  23957  ufilen  23959  fin1aufil  23961  fmf  23974  rnelfm  23982  flimclslem  24013  hauspwpwf1  24016  supnfcls  24049  flimfnfcls  24057  fclscmp  24059  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem1  24081  cnextrel  24092  tsmsfbas  24157  ustref  24248  trust  24259  restutop  24267  isusp  24291  xmet0  24373  imasdsf1olem  24404  blfvalps  24414  blfps  24437  blf  24438  restmetu  24604  dscmet  24606  isngp2  24631  nm0  24663  nrginvrcn  24734  nmoix  24771  qdensere  24811  iccconn  24871  iccpnfcnv  24994  xrhmeo  24996  lebnumlem3  25014  metsscmetcld  25368  bcthlem5  25381  csschl  25429  rrxmfval  25459  minveclem3b  25481  cniccbdd  25515  ovolicc2lem4  25574  iunmbl  25607  ioorinv  25630  ioorcl  25631  i1f1lem  25743  limcvallem  25926  ellimc2  25932  limccnp  25946  limccnp2  25947  limcco  25948  perfdvf  25958  recnprss  25959  fncpn  25989  dvcmulf  26002  c1lip1  26056  lhop2  26074  q1pcl  26216  r1pdeglt  26219  ply1remlem  26224  plyssc  26259  ulm0  26452  cxpeq0  26738  cxplea  26756  cxplogb  26847  asinlem  26929  isppw2  27176  muval2  27195  dchrfi  27317  dchrpt  27329  bposlem6  27351  lgsdir2lem2  27388  lgsqr  27413  gausslemma2dlem4  27431  2lgslem2  27457  2lgslem3  27466  2lgs  27469  2sqlem7  27486  2sqlem11  27491  chtppilim  27537  nosgnn0i  27722  nolesgn2ores  27735  nogesgn1ores  27737  nosepnelem  27742  nosepdmlem  27746  nosupbnd1lem3  27773  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  oldval  27911  made0  27930  lrrecpo  27992  pncan2s  28122  divscan3d  28278  abssor  28288  om2noseqfo  28322  noseqrdglem  28329  noseqrdgfn  28330  noseqrdg0  28331  n0scut  28356  nohalf  28425  expsne0  28432  tgldimor  28528  tgcgr4  28557  tglnfn  28573  tglnunirn  28574  mirne  28693  mircinv  28694  perpln1  28736  perpln2  28737  lmiisolem  28822  xmstrkgc  28918  axcgrtr  28948  axsegconlem9  28958  axlowdimlem5  28979  axlowdimlem17  28991  axlowdim1  28992  uhgr0e  29106  edglnl  29178  uhgr0edgfi  29275  issubgr2  29307  subgrprop2  29309  egrsubgr  29312  0grsubgr  29313  0uhgrsubgr  29314  uhgrsubgrself  29315  nbgr1vtx  29393  nbgrssovtx  29396  nb3grprlem1  29415  uvtx01vtx  29432  cplgr1vlem  29464  cplgr1v  29465  usgrexilem  29475  wlkcomp  29667  wlk1walk  29675  wlkp1lem5  29713  uhgrwkspthlem1  29789  pthdlem1  29802  clwlkcomp  29815  lfgrn1cycl  29838  uspgrn2crct  29841  wwlksn0s  29894  umgrwwlks2on  29990  clwwlkn  30058  clwwlkn1  30073  0ewlk  30146  1ewlk  30147  0spth  30158  upgr1wlkdlem2  30178  wlk2v2e  30189  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth0  30246  frgr0v  30294  frgr1v  30303  1vwmgr  30308  ex-opab  30464  grpoinvf  30564  nvmid  30691  nmlnoubi  30828  hiidrcl  31127  hsn0elch  31280  shjshseli  31525  cmbr4i  31633  dfiop2  31785  kbpj  31988  nmopun  32046  adjeq0  32123  kbass2  32149  pjssdif1i  32207  pjinvari  32223  pjcmul2i  32234  pj3i  32240  stge1i  32270  stle0i  32271  sumdmdlem2  32451  dmdbr6ati  32455  dmdbr7ati  32456  rabsnel  32528  unidifsnel  32563  unidifsnne  32564  disjdifprg  32597  ofoprabco  32682  padct  32733  fpwrelmapffslem  32746  xrlelttric  32759  xnn0gt0  32776  iundisj2cnt  32804  f1ocnt  32807  fz1nnct  32808  fz1nntr  32809  hashxpe  32814  nn0min  32824  wrdt2ind  32920  xrge0tsmsbi  33042  opprabs  33475  rtelextdg2lem  33717  2sqr3minply  33738  locfinref  33787  dispcmp  33805  zartopn  33821  zarcmplem  33827  pstmxmet  33843  xrge0iifcnv  33879  xrge0iif1  33884  qqhre  33966  esumcl  33994  esumpr2  34031  esumpinfval  34037  esumpcvgval  34042  ofcfn  34064  pwsiga  34094  prsiga  34095  sigainb  34100  ldgenpisyslem1  34127  measiuns  34181  relfae  34211  pmeasmono  34289  sitgf  34312  eulerpartgbij  34337  sgnmulsgn  34514  sgnmulsgp  34515  signswch  34538  signslema  34539  signstlen  34544  signstfvn  34546  circlevma  34619  bnj216  34708  bnj151  34853  bnj517  34861  bnj970  34923  bnj1145  34969  bnj1498  35037  fineqvrep  35071  fineqvac  35073  wevgblacfn  35076  0nn0m1nnn0  35080  pthhashvtx  35095  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  36288  fneref  36316  neibastop2lem  36326  limsucncmpi  36411  bj-exlimmpbir  36880  curryset  36912  bj-snglex  36939  bj-restpw  37058  bj-inftyexpidisj  37176  topdifinffinlem  37313  relowlssretop  37329  rdgeqoa  37336  finxpreclem6  37362  fvineqsneq  37378  pibt2  37383  poimirlem23  37603  poimirlem29  37609  poimirlem31  37611  volsupnfl  37625  cnambfre  37628  dvasin  37664  dvacos  37665  sdclem2  37702  sstotbnd2  37734  ssbnd  37748  ismgmOLD  37810  grpokerinj  37853  rngomndo  37895  isdrngo1  37916  ac6s6  38132  iss2  38300  cnvelrels  38451  cosselrels  38452  brssrid  38458  brcnvssrid  38463  dfdisjs5  38668  eldisjs5  38682  mpets2  38797  pets  38808  prtlem12  38823  riotasv2d  38913  lkrscss  39054  islshpkrN  39076  isline  39696  ispointN  39699  0psubN  39706  linepsubN  39709  atpsubN  39710  cdlemk36  40870  diafn  40991  dibfna  41111  dibvalrel  41120  dicvalrelN  41142  diclspsn  41151  dihvalrel  41236  dih1  41243  lclkrlem1  41463  lclkr  41490  mapd1o  41605  mapdin  41619  hdmapfnN  41786  hgmapfnN  41845  lcmineqlem10  41995  sticksstones9  42111  sn-iotalem  42214  repncan2  42358  sn-inelr  42443  elrfirn  42651  ismrcd1  42654  istopclsd  42656  rabren3dioph  42771  jm2.17b  42918  jm2.22  42952  jm2.23  42953  ttac  42993  pw2f1ocnv  42994  dnnumch1  43001  hbtlem5  43085  mncn0  43096  aaitgo  43119  rngunsnply  43130  unielss  43179  onexlimgt  43204  cantnfresb  43286  dflim5  43291  naddwordnexlem4  43363  safesnsupfiss  43377  safesnsupfidom1o  43379  safesnsupfilb  43380  ensucne0OLD  43492  clcnvlem  43585  relexp01min  43675  ntrf  44085  ssrecnpr  44277  seff  44278  sblpnf  44279  nzss  44286  dvconstbi  44303  ipo0  44418  ifr0  44419  addrfn  44441  subrfn  44442  mulvfn  44443  refsum2cnlem1  44937  rn1st  45183  ellimciota  45535  dvmptconst  45836  dvmptidg  45838  dvmulcncf  45846  dvdivcncf  45848  stoweidlem26  45947  stoweidlem50  45971  stoweidlem57  45978  aiotaval  47010  ndfatafv2nrn  47136  afv2ndefb  47139  funop1  47198  fun2dmnopgexmpl  47199  2ffzoeq  47242  iccpartiltu  47296  iccpartigtl  47297  zofldiv2ALTV  47536  evenprm2  47588  9fppr8  47611  stgoldbwt  47650  nnsum3primesle9  47668  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  tgblthelfgott  47689  dfclnbgr6  47728  grtrimap  47797  usgrexmpl2trifr  47852  uspgrex  47873  0mgm  47889  nnsgrpmgm  47899  rngchomffvalALTV  48001  rhmsubcALTVlem1  48004  funcringcsetcALTV2lem4  48016  funcringcsetclem4ALTV  48039  srhmsubcALTV  48048  mapsnop  48069  zlmodzxzldeplem4  48232  zofldiv2  48265  fdivval  48273  nnlog2ge0lt1  48300  dig1  48342  itcoval2  48398  itcoval3  48399  mosn  48544  mo0  48545  mof02  48552  mofeu  48561  f102g  48565  f1mo  48566  f1omo  48574  intubeu  48656  unilbeu  48657  functhinclem1  48708  fullthinc  48713  thincciso  48716  indthinc  48719  indthincALT  48720